:: SERIES_4 semantic presentation begin theorem :: SERIES_4:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_4:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 3) ")" )))) ; theorem :: SERIES_4:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_4:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_4:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 3) ")" )))) ; theorem :: SERIES_4:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 4) ")" )))) ; theorem :: SERIES_4:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "d")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "d")) ")" )))) ; theorem :: SERIES_4:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (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) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "c")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )))) ; theorem :: SERIES_4:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 2))))) ; theorem :: SERIES_4:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (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 (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" )))))) ; theorem :: SERIES_4:11 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" )))))) ; theorem :: SERIES_4:12 (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 10) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 10) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 9) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 9) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ))))) ; theorem :: SERIES_4:13 (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")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))))) ; theorem :: SERIES_4:14 (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 (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ))))) ; theorem :: SERIES_4:15 (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 "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Num 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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 4) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 3) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 4) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 3) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 3))))) ; theorem :: SERIES_4:16 (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 "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 3) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 3) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Num 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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 9) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 8) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 9) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 8) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 3))))) ; theorem :: SERIES_4:17 (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 (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 2))))) ; theorem :: SERIES_4:18 (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) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 3) ($#k13_newton :::"|^"::: ) (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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 3) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: SERIES_4:19 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (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 (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: SERIES_4:20 (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) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k3_prepower :::"-Root"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k2_prepower :::"-Root"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_prepower :::"-Root"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: SERIES_4:21 (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 "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))))) ; theorem :: SERIES_4:22 (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 "(" (Set (Var "n")) ($#k9_newton :::"!"::: ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ))) ")" )) "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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ))))) ; theorem :: SERIES_4:23 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (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 (Set "(" (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (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_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )))))) ; theorem :: SERIES_4:24 (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 (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 4) ")" ))) & (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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 4) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 2))))) ; theorem :: SERIES_4:25 (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 (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (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_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))))) ; theorem :: SERIES_4:26 (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) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ))))) ; theorem :: SERIES_4:27 (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 (Var "n"))) & (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_hidden :::"="::: ) (Set (Set (Var "n")) ($#k9_newton :::"!"::: ) )))) ; theorem :: SERIES_4:28 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "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 (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "n")))) & (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k9_newton :::"!"::: ) ")" )))))) ; theorem :: SERIES_4:29 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "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 (Var "a"))) & (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_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))))))) ; theorem :: SERIES_4:30 (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 2))) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#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 2))) "holds" (Bool (Set (Set "(" ($#k1_series_3 :::"Partial_Product"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))))) ;