:: SERIES_5 semantic presentation begin theorem :: SERIES_5:1 (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")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 4))) ; theorem :: SERIES_5: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")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 4) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" )))) ; theorem :: SERIES_5:3 (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")))) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_5:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" )))) ; theorem :: SERIES_5:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 2) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" )))) ; theorem :: SERIES_5:8 (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 "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: SERIES_5:9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 2) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2)))) ; theorem :: SERIES_5:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: SERIES_5:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 2) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: SERIES_5:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) ; theorem :: SERIES_5:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "y")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "y")) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (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 "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Num 1))) ; theorem :: SERIES_5:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (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 "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Num 2))) ; theorem :: SERIES_5:17 (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 (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Num 9) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_5:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" )))) ; theorem :: SERIES_5:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d"))))) ; theorem :: SERIES_5:20 (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")) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 3))) ; theorem :: SERIES_5:21 (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 "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 3)))) ; theorem :: SERIES_5:22 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 3))) ; theorem :: SERIES_5:23 (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 "(" (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 (Set "(" (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ))) ; theorem :: SERIES_5:24 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))))) ; theorem :: SERIES_5:25 (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 (Var "y"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "z")))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "z")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SERIES_5:26 (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 (Var "b")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "c")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_5:27 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "d")))) "holds" (Bool (Set (Set (Var "c")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "c")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "d")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "d")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" )))) ; theorem :: SERIES_5:28 (Bool "for" (Set (Var "m")) "," (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:29 (Bool "for" (Set (Var "m")) "," (Set (Var "x")) "," (Set (Var "u")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "m")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "u")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (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"::: ) ")" ) ")" )))) ; theorem :: SERIES_5:30 (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 "(" (Num 9) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))))) ; theorem :: SERIES_5:31 (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 (Set "(" (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" )))) ; theorem :: SERIES_5:32 (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 "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" )))) ; theorem :: SERIES_5:33 (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 "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: SERIES_5:34 (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 ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_5:35 (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 9))) ; theorem :: SERIES_5:36 (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")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Num 17) ($#k13_complex1 :::"/"::: ) (Num 4)))) ; theorem :: SERIES_5:37 (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")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_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 :::">="::: ) (Num 9))) ; theorem :: SERIES_5:38 (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")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 8))) ; theorem :: SERIES_5:39 (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")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "c")) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 64))) ; theorem :: SERIES_5:40 (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_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 (Num 1) ($#k13_complex1 :::"/"::: ) (Num 3)))) ; theorem :: SERIES_5:41 (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 "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k13_complex1 :::"/"::: ) (Num 3)))) ; theorem :: SERIES_5:42 (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 "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_power :::"to_power"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k3_power :::"to_power"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "b")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k3_power :::"to_power"::: ) (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ")" )))) ; theorem :: SERIES_5:43 (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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ))))) ; theorem :: SERIES_5:44 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 3))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))))) ; theorem :: SERIES_5:45 (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 "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ; theorem :: SERIES_5:46 (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")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_5:47 (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 (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" )) "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 (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: SERIES_5:48 (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 (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) "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 (Num 2) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: SERIES_5:49 (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 (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Num 2)))) ; theorem :: SERIES_5:50 (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 "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: SERIES_5:51 (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 (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")))))) ; theorem :: SERIES_5:52 (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "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 "s1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) "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 "s1")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: SERIES_5:53 (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "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 "s1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )) "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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s1")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k5_square_1 :::"^2"::: ) )))) ; theorem :: SERIES_5:54 (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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (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 "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 6) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" ))))) ; theorem :: SERIES_5:55 (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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (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 "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set "(" (Num 2) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" ))))) ; theorem :: SERIES_5:56 (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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) "holds" (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 "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))))) ; theorem :: SERIES_5:57 (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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) "holds" (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 "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))))) ;