:: PREPOWER  semantic presentation begin  registrationlet "i" be   ($#m1_hidden :::"Integer":::); 
cluster (Set  ($#k16_complex1 :::"|."::: ) "i" ($#k16_complex1 :::".|"::: ) ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 


























theorem :: PREPOWER:1 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a"))))) ; 
 
theorem :: PREPOWER:2 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) ; 
 definitionlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func "a" :::"GeoSeq":::  ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: PREPOWER:def 1 (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set "a"  ($#k1_newton :::"|^"::: )  (Set (Var "m"))))); end; 





:: deftheorem    defines :::"GeoSeq"::: PREPOWER:def 1 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_prepower :::"GeoSeq"::: )  )) "iff" (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")))))  ")" ))); 
 
theorem :: PREPOWER:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_prepower :::"GeoSeq"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "m"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "a"))))  ")" )  ")" )  ")" ))) ; 
 
theorem :: PREPOWER:4 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_prepower :::"GeoSeq"::: )  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: PREPOWER:5 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:6 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:7 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: PREPOWER:8 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "b"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: PREPOWER:9 (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":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:10 (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":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:11 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:13 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:14 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) ; 
 
theorem :: PREPOWER:15 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Num 2)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))))) ; 
 
theorem :: PREPOWER:16 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: PREPOWER:17 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set (Var "a")) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: PREPOWER:18 (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "m"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "s2")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")) ")" )  ($#k2_newton :::"|^"::: )  (Set (Var "m"))))  ")" ))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "n")))
 ; func "n" :::"-Root"::: "a" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: PREPOWER:def 2 (Bool  "("  (Bool (Set it  ($#k1_newton :::"|^"::: )  "n")  ($#r1_hidden :::"="::: )  "a") & (Bool it  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) if (Bool "a"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) if (Bool "a"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; end; 







:: deftheorem    defines :::"-Root"::: PREPOWER:def 2 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" )))); 
 definitionlet "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "a" be   ($#m1_subset_1 :::"Real":::); :: original: :::"-Root"::: redefine func "n" :::"-Root"::: "a" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: PREPOWER:19 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: PREPOWER:20 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_prepower :::"-Root"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:21 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 1)  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: PREPOWER:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: PREPOWER:23 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k3_prepower :::"-Root"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: PREPOWER:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: PREPOWER:25 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "m"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))))) ; 
 
theorem :: PREPOWER:26 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" ) ")" ))))) ; 
 
theorem :: PREPOWER:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "b")))))) ; 
 
theorem :: PREPOWER:28 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "b")))))) ; 
 
theorem :: PREPOWER:29 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: PREPOWER:30 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" ))) ; 
 
theorem :: PREPOWER:31 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k5_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )  ($#k10_real_1 :::"/"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:32 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 2)  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a"))))) ; 
 
theorem :: PREPOWER:33 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" ))) ; 
 definitionlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "k" be   ($#m1_hidden :::"Integer":::); func "a" :::"#Z"::: "k" ->    ($#m1_hidden :::"set"::: )   equals :: PREPOWER:def 3 (Set "a"  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  "k" ")" )) if (Bool "k"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) (Set (Set  "(" "a"  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  "k" ")" ) ")" )  ($#k5_xcmplx_0 :::"""::: )  ) if (Bool "k"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; end; 






:: deftheorem    defines :::"#Z"::: PREPOWER:def 3 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set (Var "k")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set (Var "k")) ")" ) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))  ")"   ")" ))); 
 registrationlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "k" be   ($#m1_hidden :::"Integer":::); 
cluster (Set "a"  ($#k4_prepower :::"#Z"::: )  "k") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a" be   ($#m1_subset_1 :::"Real":::); let "k" be   ($#m1_hidden :::"Integer":::); :: original: :::"#Z"::: redefine func "a" :::"#Z"::: "k" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: PREPOWER:34 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:35 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: PREPOWER:36 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:37 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Num 1)  ($#k5_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:38 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: PREPOWER:39 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: PREPOWER:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: PREPOWER:41 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: PREPOWER:42 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k5_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: PREPOWER:43 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  "(" (Set (Var "m"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "m")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: PREPOWER:44 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "l")) ")" ))))) ; 
 
theorem :: PREPOWER:45 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" )  ($#k4_prepower :::"#Z"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "l")) ")" ))))) ; 
 
theorem :: PREPOWER:46 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a")) ")" )  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")) ")" )))))) ; 
 definitionlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "p" be   ($#m1_hidden :::"Rational":::); func "a" :::"#Q"::: "p" ->    ($#m1_hidden :::"set"::: )   equals :: PREPOWER:def 4 (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  "p" ")" )  ($#k2_prepower :::"-Root"::: )  (Set  "(" "a"  ($#k4_prepower :::"#Z"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  "p" ")" ) ")" )); end; 






:: deftheorem    defines :::"#Q"::: PREPOWER:def 4 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rat_1 :::"denominator"::: )  (Set (Var "p")) ")" )  ($#k2_prepower :::"-Root"::: )  (Set  "(" (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set  "("  ($#k2_rat_1 :::"numerator"::: )  (Set (Var "p")) ")" ) ")" ))))); 
 registrationlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "p" be   ($#m1_hidden :::"Rational":::); 
cluster (Set "a"  ($#k6_prepower :::"#Q"::: )  "p") ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a" be   ($#m1_subset_1 :::"Real":::); let "p" be   ($#m1_hidden :::"Rational":::); :: original: :::"#Q"::: redefine func "a" :::"#Q"::: "p" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: PREPOWER:47 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:48 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: PREPOWER:49 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: PREPOWER:50 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k5_xcmplx_0 :::"""::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a"))))))) ; 
 
theorem :: PREPOWER:51 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::) "holds"  (Bool (Set (Num 1)  ($#k7_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:52 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: PREPOWER:53 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: PREPOWER:54 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: PREPOWER:55 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: PREPOWER:56 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: PREPOWER:57 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k7_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: PREPOWER:58 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" )  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" ))))) ; 
 
theorem :: PREPOWER:59 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")) ")" )  ($#k6_prepower :::"#Q"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set  "(" (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")) ")" ))))) ; 
 
theorem :: PREPOWER:60 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:61 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:62 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">"::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:63 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "q")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "q")))))) ; 
 
theorem :: PREPOWER:64 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "q")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "q")))))) ; 
 
theorem :: PREPOWER:65 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)))) ; 
 
theorem :: PREPOWER:66 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )   (Set   ($#k3_numbers :::"RAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_XBOOLE_0() bbbadV1_PARTFUN1((Set   ($#k5_numbers :::"NAT"::: )  )) bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_valued_0 :::"ext-real-valued"::: )     ($#v3_valued_0 :::"real-valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; definitioncanceled; mode Rational_Sequence is (Set   ($#k3_numbers :::"RAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )    ($#m1_subset_1 :::"Real_Sequence":::); end; 
:: deftheorem   PREPOWER:def 5 :  canceled;  
 
theorem :: PREPOWER:67 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))  ")" )  ")" ))) ; 
 
theorem :: PREPOWER:68 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))  ")" )  ")" ))) ; 
 definitionlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "s" be   ($#m1_subset_1 :::"Rational_Sequence":::); func "a" :::"#Q"::: "s" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: PREPOWER:def 6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set "a"  ($#k6_prepower :::"#Q"::: )  (Set  "(" "s"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 






:: deftheorem    defines :::"#Q"::: PREPOWER:def 6 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )))); 
 
theorem :: PREPOWER:69 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ))) ; 
 
theorem :: PREPOWER:70 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s2")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s2")))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s1"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s2"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s2")) ")" )))  ")" ))) ; 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set (Const "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func "a" :::"#R"::: "b" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: PREPOWER:def 7 (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  "b") & (Bool (Set "a"  ($#k8_prepower :::"#Q"::: )  (Set (Var "s"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" "a"  ($#k8_prepower :::"#Q"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  it)  ")" )); end; 







:: deftheorem    defines :::"#R"::: PREPOWER:def 7 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))) "iff" (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Rational_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "a"))  ($#k8_prepower :::"#Q"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b3")))  ")" ))  ")" ))); 
 definitionlet "a", "b" be   ($#m1_subset_1 :::"Real":::); :: original: :::"#R"::: redefine func "a" :::"#R"::: "b" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: PREPOWER:71 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:72 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: PREPOWER:73 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k9_prepower :::"#R"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:74 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))))) ; 
 
theorem :: PREPOWER:75 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:76 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:77 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:78 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:79 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:80 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" )  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: PREPOWER:81 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: PREPOWER:82 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b"))))) ; 
 
theorem :: PREPOWER:83 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b"))))) ; 
 
theorem :: PREPOWER:84 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b"))))) ; 
 
theorem :: PREPOWER:85 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:86 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: PREPOWER:87 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) ; 
 
theorem :: PREPOWER:88 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 
theorem :: PREPOWER:89 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Rational":::)  (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s2")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k7_prepower :::"#Q"::: )  (Set (Var "p"))))  ")" )  ")" )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")) ")" )  ($#k7_prepower :::"#Q"::: )  (Set (Var "p")))))) ; 
 
theorem :: PREPOWER:90 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "s1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s2")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "s1")) ")" ))))) ; 
 
theorem :: PREPOWER:91 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b")) ")" )  ($#k9_prepower :::"#R"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 begin  







theorem :: PREPOWER:92 (Bool  "for" (Set (Var "r")) "," (Set (Var "u")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "u"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "u"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k13_newton :::"|^"::: )  (Set (Var "k")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))))) ; 
 
theorem :: PREPOWER:93 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Set (Var "n"))))))) ; 
 
theorem :: PREPOWER:94 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Var "n"))  ($#r1_int_1 :::"divides"::: )  (Set (Set (Var "m"))  ($#k9_real_1 :::"-"::: )  (Set (Var "l"))))) ; 
 
theorem :: PREPOWER:95 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r1_nat_d :::"divides"::: )  (Set (Var "n"))) "iff" (Bool (Set (Var "m"))  ($#r1_int_1 :::"divides"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: PREPOWER:96 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "m"))  ($#k6_nat_d :::"gcd"::: )  (Set  "("  ($#k1_int_2 :::"abs"::: )  (Set  "(" (Set (Var "n"))  ($#k9_real_1 :::"-"::: )  (Set (Var "m")) ")" ) ")" )))) ; 
 
theorem :: PREPOWER:97 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_int_2 :::"gcd"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: PREPOWER:98 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "l")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: PREPOWER:99 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "l")))))) ; 
 
theorem :: PREPOWER:100 (Bool  "for" (Set (Var "l")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k5_prepower :::"#Z"::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ;