:: NAT_D semantic presentation begin definitionlet "k", "l" be ($#m1_hidden :::"Nat":::); :: original: :::"div"::: redefine func "k" :::"div"::: "l" -> ($#m1_hidden :::"Nat":::) means :: NAT_D:def 1 (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set "(" "l" ($#k3_xcmplx_0 :::"*"::: ) it ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) "l") ")" )) "or" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "l" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"div"::: NAT_D:def 1 : (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_d :::"div"::: ) (Set (Var "l")))) "iff" (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "l"))) ")" )) "or" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" )); definitionlet "k", "l" be ($#m1_hidden :::"Nat":::); :: original: :::"mod"::: redefine func "k" :::"mod"::: "l" -> ($#m1_hidden :::"Nat":::) means :: NAT_D:def 2 (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "k" ($#r1_hidden :::"="::: ) (Set (Set "(" "l" ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) it)) & (Bool it ($#r1_xxreal_0 :::"<"::: ) "l") ")" )) "or" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "l" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"mod"::: NAT_D:def 2 : (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_d :::"mod"::: ) (Set (Var "l")))) "iff" (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b3")))) & (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "l"))) ")" )) "or" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" )); definitionlet "k", "l" be ($#m1_hidden :::"Nat":::); :: original: :::"div"::: redefine func "k" :::"div"::: "l" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"mod"::: redefine func "k" :::"mod"::: "l" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NAT_D:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set (Var "j")) ($#k4_nat_d :::"mod"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) ; theorem :: NAT_D:2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k3_nat_1 :::"*"::: ) (Set "(" (Set (Var "j")) ($#k3_nat_d :::"div"::: ) (Set (Var "i")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "j")) ($#k4_nat_d :::"mod"::: ) (Set (Var "i")) ")" )))) ; definitionlet "k", "l" be ($#m1_hidden :::"Nat":::); :: original: :::"divides"::: redefine pred "k" :::"divides"::: "l" means :: NAT_D:def 3 (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "l" ($#r1_hidden :::"="::: ) (Set "k" ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t"))))); reflexivity (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t")))))) ; end; :: deftheorem defines :::"divides"::: NAT_D:def 3 : (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r1_nat_d :::"divides"::: ) (Set (Var "l"))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t"))))) ")" )); theorem :: NAT_D:3 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "j")) ($#r1_nat_d :::"divides"::: ) (Set (Var "i"))) "iff" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k3_nat_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k3_nat_d :::"div"::: ) (Set (Var "j")) ")" ))) ")" )) ; theorem :: NAT_D:4 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_nat_d :::"divides"::: ) (Set (Var "h")))) "holds" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "h")))) ; theorem :: NAT_D:5 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_nat_d :::"divides"::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) ; theorem :: NAT_D:6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Num 1) ($#r1_nat_d :::"divides"::: ) (Set (Var "i"))) ")" )) ; theorem :: NAT_D:7 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) ; theorem :: NAT_D:8 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "h")))) "holds" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "h"))))) ; theorem :: NAT_D:9 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "j")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "h"))))) ; theorem :: NAT_D:10 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "h")))) ; theorem :: NAT_D:11 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Var "h")))) "holds" (Bool (Set (Var "i")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "j")) ($#k4_nat_d :::"mod"::: ) (Set (Var "h"))))) ; definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); redefine func "k" :::"lcm"::: "n" means :: NAT_D:def 4 (Bool "(" (Bool "k" ($#r1_nat_d :::"divides"::: ) it) & (Bool "n" ($#r1_nat_d :::"divides"::: ) it) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "k" ($#r1_nat_d :::"divides"::: ) (Set (Var "m"))) & (Bool "n" ($#r1_nat_d :::"divides"::: ) (Set (Var "m")))) "holds" (Bool it ($#r1_nat_d :::"divides"::: ) (Set (Var "m"))) ")" ) ")" ); end; :: deftheorem defines :::"lcm"::: NAT_D:def 4 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "k")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b3"))) & (Bool (Set (Var "n")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_nat_d :::"divides"::: ) (Set (Var "m"))) & (Bool (Set (Var "n")) ($#r1_nat_d :::"divides"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "b3")) ($#r1_nat_d :::"divides"::: ) (Set (Var "m"))) ")" ) ")" ) ")" ))); definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); :: original: :::"lcm"::: redefine func "k" :::"lcm"::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); redefine func "k" :::"gcd"::: "n" means :: NAT_D:def 5 (Bool "(" (Bool it ($#r1_nat_d :::"divides"::: ) "k") & (Bool it ($#r1_nat_d :::"divides"::: ) "n") & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) "k") & (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) "n")) "holds" (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"gcd"::: NAT_D:def 5 : (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_nat_d :::"divides"::: ) (Set (Var "k"))) & (Bool (Set (Var "b3")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "m")) ($#r1_nat_d :::"divides"::: ) (Set (Var "b3"))) ")" ) ")" ) ")" ))); definitionlet "k", "n" be ($#m1_hidden :::"Nat":::); :: original: :::"gcd"::: redefine func "k" :::"gcd"::: "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; scheme :: NAT_D:sch 1 Euklides{ F1( ($#m1_hidden :::"Nat":::)) -> ($#m1_hidden :::"Nat":::), F2() -> ($#m1_hidden :::"Nat":::), F3() -> ($#m1_hidden :::"Nat":::) } : (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set F1 "(" (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F2 "(" ")" ) ($#k6_nat_d :::"gcd"::: ) (Set F3 "(" ")" ))) & (Bool (Set F1 "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) provided (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set F3 "(" ")" )) & (Bool (Set F3 "(" ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set F2 "(" ")" )) ")" ) and (Bool "(" (Bool (Set F1 "(" (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool (Set F1 "(" (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) ")" ) and (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set F1 "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" (Set (Var "n")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set F1 "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) proof end; theorem :: NAT_D:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: NAT_D:13 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_D:14 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Num 1) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: NAT_D:15 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "k")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set (Var "l")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_D:16 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "k")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "l")))) ; theorem :: NAT_D:17 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "k")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:18 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k3_nat_d :::"div"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: NAT_D:19 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "k")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "l")) ")" ) ($#k3_nat_d :::"div"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k3_nat_d :::"div"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k3_nat_d :::"div"::: ) (Set (Var "n")) ")" )))) ; begin theorem :: NAT_D:20 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" ) ($#k3_nat_d :::"div"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))) ; theorem :: NAT_D:21 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "m")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "m")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:22 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "p")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "s")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:23 (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_nat_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:24 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "k")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) ; theorem :: NAT_D:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_D:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:27 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "i")) ($#k3_nat_d :::"div"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_D:28 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "n")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k6_nat_d :::"gcd"::: ) (Set "(" (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Set (Var "m")) ")" )))) ; scheme :: NAT_D:sch 2 INDI{ F1() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool P1[(Set ($#k6_numbers :::"0"::: ) )]) and (Bool (Set F1 "(" ")" ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool P1[(Set (Set F1 "(" ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "i")))]) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Set "(" (Set F1 "(" ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "i")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")))])) proof end; theorem :: NAT_D:29 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "j")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "j")) ")" )))) ; theorem :: NAT_D:30 (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 (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "j")) ")" )))) ; theorem :: NAT_D:31 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k5_nat_d :::"lcm"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: NAT_D:32 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: NAT_D:33 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set (Set (Var "i")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "j"))) "is" ($#v1_int_1 :::"integer"::: ) ))) ; definitionlet "i", "j" be ($#m1_hidden :::"Nat":::); :: original: :::"-'"::: redefine func "i" :::"-'"::: "j" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: NAT_D:34 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: NAT_D:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "a")) ($#k7_nat_d :::"-'"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a")))) ; theorem :: NAT_D:36 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) ; theorem :: NAT_D:37 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) ; theorem :: NAT_D:38 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set "(" (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))) ; theorem :: NAT_D:39 (Bool "for" (Set (Var "i")) "," (Set (Var "i1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i1"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) "or" (Bool (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i1"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i1"))))) ; theorem :: NAT_D:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: NAT_D:41 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) "holds" (Bool (Set (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i1"))))) ; theorem :: NAT_D:42 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) "holds" (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:43 (Bool "for" (Set (Var "i")) "," (Set (Var "i1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i1"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) "or" (Bool (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i1"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: NAT_D:44 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) "holds" (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) ; theorem :: NAT_D:45 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)))) ; theorem :: NAT_D:46 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2")))) "holds" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) ")" )) ; theorem :: NAT_D:47 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) "or" (Bool (Set (Set "(" (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set "(" (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set "(" (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) & (Bool (Set (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) ")" )) ; theorem :: NAT_D:48 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) "or" (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1))) ")" )) "holds" (Bool "(" (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i2")) ($#k1_nat_1 :::"+"::: ) (Num 2))) ")" )) ; theorem :: NAT_D:49 (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i2"))) "or" (Bool (Set (Set (Var "i1")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i2"))) ")" )) "holds" (Bool (Set (Var "i1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i2")) ($#k7_nat_d :::"-'"::: ) (Num 1)))) ; theorem :: NAT_D:50 (Bool "for" (Set (Var "i")) "," (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "i1")))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i2"))))) ; theorem :: NAT_D:51 (Bool "for" (Set (Var "i")) "," (Set (Var "i1")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "i1")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i1")))) ; theorem :: NAT_D:52 (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))))) ; theorem :: NAT_D:53 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) ; theorem :: NAT_D:54 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) ; theorem :: NAT_D:55 (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "j"))))) ; theorem :: NAT_D:56 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))))) ; theorem :: NAT_D:57 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "k"))))) ; theorem :: NAT_D:58 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i")))) ; theorem :: NAT_D:59 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:60 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Num 2)) ")" )) ; theorem :: NAT_D:61 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k5_int_1 :::"div"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_int_1 :::"div"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")))) ")" & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")))) ")" )) ; theorem :: NAT_D:62 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" ))) ; theorem :: NAT_D:63 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")))) ")" ")" )) ; theorem :: NAT_D:64 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "n"))) ")" & "(" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")))) ")" ")" )) ; theorem :: NAT_D:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")))))) ; theorem :: NAT_D:66 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:67 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))))) ; theorem :: NAT_D:68 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) (Bool "ex" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "a")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ))))) ; theorem :: NAT_D:69 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: NAT_D:70 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_nat_d :::"mod"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ;