:: NEWTON  semantic presentation begin  




















theorem :: NEWTON:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  ")" )  "}"   ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: NEWTON:2 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "a"))  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "F")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))))) ; 
 
theorem :: NEWTON:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "G")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "a"))  ($#k10_rvsum_1 :::"*"::: )  (Set (Var "G")) ")" ))))) ; 
 registrationlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k2_finseq_2 :::"|->"::: )  "x") ->   ($#v1_valued_0 :::"complex-yielding"::: )   ; 
end; definitionlet "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); func "x" :::"|^"::: "n" ->    ($#m1_hidden :::"set"::: )   equals :: NEWTON:def 1 (Set   ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" "n"  ($#k2_finseq_2 :::"|->"::: )  "x" ")" )); end; 






:: deftheorem    defines :::"|^"::: NEWTON:def 1 :  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k19_rvsum_1 :::"Product"::: )  (Set  "(" (Set (Var "n"))  ($#k2_finseq_2 :::"|->"::: )  (Set (Var "x")) ")" ))))); 
 registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "x"  ($#k1_newton :::"|^"::: )  "n") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "x" be   ($#m1_subset_1 :::"Real":::); let "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"|^"::: redefine func "x" :::"|^"::: "n" ->   ($#m1_subset_1 :::"Real":::); end; 


registrationlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "z"  ($#k1_newton :::"|^"::: )  "n") ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; 
theorem :: NEWTON:4 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NEWTON:5 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: NEWTON:6 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")))))) ; 
 registrationlet "x", "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "x"  ($#k1_newton :::"|^"::: )  "n") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 




theorem :: NEWTON:7 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")) ")" ))))) ; 
 
theorem :: NEWTON:8 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "s"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "t")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "t")) ")" ))))) ; 
 
theorem :: NEWTON:9 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "s"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "t")) ")" ))))) ; 
 
theorem :: NEWTON:10 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Num 1)  ($#k2_newton :::"|^"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NEWTON:11 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k2_newton :::"|^"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k1_finseq_2 :::"idseq"::: )  "n") ->   ($#v4_valued_0 :::"natural-valued"::: )   ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); func "n" :::"!":::  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: NEWTON:def 2 (Set   ($#k19_rvsum_1 :::"Product"::: )  (Set  "("  ($#k1_finseq_2 :::"idseq"::: )  "n" ")" )); end; 





:: deftheorem    defines :::"!"::: NEWTON:def 2 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_newton :::"!"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k19_rvsum_1 :::"Product"::: )  (Set  "("  ($#k1_finseq_2 :::"idseq"::: )  (Set (Var "n")) ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k3_newton :::"!"::: )  ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; 
theorem :: NEWTON:12 (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_newton :::"!"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: NEWTON:13 (Bool (Set (Num 1)  ($#k3_newton :::"!"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: NEWTON:14 (Bool (Set (Num 2)  ($#k3_newton :::"!"::: )  )  ($#r1_hidden :::"="::: )  (Num 2)) ; 
 
theorem :: NEWTON:15 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k3_newton :::"!"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k3_newton :::"!"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: NEWTON:16 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k3_newton :::"!"::: )  ) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k3_newton :::"!"::: )  ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: NEWTON:17 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set (Var "s"))  ($#k3_newton :::"!"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k3_newton :::"!"::: )  ) ->   ($#v2_xxreal_0 :::"positive"::: )   ; 
end; 
theorem :: NEWTON:18 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set  "(" (Set (Var "s"))  ($#k3_newton :::"!"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k3_newton :::"!"::: )  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 definitionlet "k", "n" be   ($#m1_hidden :::"Nat":::); func "n" :::"choose"::: "k" ->    ($#m1_hidden :::"set"::: )   means :: NEWTON:def 3 (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k6_xcmplx_0 :::"-"::: )  "k"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" "n"  ($#k3_newton :::"!"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" "k"  ($#k3_newton :::"!"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "l"))  ($#k3_newton :::"!"::: )  ")" ) ")" )))) if (Bool "n"  ($#r1_xxreal_0 :::">="::: )  "k")  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 






:: deftheorem    defines :::"choose"::: NEWTON:def 3 :  (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_newton :::"choose"::: )  (Set (Var "k")))) "iff" (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "k"))))) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k3_newton :::"!"::: )  ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "(" (Set (Var "k"))  ($#k3_newton :::"!"::: )  ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "l"))  ($#k3_newton :::"!"::: )  ")" ) ")" ))))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k"))))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k4_newton :::"choose"::: )  (Set (Var "k")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" ))); 
 registrationlet "k", "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k4_newton :::"choose"::: )  "k") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "k", "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"choose"::: redefine func "n" :::"choose"::: "k" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: NEWTON:19 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NEWTON:20 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "t"))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "t"))))) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set (Var "r"))))) ; 
 
theorem :: NEWTON:21 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NEWTON:22 (Bool  "for" (Set (Var "t")) "," (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "t"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k5_newton :::"choose"::: )  (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "t"))  ($#k5_newton :::"choose"::: )  (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "t"))  ($#k5_newton :::"choose"::: )  (Set (Var "s")) ")" )))) ; 
 
theorem :: NEWTON:23 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 
theorem :: NEWTON:24 (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))) ; 
 
theorem :: NEWTON:25 (Bool  "for" (Set (Var "s")) "," (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "s"))  ($#k5_newton :::"choose"::: )  (Set (Var "r"))) "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ))) ; 
 
theorem :: NEWTON:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "i")) ")" )  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "l"))  ($#k5_newton :::"choose"::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )  ($#k5_newton :::"choose"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))))) ; 
 registrationlet "k", "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k4_newton :::"choose"::: )  "k") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; definitionlet "k", "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"choose"::: redefine func "n" :::"choose"::: "k" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); func  "(" "a" "," "b" ")"  :::"In_Power"::: "n" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: NEWTON:def 4 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set "n"  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it)) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "m"))))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" "n"  ($#k6_newton :::"choose"::: )  (Set (Var "m")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "a"  ($#k1_newton :::"|^"::: )  (Set (Var "l")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "b"  ($#k1_newton :::"|^"::: )  (Set (Var "m")) ")" )))  ")" )  ")" ); end; 







:: deftheorem    defines :::"In_Power"::: NEWTON:def 4 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b4")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k7_newton :::"In_Power"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "l")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b4")))) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "l"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "m")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "l")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")) ")" )))  ")" )  ")" )  ")" )))); 
 
theorem :: NEWTON:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k7_newton :::"In_Power"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ))) ; 
 
theorem :: NEWTON:28 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k7_newton :::"In_Power"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")))))) ; 
 
theorem :: NEWTON:29 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k7_newton :::"In_Power"::: )  (Set (Var "s")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "s"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "s")))))) ; 
 
theorem :: NEWTON:30 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k7_newton :::"In_Power"::: )  (Set (Var "s")) ")" ))))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Newton_Coeff"::: "n" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) means :: NEWTON:def 5 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set "n"  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it)) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "n"  ($#k6_newton :::"choose"::: )  (Set (Var "k"))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Newton_Coeff"::: NEWTON:def 5 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_newton :::"Newton_Coeff"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b2")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "i"))  ($#k5_real_1 :::"-"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k6_newton :::"choose"::: )  (Set (Var "k"))))  ")" )  ")" )  ")" ))); 
 
theorem :: NEWTON:31 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k8_newton :::"Newton_Coeff"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set  "(" (Num 1) "," (Num 1) ")"   ($#k7_newton :::"In_Power"::: )  (Set (Var "s"))))) ; 
 
theorem :: NEWTON:32 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k8_newton :::"Newton_Coeff"::: )  (Set (Var "s")) ")" )))) ; 
 begin  
theorem :: NEWTON:33 (Bool  "for" (Set (Var "l")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "l")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) ; 
 
theorem :: NEWTON:34 (Bool  "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "l"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"!"::: redefine func "n" :::"!":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; 
theorem :: NEWTON:35 (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "l"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "l"))  ($#k9_newton :::"!"::: )  ))) ; 
 
theorem :: NEWTON:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: NEWTON:37 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Set (Var "k"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 
theorem :: NEWTON:38 (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "l"))  ($#k9_newton :::"!"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "l")))) ; 
 
theorem :: NEWTON:39 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool  "not" (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: NEWTON:40 (Bool  "for" (Set (Var "j")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "j"))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "j"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" )  ($#k9_newton :::"!"::: )  ))) ; 
 
theorem :: NEWTON:41 (Bool  "for" (Set (Var "j")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l"))) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "j"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "l"))  ($#k9_newton :::"!"::: )  ))) ; 
 
theorem :: NEWTON:42 (Bool  "for" (Set (Var "j")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "j"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "l"))  ($#k9_newton :::"!"::: )  ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "l")))) ; 
 
theorem :: NEWTON:43 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set  "(" (Set (Var "n"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")) ")" )  ($#k5_nat_d :::"lcm"::: )  (Set (Var "k"))))) ; 
 
theorem :: NEWTON:44 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: NEWTON:45 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m")))  ")" ) "iff" (Bool (Set (Set (Var "n"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m")))  ")" )) ; 
 
theorem :: NEWTON:46 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: NEWTON:47 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n"))))) ; 
 
theorem :: NEWTON:48 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set  "(" (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k"))))) ; 
 
theorem :: NEWTON:49 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: NEWTON:50 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) & (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "k")))  ")" ) "iff" (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k"))))  ")" )) ; 
 
theorem :: NEWTON:51 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: NEWTON:52 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: NEWTON:53 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")) ")" )  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: NEWTON:54 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set  "(" (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: NEWTON:55 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set  "(" (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")) ")" )  ($#k5_nat_d :::"lcm"::: )  (Set (Var "m"))))) ; 
 
theorem :: NEWTON:56 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k"))))) ; 
 
theorem :: NEWTON:57 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "k"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "k"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n"))))) ; 
 
theorem :: NEWTON:58 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NEWTON:59 (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"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NEWTON:60 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")) ")" )  ($#k5_nat_d :::"lcm"::: )  (Set  "(" (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "k")) ")" ))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set  "(" (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "k")) ")" )))) ; 
 
theorem :: NEWTON:61 (Bool  "for" (Set (Var "m")) "," (Set (Var "l")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set  "(" (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "l")) ")" ))  ($#r1_nat_d :::"divides"::: )  (Set (Set  "(" (Set (Var "m"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "n")) ")" )  ($#k6_nat_d :::"gcd"::: )  (Set (Var "l"))))) ; 
 
theorem :: NEWTON:62 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "n"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "m")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "n"))  ($#k5_nat_d :::"lcm"::: )  (Set (Var "m"))))) ; 
 











theorem :: NEWTON:63 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "n"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Set  "(" (Set (Var "m"))  ($#k3_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k3_nat_d :::"div"::: )  (Set (Var "m")) ")" ) ")" )))) ; 
 
theorem :: NEWTON:64 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: NEWTON:65 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i2")))) ; 
 
theorem :: NEWTON:66 (Bool  "for" (Set (Var "i2")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "i1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "i1"))  ($#k5_int_1 :::"div"::: )  (Set (Var "i2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "i2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "i1"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "i2")) ")" )))) ; 
 
theorem :: NEWTON:67 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "i1")) "being"   ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set  "(" (Set (Var "i"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "i1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")))))) ; 
 definitionfunc  :::"SetPrimes":::  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) means :: NEWTON:def 6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" )); end; 




:: deftheorem    defines :::"SetPrimes"::: NEWTON:def 6 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_newton :::"SetPrimes"::: )  )) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool (Set (Var "n")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" ))  ")" )); 
 registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )     ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xreal_0 :::"real"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_int_1 :::"integer"::: )     ($#v1_int_2 :::"prime"::: )   bbbadV1_RAT_1()   ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )   bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() bbbadV4_MEMBERED() bbbadV5_MEMBERED() bbbadV6_MEMBERED()  for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 

cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v7_ordinal1 :::"natural"::: )     ($#v1_xcmplx_0 :::"complex"::: )     ($#v1_xreal_0 :::"real"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_int_1 :::"integer"::: )     ($#v1_int_2 :::"prime"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Prime is   ($#v1_int_2 :::"prime"::: )    ($#m1_hidden :::"Nat":::); end; 


definitionlet "p" be   ($#m1_hidden :::"Nat":::); func  :::"SetPrimenumber"::: "p" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) means :: NEWTON:def 7 (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<"::: )  "p") & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" )  ")" )); end; 





:: deftheorem    defines :::"SetPrimenumber"::: NEWTON:def 7 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "p")))) "iff" (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "q"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))) & (Bool (Set (Var "q")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" )  ")" ))  ")" ))); 
 
theorem :: NEWTON:68 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_newton :::"SetPrimes"::: )  ))) ; 
 
theorem :: NEWTON:69 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "q"))))) ; 
 
theorem :: NEWTON:70 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "p"))))) ; 
 
theorem :: NEWTON:71 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "p"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k11_newton :::"SetPrimenumber"::: )  "n") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 



theorem :: NEWTON:72 (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::) "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_int_2 :::"prime"::: )  ) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "l")))  ")" ))) ; 
 registration
cluster (Set   ($#k10_newton :::"SetPrimes"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Num 2)) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: NEWTON:73 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "m")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "m"))))) ; 
 
theorem :: NEWTON:74 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool  "not" (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "m")))))) ; 
 
theorem :: NEWTON:75 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "("  ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "n")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) )) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: NEWTON:76 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set  "("  ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "g")))))) ; 
 
theorem :: NEWTON:77 (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool  "not" (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "m")))))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"primenumber"::: "n" ->   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: NEWTON:def 8 (Bool "n"  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k11_newton :::"SetPrimenumber"::: )  it ")" ))); end; 





:: deftheorem    defines :::"primenumber"::: NEWTON:def 8 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_int_2 :::"prime"::: )     ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_newton :::"primenumber"::: )  (Set (Var "n")))) "iff" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "b2")) ")" )))  ")" ))); 
 
theorem :: NEWTON:78 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k11_newton :::"SetPrimenumber"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "k")) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n"))) & (Bool (Set (Var "k")) "is"   ($#v1_int_2 :::"prime"::: )  )  ")" )  "}"  )) ; 
 
theorem :: NEWTON:79 (Bool (Set   ($#k10_newton :::"SetPrimes"::: )  ) "is"   ($#v1_finset_1 :::"infinite"::: )  ) ; 
 registration
cluster (Set   ($#k10_newton :::"SetPrimes"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"infinite"::: )   ; 
end; 



theorem :: NEWTON:80 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i")) "is"   ($#v1_int_2 :::"prime"::: )  )) "holds"  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")))) "or" (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) "or" (Bool (Set (Var "i"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: NEWTON:81 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2)))  ")" )) ; 
 
theorem :: NEWTON:82 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k5_int_1 :::"div"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k3_nat_d :::"div"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "m"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k4_nat_d :::"mod"::: )  (Set (Var "n"))))  ")" )) ; 
 



theorem :: NEWTON:83 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: NEWTON:84 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 definitionlet "m", "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"|^"::: redefine func "m" :::"|^"::: "n" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; 
theorem :: NEWTON:85 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) ; 
 
theorem :: NEWTON:86 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds" (Bool (Set (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))) ; 
 


scheme  :: NEWTON:sch 1 Euklides9{ F1(  ($#m1_hidden :::"Nat":::)) ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F2(  ($#m1_hidden :::"Nat":::)) ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F3() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F4() ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) } : 
(Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set F1 "(" (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F3 "("  ")" )  ($#k6_nat_d :::"gcd"::: )  (Set F4 "("  ")" ))) & (Bool (Set F2 "(" (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))
 provided
(Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set F4 "("  ")" ))
 and  
(Bool (Set F4 "("  ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "("  ")" ))
 and  
(Bool (Set F1 "(" (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" ))
 and  
(Bool (Set F2 "(" (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))
 and  
(Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F2 "(" (Set (Var "k")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set F1 "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "k")) ")" )) & (Bool (Set F2 "(" (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set F1 "(" (Set (Var "k")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set F2 "(" (Set (Var "k")) ")" )))  ")" ))
 proof 


end; 








theorem :: NEWTON:87 (Bool  "for" (Set (Var "r")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: NEWTON:88 (Bool  "for" (Set (Var "n1")) "," (Set (Var "m1")) "," (Set (Var "n2")) "," (Set (Var "m2")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n1")) ")" )  ($#k3_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n2")) ")" )  ($#k3_nat_1 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "n1"))  ($#r1_hidden :::"="::: )  (Set (Var "n2"))) & (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set (Var "m2")))  ")" )) ; 
 
theorem :: NEWTON:89 (Bool  "for" (Set (Var "m")) "," (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 "m"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "m"))  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))) ;