:: POWER  semantic presentation begin  























theorem :: POWER:1 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: POWER:2 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: POWER:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"even"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func "n" :::"-root"::: "a" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   equals :: POWER:def 1 (Set "n"  ($#k2_prepower :::"-Root"::: )  "a") if (Bool  "("  (Bool "a"  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "n"  ($#r1_xxreal_0 :::">="::: )  (Num 1))  ")" ) (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" "n"  ($#k2_prepower :::"-Root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  "a" ")" ) ")" )) if (Bool  "("  (Bool "a"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "n" "is"   ($#v1_abian :::"odd"::: )  )  ")" ) ; end; 






:: deftheorem    defines :::"-root"::: POWER:def 1 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "implies" (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set (Var "a"))))  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "implies" (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n"))  ($#k2_prepower :::"-Root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" ) ")" )))  ")"   ")" ))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "a" be   ($#m1_subset_1 :::"Real":::); :: original: :::"-root"::: redefine func "n" :::"-root"::: "a" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POWER:4 (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  "("  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: POWER:5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POWER:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_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"))  ($#k2_power :::"-root"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: POWER:7 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_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"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: POWER:8 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))) ; 
 
theorem :: POWER:9 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: POWER:10 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" ) ")" ))))) ; 
 
theorem :: POWER:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: POWER:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: POWER:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (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))  ")" ) "or" (Bool  "("  (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: POWER:14 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (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))  ")" ) "or" (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "m")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set  "(" (Set (Var "m"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k1_power :::"-root"::: )  (Set (Var "a")))))) ; 
 
theorem :: POWER:15 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool  "("  (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))  ")" ) "or" (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  ) & (Bool (Set (Var "m")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "m"))  ($#k1_power :::"-root"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" )  ($#k1_power :::"-root"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" ) ")" ))))) ; 
 
theorem :: POWER:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool  "("  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))  ")" ) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "b")))))) ; 
 
theorem :: POWER:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))  ")" ) "or" (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )  ")" )) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "b")))))) ; 
 
theorem :: POWER:18 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_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"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: POWER:19 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a"))))  ")" ))) ; 
 
theorem :: POWER:20 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_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 :::"<"::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" ))) ; 
 
theorem :: POWER:21 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1)))  ")" ))) ; 
 
theorem :: POWER:22 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_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"))  ($#k1_power :::"-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 :: POWER:23 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (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"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-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", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func "a" :::"to_power"::: "b" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: POWER:def 2 (Bool it  ($#r1_hidden :::"="::: )  (Set "a"  ($#k9_prepower :::"#R"::: )  "b")) if (Bool "a"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) if (Bool  "("  (Bool "a"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool "b"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  "b") & (Bool it  ($#r1_hidden :::"="::: )  (Set "a"  ($#k4_prepower :::"#Z"::: )  (Set (Var "k"))))  ")" )) if (Bool "b" "is"   ($#m1_hidden :::"Integer":::)) ; end; 






:: deftheorem    defines :::"to_power"::: POWER:def 2 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (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 "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k9_prepower :::"#R"::: )  (Set (Var "b"))))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "b")) "is"   ($#m1_hidden :::"Integer":::))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))) "iff" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k"))))  ")" ))  ")" )  ")"   ")" )); 
 definitionlet "a", "b" be   ($#m1_subset_1 :::"Real":::); :: original: :::"to_power"::: redefine func "a" :::"to_power"::: "b" ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POWER:24 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: POWER:25 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: POWER:26 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k3_power :::"to_power"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: POWER:27 (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"))  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:28 (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"))  ($#k3_power :::"to_power"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:29 (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"))  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "b"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:30 (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")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:31 (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")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:32 (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  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: POWER:33 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: POWER:34 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POWER:35 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) ; 
 
theorem :: POWER:36 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 
theorem :: POWER:37 (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 "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c"))))) ; 
 
theorem :: POWER:38 (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 "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c"))))) ; 
 
theorem :: POWER:39 (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 (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "c"))  ($#k3_power :::"to_power"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "c"))  ($#k3_power :::"to_power"::: )  (Set (Var "b"))))) ; 
 
theorem :: POWER:40 (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 (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "c"))  ($#k3_power :::"to_power"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "c"))  ($#k3_power :::"to_power"::: )  (Set (Var "b"))))) ; 
 registrationlet "a" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); 
identify ; 
end; 
theorem :: POWER:41 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: POWER:42 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k3_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POWER:43 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k4_prepower :::"#Z"::: )  (Set (Var "k")))))) ; 
 
theorem :: POWER:44 (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"))  ($#k3_power :::"to_power"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k6_prepower :::"#Q"::: )  (Set (Var "p")))))) ; 
 
theorem :: POWER:45 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_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 "a"))  ($#k3_power :::"to_power"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k1_power :::"-root"::: )  (Set (Var "a")))))) ; 
 
theorem :: POWER:46 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: POWER:47 (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 "k")) "is"   ($#v1_abian :::"even"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "k")))))) ; 
 
theorem :: POWER:48 (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 "k")) "is"   ($#v1_abian :::"odd"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "k")) ")" ))))) ; 
 
theorem :: POWER:49 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"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")) ")" )  ($#k3_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: POWER:50 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "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_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "d"))))) ; 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume that  
(Bool (Set (Const "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 and  
(Bool (Set (Const "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))
 and  
(Bool (Set (Const "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func  :::"log":::  "(" "a" "," "b" ")"  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: POWER:def 3 (Bool (Set "a"  ($#k3_power :::"to_power"::: )  it)  ($#r1_hidden :::"="::: )  "b"); end; 







:: deftheorem    defines :::"log"::: POWER:def 3 :  (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"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#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   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool (Set (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))); 
 definitionlet "a", "b" be   ($#m1_subset_1 :::"Real":::); :: original: :::"log"::: redefine func  :::"log":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POWER:51 (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"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POWER:52 (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"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: POWER:53 (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 "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" ))) ; 
 
theorem :: POWER:54 (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 "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "b"))  ($#k13_complex1 :::"/"::: )  (Set (Var "c")) ")" ) ")" ))) ; 
 
theorem :: POWER:55 (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 "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set  "(" (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )))) ; 
 
theorem :: POWER:56 (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 "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k5_power :::"log"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" )))) ; 
 
theorem :: POWER:57 (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 :::">"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: POWER:58 (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 "a"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_power :::"log"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: POWER:59 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 definitionfunc  :::"number_e":::  ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: POWER:def 4 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s"))))); end; 




:: deftheorem    defines :::"number_e"::: POWER:def 4 :  (Bool  "for" (Set (Var "b1")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_power :::"number_e"::: )  )) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k4_power :::"to_power"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))))  ")" )); 
 definition:: original: :::"number_e"::: redefine func  :::"number_e":::  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POWER:60 (Bool (Set (Num 2)  ($#k4_power :::"to_power"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 4)) ; 
 
theorem :: POWER:61 (Bool (Set (Num 2)  ($#k4_power :::"to_power"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Num 8)) ; 
 
theorem :: POWER:62 (Bool (Set (Num 2)  ($#k4_power :::"to_power"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 16)) ; 
 
theorem :: POWER:63 (Bool (Set (Num 2)  ($#k4_power :::"to_power"::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Num 32)) ; 
 
theorem :: POWER:64 (Bool (Set (Num 2)  ($#k4_power :::"to_power"::: )  (Num 6))  ($#r1_hidden :::"="::: )  (Num 64)) ;