:: SERIES_3  semantic presentation begin  





















registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set  ($#k16_complex1 :::"|."::: ) "x" ($#k16_complex1 :::".|"::: ) ) ->  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; 
theorem :: SERIES_3:1 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "m")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k13_complex1 :::"/"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "y"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: SERIES_3:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: SERIES_3:3 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "b"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) ; 
 
theorem :: SERIES_3:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k4_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: SERIES_3:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k4_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SERIES_3:6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: SERIES_3:7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: SERIES_3:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: SERIES_3:9 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: SERIES_3:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: SERIES_3:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z")) ")" )  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )))) ; 
 
theorem :: SERIES_3:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "c"))))) ; 
 
theorem :: SERIES_3:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 3))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c"))))) ; 
 
theorem :: SERIES_3:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k13_complex1 :::"/"::: )  (Set (Var "c")) ")" )  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "b"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k13_complex1 :::"/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: SERIES_3:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 3)  ($#k1_power :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )))) ; 
 
theorem :: SERIES_3:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 3))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 3)  ($#k1_power :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: SERIES_3:17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 3)))) ; 
 
theorem :: SERIES_3:18 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 4)))) ; 
 
theorem :: SERIES_3:19 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 2)))) ; 
 
theorem :: SERIES_3:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 9))) ; 
 
theorem :: SERIES_3:21 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Num 4)))) ; 
 
theorem :: SERIES_3:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) ; 
 
theorem :: SERIES_3:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 25)  ($#k13_complex1 :::"/"::: )  (Num 4)))) ; 
 
theorem :: SERIES_3:24 (Bool  "for" (Set (Var "x")) "," (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ))) ; 
 
theorem :: SERIES_3:25 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  )))) ; 
 
theorem :: SERIES_3:26 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "y")) ")" )))) ; 
 
theorem :: SERIES_3:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "a")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "b")) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Num 1)  ($#k13_complex1 :::"/"::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: SERIES_3:28 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "y")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k1_newton :::"|^"::: )  (Num 3))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 6)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k3_square_1 :::"^2"::: )  ")" )))) ; 
 
theorem :: SERIES_3:29 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SERIES_3:30 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_power :::"to_power"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k3_power :::"to_power"::: )  (Set (Var "b")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "c"))  ($#k3_power :::"to_power"::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" )  ($#k3_power :::"to_power"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 3) ")" )))) ; 
 
theorem :: SERIES_3:31 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 2) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 2) ")" ) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 2) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: SERIES_3:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:33 (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:34 (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:35 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:36 (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s1"))))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:37 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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  "("  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:38 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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  "("  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:39 (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s2")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: SERIES_3:40 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s2")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: SERIES_3:41 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "s")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:42 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "s")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 definitionlet "s" be   ($#m1_subset_1 :::"Real_Sequence":::); func  :::"Partial_Product"::: "s" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: SERIES_3:def 1 (Bool  "("  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "s"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "s"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Partial_Product"::: SERIES_3:def 1 :  (Bool  "for" (Set (Var "s")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")))) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )  ")" )  ")" )); 
 
theorem :: SERIES_3:43 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:44 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: SERIES_3:45 (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  "("  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))  ")" ))) ; 
 
theorem :: SERIES_3:46 (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 
theorem :: SERIES_3:47 (Bool  "for" (Set (Var "s1")) "," (Set (Var "s2")) "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  "("  (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_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s2")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set  "(" (Set (Var "s1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "s2")) ")" ) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:48 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 2) ")" )))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k4_nat_1 :::"*"::: )  (Set (Var "n")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 4) ")" ) ")" ))))) ; 
 
theorem :: SERIES_3:49 (Bool  "for" (Set (Var "s1")) "," (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  "("  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:50 (Bool  "for" (Set (Var "s1")) "," (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  "("  (Bool (Set (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Num 1)  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s1")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))) ; 
 
theorem :: SERIES_3:51 (Bool  "for" (Set (Var "s3")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s4")) "," (Set (Var "s5")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s3"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s2")))) & (Bool (Set (Var "s4"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s1")))) & (Bool (Set (Var "s5"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s2"))))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s4")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s5")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: SERIES_3:52 (Bool  "for" (Set (Var "s4")) "," (Set (Var "s1")) "," (Set (Var "s5")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "s4"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s1")))) & (Bool (Set (Var "s5"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "s2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "s2")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_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_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k5_square_1 :::"^2"::: )  ))  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s3")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s4")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s5")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: SERIES_3:53 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (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  "("  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1) ")" )))  ")" )  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_series_3 :::"Partial_Product"::: )  (Set (Var "s")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ;