:: INT_2 semantic presentation begin definitionlet "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"|."::: redefine func :::"abs"::: "a" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: INT_2:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))))) "holds" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "c")))) ; theorem :: INT_2:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c"))))) ; theorem :: INT_2:3 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) "iff" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"Integer":::); func "a" :::"lcm"::: "b" -> ($#m1_hidden :::"Nat":::) means :: INT_2:def 1 (Bool "(" (Bool "a" ($#r1_int_1 :::"divides"::: ) it) & (Bool "b" ($#r1_int_1 :::"divides"::: ) it) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "a" ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) & (Bool "b" ($#r1_int_1 :::"divides"::: ) (Set (Var "m")))) "holds" (Bool it ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) ")" ) ")" ))) ; end; :: deftheorem defines :::"lcm"::: INT_2:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b3"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "b3")) ($#r1_int_1 :::"divides"::: ) (Set (Var "m"))) ")" ) ")" ) ")" ))); theorem :: INT_2:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; definitionlet "a", "b" be ($#m1_hidden :::"Integer":::); func "a" :::"gcd"::: "b" -> ($#m1_hidden :::"Nat":::) means :: INT_2:def 2 (Bool "(" (Bool it ($#r1_int_1 :::"divides"::: ) "a") & (Bool it ($#r1_int_1 :::"divides"::: ) "b") & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) "a") & (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) "b")) "holds" (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) it) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "b1")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b1"))) ")" ) ")" ))) ; end; :: deftheorem defines :::"gcd"::: INT_2:def 2 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "b3")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "m")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b3"))) ")" ) ")" ) ")" ))); theorem :: INT_2:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: INT_2:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) "iff" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k4_xcmplx_0 :::"-"::: ) "n") -> ($#~v7_ordinal1 "non" ($#v7_ordinal1 :::"natural"::: ) ) ; end; theorem :: INT_2:7 (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)) "is" (Bool "not" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: INT_2:8 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")))) & (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) ")" )) ; theorem :: INT_2:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "c")))) "holds" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "c")))) ; theorem :: INT_2:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b"))))) "implies" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b"))))) "implies" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "implies" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")))) ")" ")" )) ; theorem :: INT_2:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b"))))) ; theorem :: INT_2:12 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Num 1) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) ")" )) ; theorem :: INT_2:13 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)))) ")" ) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" )) ; theorem :: INT_2:14 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) ")" )) ; theorem :: INT_2:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "c"))) "iff" (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")))) ")" )) ; theorem :: INT_2:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b"))) "iff" (Bool (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "a"))) ($#r1_int_1 :::"divides"::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "b")))) ")" )) ; theorem :: INT_2:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: INT_2:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b"))))) ; theorem :: INT_2:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_int_1 :::"divides"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "c")))) ; theorem :: INT_2:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: INT_2:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "a")))) ; theorem :: INT_2:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))))) ; definitionlet "a", "b" be ($#m1_hidden :::"Integer":::); pred "a" "," "b" :::"are_relative_prime"::: means :: INT_2:def 3 (Bool (Set "a" ($#k3_int_2 :::"gcd"::: ) "b") ($#r1_hidden :::"="::: ) (Num 1)); symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "b")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Num 1))) ; end; :: deftheorem defines :::"are_relative_prime"::: INT_2:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_int_2 :::"are_relative_prime"::: ) ) "iff" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )); theorem :: INT_2:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "ex" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a1")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b1")))) & (Bool (Set (Var "a1")) "," (Set (Var "b1")) ($#r1_int_2 :::"are_relative_prime"::: ) ) ")" ))) ; theorem :: INT_2:24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "c")))) & (Bool (Set (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "c")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "c")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "c")))) ")" )) ; theorem :: INT_2:25 (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Var "c")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) ; theorem :: INT_2:26 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b"))) "," (Set (Var "c")) ($#r1_int_2 :::"are_relative_prime"::: ) )) ; definitionlet "p" be ($#m1_hidden :::"Nat":::); attr "p" is :::"prime"::: means :: INT_2:def 4 (Bool "(" (Bool "p" ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "n")) ($#r1_int_1 :::"divides"::: ) "p") "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) "p") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"prime"::: INT_2:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "n")) ($#r1_int_1 :::"divides"::: ) (Set (Var "p"))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ) ")" ) ")" ) ")" )); theorem :: INT_2:27 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_int_1 :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) ; theorem :: INT_2:28 (Bool (Num 2) "is" ($#v1_int_2 :::"prime"::: ) ) ; theorem :: INT_2:29 (Bool (Bool "not" (Num 4) "is" ($#v1_int_2 :::"prime"::: ) )) ; registration cluster ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v7_ordinal1 :::"natural"::: ) ($#v1_xcmplx_0 :::"complex"::: ) bbbadV1_XREAL_0() ($#v1_int_1 :::"integer"::: ) ($#v1_int_2 :::"prime"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v7_ordinal1 :::"natural"::: ) ($#v1_xcmplx_0 :::"complex"::: ) bbbadV1_XREAL_0() ($#v1_int_1 :::"integer"::: ) ($#~v1_int_2 "non" ($#v1_int_2 :::"prime"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: INT_2:30 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Bool "not" (Set (Var "p")) "," (Set (Var "q")) ($#r1_int_2 :::"are_relative_prime"::: ) ))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: INT_2:31 (Bool "for" (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "l")) ($#r1_xxreal_0 :::">="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "p")) ($#r1_int_1 :::"divides"::: ) (Set (Var "l"))) ")" ))) ; begin theorem :: INT_2:32 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "j")))) & (Bool (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set (Var "j")))) ")" )) ; theorem :: INT_2:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k2_int_2 :::"lcm"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "b")) ")" )))) ; theorem :: INT_2:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "b")) ")" )))) ;