:: SERIES_2 semantic presentation begin theorem :: SERIES_2:1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SERIES_2:2 (Bool "for" (Set (Var "n")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 5) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 10) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 10) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" )) ; theorem :: SERIES_2:3 (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 (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))))) ; theorem :: SERIES_2:4 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_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 "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: SERIES_2:5 (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) ($#k4_nat_1 :::"*"::: ) (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_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2))))) ; theorem :: SERIES_2:6 (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 "(" (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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3))))) ; theorem :: SERIES_2:7 (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")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (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 "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 4))))) ; theorem :: SERIES_2:8 (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")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ))) ")" )) "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 "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 5))))) ; theorem :: SERIES_2:9 (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 (Var "n")) ($#k4_nat_1 :::"*"::: ) (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_hidden :::"="::: ) (Set (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: SERIES_2:10 (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")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 4) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:11 (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 "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))) ")" )) "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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 18) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:12 (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")) ($#k13_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 (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 6))))) ; theorem :: SERIES_2:13 (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 "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_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 "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))))) ; theorem :: SERIES_2:14 (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 "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Num 2))) & (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 (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 3))))) ; theorem :: SERIES_2: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 (Var "n")) ($#k13_newton :::"|^"::: ) (Num 3))) ")" )) "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")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 4))))) ; theorem :: SERIES_2: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"::: ) ) "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 "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Num 3))) & (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 (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))))) ; theorem :: SERIES_2: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")) ($#k13_newton :::"|^"::: ) (Num 4))) ")" )) "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 "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 30))))) ; theorem :: SERIES_2: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 "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 4) ")" ))) ")" )) "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 "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))))) ; theorem :: SERIES_2:19 (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")) ($#k13_newton :::"|^"::: ) (Num 5))) ")" )) "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 "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 12))))) ; theorem :: SERIES_2:20 (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")) ($#k13_newton :::"|^"::: ) (Num 6))) ")" )) "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 "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 6) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 42))))) ; theorem :: SERIES_2: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 (Var "n")) ($#k13_newton :::"|^"::: ) (Num 7))) ")" )) "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 "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 6) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 24))))) ; theorem :: SERIES_2: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 (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_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 "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 5) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 12))))) ; theorem :: SERIES_2:23 (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")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (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 "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 10))))) ; theorem :: SERIES_2: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"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#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 "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 4))))) ; theorem :: SERIES_2:25 (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) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (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 2))) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Num 4) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:26 (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) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (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 :::"="::: ) (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 "n")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: SERIES_2: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 (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#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 :::"="::: ) (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 "n")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: SERIES_2:28 (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) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))) & (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 12) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 4) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:29 (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) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 24) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 6) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2: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"::: ) ) "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) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ")" )) "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 3) ($#k13_complex1 :::"/"::: ) (Num 4) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 2) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:31 (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 2) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))) ")" )) "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 "(" (Num 29) ($#k13_complex1 :::"/"::: ) (Num 36) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 3) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 4) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:32 (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")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ))) ")" )) "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) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 3) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ))))) ; theorem :: SERIES_2: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_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 4) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))) ")" )) "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 "(" (Num 2) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 4) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2: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_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#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"::: ) ) "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 (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:35 (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 3) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set "(" (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"::: ) ) "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 (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 3) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:36 (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 "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 3) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: SERIES_2:37 (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")) ($#k9_newton :::"!"::: ) ")" ) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")))) ")" )) "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 :::"-"::: ) (Num 1))))) ; theorem :: SERIES_2:38 (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")) ($#k13_complex1 :::"/"::: ) (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 (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ))))) ; theorem :: SERIES_2:39 (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 "(" (Set "(" (Set "(" (Set (Var "n")) ($#k13_newton :::"|^"::: ) (Num 2) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k9_newton :::"!"::: ) ")" ))) & (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 "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ))))) ; theorem :: SERIES_2:40 (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")) ($#k4_nat_1 :::"*"::: ) (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#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 (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k13_newton :::"|^"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ($#k9_newton :::"!"::: ) ")" ) ")" ))))) ; theorem :: SERIES_2:41 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "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"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")))) ")" )) "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 "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b"))))))) ; theorem :: SERIES_2:42 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "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"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")))) ")" )) "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")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2)))))) ;