:: INT_4 semantic presentation begin theorem :: INT_4:1 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "X")) "," (Set (Set (Var "a")) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))) ($#r2_tarski :::"are_equipotent"::: ) ))) ; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK17_MEMBER_1("X" "," "a")) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: INT_4:2 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "a")) ($#k2_measure6 :::"++"::: ) (Set (Var "X")) ")" ))))) ; theorem :: INT_4:3 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "X")) "," (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) ($#r2_tarski :::"are_equipotent"::: ) ))) ; theorem :: INT_4:4 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "implies" (Bool (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" & (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" ) ")" ))) ; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK23_MEMBER_1("X" "," "a")) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: INT_4:5 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X")) ")" ))))) ; begin theorem :: INT_4:6 (Bool "for" (Set (Var "i")) "," (Set (Var "i1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_int_1 :::"divides"::: ) (Set (Var "i1"))) & (Bool (Set (Var "i1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i1"))))) ; theorem :: INT_4:7 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i3")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "i2"))) "iff" (Bool (Set (Set (Var "i1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i3"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "i2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i3")))) ")" )) ; theorem :: INT_4:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k4_nat_d :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_nat_d :::"mod"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "m")))))) ; theorem :: INT_4:9 (Bool "for" (Set (Var "i1")) "," (Set (Var "i")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "i1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i"))) "," (Set (Set (Var "i2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i3"))) & (Bool (Set (Var "i")) "," (Set (Var "i3")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Var "i1")) "," (Set (Var "i2")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i3")))) ; theorem :: INT_4:10 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i3")))) "holds" (Bool (Set (Set (Var "i1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k"))) "," (Set (Set (Var "i2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "i3")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")))))) ; theorem :: INT_4:11 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "i1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i3"))) "," (Set (Set (Var "i2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i3"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i")))) ; theorem :: INT_4:12 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k6_int_1 :::"mod"::: ) (Set (Var "i"))))) ; theorem :: INT_4:13 (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "r")))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" )))) ; theorem :: INT_4:14 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "i3")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i1")) "," (Set (Var "i2")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i3")))) "holds" (Bool (Set (Set (Var "i1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "i3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i2")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "i3"))))) ; theorem :: INT_4:15 (Bool "for" (Set (Var "a")) "," (Set (Var "m")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: INT_4:16 (Bool "for" (Set (Var "m")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: INT_4:17 (Bool "for" (Set (Var "m")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Bool "not" (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: INT_4:18 (Bool "for" (Set (Var "m")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; begin theorem :: INT_4:19 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k4_nat_d :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: INT_4:20 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" )))) ; theorem :: INT_4:21 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "not" (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "q")) ($#k4_nat_d :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))))) ; theorem :: INT_4:22 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set (Var "p")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")))) ")" )) ; theorem :: INT_4:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k4_nat_d :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_nat_d :::"mod"::: ) (Set (Var "m")))) "iff" (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")))) ")" )) ; theorem :: INT_4:24 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Bool "not" (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: INT_4:25 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Bool "not" (Set (Set "(" (Set "(" (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "q")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; begin definitionlet "m" be ($#m1_hidden :::"Integer":::); func :::"Cong"::: "m" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) means :: INT_4:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) "m") ")" )); end; :: deftheorem defines :::"Cong"::: INT_4:def 1 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "m"))) ")" )) ")" ))); registrationlet "m" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k1_int_4 :::"Cong"::: ) "m") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "m" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k1_int_4 :::"Cong"::: ) "m") -> ($#v1_relat_2 :::"reflexive"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; theorem :: INT_4:26 (Bool "for" (Set (Var "m")) "," (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")) ")" ) "," (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")) ")" ) "," (Set (Var "x")) ")" ))) "implies" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))) ; theorem :: INT_4:27 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "m")) "," (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")))))) ; theorem :: INT_4:28 (Bool "for" (Set (Var "a")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "for" (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "b")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k13_newton :::"|^"::: ) (Set "(" (Set "(" ($#k1_euler_1 :::"Euler"::: ) (Set (Var "m")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")))))) ; theorem :: INT_4:29 (Bool "for" (Set (Var "m")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "fp")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c1")) ($#r1_hidden :::"<>"::: ) (Set (Var "c2")))) "holds" (Bool "not" (Bool (Set (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "c1"))) "," (Set (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "c2"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "m")))) ")" ) ")" ))) ; begin theorem :: INT_4:30 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "d")) "," (Set (Var "b")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_real_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set ($#k5_wsierp_1 :::"Del"::: ) "(" (Set "(" (Set (Var "fp")) ($#k1_wsierp_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "b")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_wsierp_1 :::"Del"::: ) "(" (Set (Var "fp")) "," (Set (Var "b")) ")" ")" ) ($#k1_wsierp_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: INT_4:31 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set "(" ($#k3_wsierp_1 :::"Product"::: ) (Set "(" ($#k5_wsierp_1 :::"Del"::: ) "(" (Set (Var "fp")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: INT_4:32 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))) ($#r1_nat_d :::"divides"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "fp")))))) ; theorem :: INT_4:33 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "fp"))))))) ; theorem :: INT_4:34 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k7_real_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k5_wsierp_1 :::"Del"::: ) "(" (Set (Var "fp")) "," (Set (Var "a")) ")" ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp")) ")" )))))) ; theorem :: INT_4:35 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_nat_d :::"divides"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set "(" ($#k5_wsierp_1 :::"Del"::: ) "(" (Set (Var "fp")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: INT_4:36 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")))) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_nat_d :::"divides"::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "fp")))))) ; theorem :: INT_4:37 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "fp1")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_real_1 :::"-"::: ) (Set "(" (Set (Var "fp1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: INT_4:38 (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "fp"))) ($#r1_nat_d :::"divides"::: ) (Set (Var "a"))))) ; theorem :: INT_4:39 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "fp")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "fp1")) "being" ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k5_real_1 :::"-"::: ) (Set "(" (Set (Var "fp1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "y")) ($#k5_real_1 :::"-"::: ) (Set "(" (Set (Var "fp1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "fp")) ($#k1_recdef_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set ($#k3_wsierp_1 :::"Product"::: ) (Set (Var "fp"))))))) ; theorem :: INT_4:40 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m1")) "," (Set (Var "m2")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m2")))) ")" ) & (Bool (Set (Set "(" (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "c2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INT_4:41 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "not" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" "not" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INT_4:42 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "c2")) "," (Set (Var "c1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "c2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1"))))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m1")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "m2")))) ")" ) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "m1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "c2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "m2")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INT_4:43 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "a")) "," (Set (Var "c1")) "," (Set (Var "b")) "," (Set (Var "c2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "c1"))) & (Bool (Set (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "c2"))) & (Bool (Set (Var "m1")) "," (Set (Var "m2")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "w")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) "," (Set (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "m1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "w")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set "(" (Set (Var "m1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "m2")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" ))) ")" ) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "m1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "c2")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "m2")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "m1")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m1")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "w")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "m2")) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INT_4:44 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m3")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m1")) "," (Set (Var "m2")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "m1")) "," (Set (Var "m3")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "m2")) "," (Set (Var "m3")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m3")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "m2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "m1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: INT_4:45 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "m3")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "not" (Bool (Set (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m2"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")))) "or" "not" (Bool (Set (Set (Var "m1")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m3"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")))) "or" "not" (Bool (Set (Set (Var "m2")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "m3"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")))) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "not" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" "not" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" "not" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "m3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INT_4:46 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "n1")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3")) ")" ) ($#k5_nat_d :::"lcm"::: ) (Set "(" (Set (Var "n2")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3"))))) ; theorem :: INT_4:47 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n1")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n2"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b"))))) "holds" (Bool "ex" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n3")))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "n1")) ($#k3_nat_d :::"div"::: ) (Set "(" (Set (Var "n1")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "n1")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n2")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "n2")) ($#k3_nat_d :::"div"::: ) (Set "(" (Set (Var "n1")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k3_nat_d :::"div"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r")) ")" ) ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3")) ")" ) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "n3")) ($#k3_nat_d :::"div"::: ) (Set "(" (Set "(" (Set (Var "n1")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "n2")) ")" ) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n3")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; begin definitionlet "m" be ($#m1_hidden :::"Nat":::); let "X" be ($#m1_hidden :::"set"::: ) ; pred "X" :::"is_CRS_of"::: "m" means :: INT_4:def 2 (Bool "ex" (Set (Var "fp")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "fp")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) "m") & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_int_4 :::"Cong"::: ) "m" ")" ) "," (Set "(" (Set (Var "b")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"is_CRS_of"::: INT_4:def 2 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m"))) "iff" (Bool "ex" (Set (Var "fp")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "fp")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_int_4 :::"Cong"::: ) (Set (Var "m")) ")" ) "," (Set "(" (Set (Var "b")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ")" ) ")" )) ")" ))); theorem :: INT_4:48 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "{" (Set (Var "a")) where a "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) "}" ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))) ; theorem :: INT_4:49 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_int_4 :::"Cong"::: ) (Set (Var "m"))))) ")" ) ")" ))) ; theorem :: INT_4:50 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m"))) "iff" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: INT_4:51 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))) "holds" (Bool "ex" (Set (Var "fp")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fp"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fp"))))) "holds" (Bool (Set (Set (Var "fp")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) & (Bool (Set (Var "fp")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )))) ; theorem :: INT_4:52 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_int_4 :::"Cong"::: ) (Set (Var "m"))))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m"))))) ; theorem :: INT_4:53 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_measure6 :::"++"::: ) (Set (Var "X"))) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))))) ; theorem :: INT_4:54 (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "m")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "X")) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) ($#r1_int_4 :::"is_CRS_of"::: ) (Set (Var "m")))))) ;