:: SERIES_4 semantic presentation begin Lm1: for a, b being real number holds ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) ) proof let a, b be real number ; ::_thesis: ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) ) A1: (a + b) |^ (1 + 1) = ((a + b) |^ 1) * (a + b) by NEWTON:6 .= (a + b) * (a + b) by NEWTON:5 .= ((a * a) + (a * b)) + ((a * b) + (b * b)) .= ((a * a) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1 .= ((a |^ 2) + (a * b)) + ((a * b) + (b |^ 2)) by WSIERP_1:1 .= ((a |^ 2) + (2 * (a * b))) + (b |^ 2) ; 2 |^ 2 = 2 * 2 by WSIERP_1:1 .= 4 ; hence ( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) ) by A1; ::_thesis: verum end; Lm2: for n being Element of NAT holds (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2 proof let n be Element of NAT ; ::_thesis: (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2 (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ (1 + 1) = ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 1) * (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) by NEWTON:6 .= (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) * (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) by NEWTON:5 .= ((((1 / 2) |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + (((1 / 2) |^ (n + 1)) * (2 |^ (n + 1)))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) .= ((((1 / 2) * (1 / 2)) |^ (n + 1)) + (((1 / 2) |^ (n + 1)) * (2 |^ (n + 1)))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 |^ (n + 1)) * ((1 / 2) |^ (n + 1))) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 * (1 / 2)) |^ (n + 1)) + ((2 |^ (n + 1)) * (2 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 2) * 1) / 2) |^ (n + 1)) + (((1 / 2) * 2) |^ (n + 1))) + (((2 * (1 / 2)) |^ (n + 1)) + ((2 * 2) |^ (n + 1))) by NEWTON:7 .= (((1 / 4) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (4 |^ (n + 1))) by NEWTON:10 .= (((1 / 4) |^ (n + 1)) + 1) + (1 + (4 |^ (n + 1))) by NEWTON:10 .= (((1 / 4) |^ (n + 1)) + 2) + (4 |^ (n + 1)) ; hence (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2 ; ::_thesis: verum end; Lm3: for n being Element of NAT holds (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2 proof let n be Element of NAT ; ::_thesis: (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2 (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ (1 + 1) = ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 1) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) by NEWTON:6 .= (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) * (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) by NEWTON:5 .= ((((1 / 3) |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) .= ((((1 / 3) * (1 / 3)) |^ (n + 1)) + (((1 / 3) |^ (n + 1)) * (3 |^ (n + 1)))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 |^ (n + 1)) * ((1 / 3) |^ (n + 1))) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 |^ (n + 1)) * (3 |^ (n + 1)))) by NEWTON:7 .= (((((1 / 3) * 1) / 3) |^ (n + 1)) + (((1 / 3) * 3) |^ (n + 1))) + (((3 * (1 / 3)) |^ (n + 1)) + ((3 * 3) |^ (n + 1))) by NEWTON:7 .= (((1 / 9) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + (9 |^ (n + 1))) by NEWTON:10 .= (((1 / 9) |^ (n + 1)) + 1) + (1 + (9 |^ (n + 1))) by NEWTON:10 .= (((1 / 9) |^ (n + 1)) + 2) + (9 |^ (n + 1)) ; hence (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2 ; ::_thesis: verum end; Lm4: for a, b being real number holds (a - b) * (a + b) = (a |^ 2) - (b |^ 2) proof let a, b be real number ; ::_thesis: (a - b) * (a + b) = (a |^ 2) - (b |^ 2) (a - b) * (a + b) = (a * a) - (b * b) .= (a |^ 2) - (b * b) by WSIERP_1:1 .= (a |^ 2) - (b |^ 2) by WSIERP_1:1 ; hence (a - b) * (a + b) = (a |^ 2) - (b |^ 2) ; ::_thesis: verum end; Lm5: for a, b being real number holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) proof let a, b be real number ; ::_thesis: (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) (a - b) |^ (1 + 1) = ((a - b) |^ 1) * (a - b) by NEWTON:6 .= (a - b) * (a - b) by NEWTON:5 .= ((a * a) - (a * b)) - ((a * b) - (b * b)) .= ((a * a) - (a * b)) - ((a * b) - (b |^ 2)) by WSIERP_1:1 .= ((a |^ 2) - (a * b)) - ((a * b) - (b |^ 2)) by WSIERP_1:1 .= ((a |^ 2) - (2 * (a * b))) + (b |^ 2) ; hence (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) ; ::_thesis: verum end; Lm6: for n being Element of NAT for a being real number st a <> 1 holds ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) proof let n be Element of NAT ; ::_thesis: for a being real number st a <> 1 holds ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) let a be real number ; ::_thesis: ( a <> 1 implies ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) ) assume a <> 1 ; ::_thesis: ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) then A1: 1 - a <> 0 ; then ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) * (1 - a)))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by XCMPLX_1:91 .= ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - (((1 - a) * (n * (a |^ (n + 1)))) / ((1 - a) |^ 2))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by WSIERP_1:1 .= ((((a - (a * (a |^ n))) - ((n * (a |^ (n + 1))) - ((n * (a |^ (n + 1))) * a))) / ((1 - a) |^ 2)) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) by XCMPLX_1:120 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * 1) .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * 1)) by A1, XCMPLX_1:60 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) / (1 - a)) * ((1 - a) / (1 - a)))) by A1, XCMPLX_1:60 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) * (1 - a)) / ((1 - a) * (1 - a)))) by XCMPLX_1:76 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 - a) |^ 1) * (1 - a)) / ((1 - a) * (1 - a)))) by NEWTON:5 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - a) |^ (1 + 1)) / ((1 - a) * (1 - a)))) by NEWTON:6 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) * (1 - a)))) by Lm5 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((((1 |^ 2) - ((2 * 1) * a)) + (a |^ 2)) / ((1 - a) |^ 2))) by WSIERP_1:1 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + (((n * (a |^ (n + 1))) + (a |^ (n + 1))) * (((1 - (2 * a)) + (a |^ 2)) / ((1 - a) |^ 2))) by NEWTON:10 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) / ((1 - a) |^ 2)) + ((((n * (a |^ (n + 1))) + (a |^ (n + 1))) * ((1 - (2 * a)) + (a |^ 2))) / ((1 - a) |^ 2)) by XCMPLX_1:74 .= ((((a - (a * (a |^ n))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) + (((((n * (a |^ (n + 1))) * 1) - (((n * (a |^ (n + 1))) * 2) * a)) + ((n * (a |^ (n + 1))) * (a |^ 2))) + ((((a |^ (n + 1)) * 1) - (((a |^ (n + 1)) * 2) * a)) + ((a |^ (n + 1)) * (a |^ 2))))) / ((1 - a) |^ 2) by XCMPLX_1:62 .= ((((a - (a |^ (n + 1))) - (n * (a |^ (n + 1)))) + ((a * n) * (a |^ (n + 1)))) + ((((n * (a |^ (n + 1))) - (((n * (a |^ (n + 1))) * 2) * a)) + ((n * (a |^ (n + 1))) * (a |^ 2))) + (((a |^ (n + 1)) - (((a |^ (n + 1)) * 2) * a)) + ((a |^ (n + 1)) * (a |^ 2))))) / ((1 - a) |^ 2) by NEWTON:6 .= ((a - ((a |^ (n + 1)) * a)) - (((n + 1) * (a |^ (n + 1))) * (a - (a |^ 2)))) / ((1 - a) |^ 2) .= ((a - ((a |^ (n + 1)) * a)) - (((n + 1) * (a |^ (n + 1))) * (a - (a * a)))) / ((1 - a) |^ 2) by WSIERP_1:1 .= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) |^ 2)) by XCMPLX_1:120 .= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - (((((n + 1) * (a |^ (n + 1))) * a) * (1 - a)) / ((1 - a) * (1 - a))) by WSIERP_1:1 .= ((a - ((a |^ (n + 1)) * a)) / ((1 - a) |^ 2)) - ((((((n + 1) * (a |^ (n + 1))) * a) / (1 - a)) * (1 - a)) / (1 - a)) by XCMPLX_1:83 .= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * ((a |^ (n + 1)) * a)) / (1 - a)) by A1, XCMPLX_1:87 .= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ ((n + 1) + 1))) / (1 - a)) by NEWTON:6 .= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) ; hence ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) ; ::_thesis: verum end; Lm7: for n being Element of NAT holds 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1)) proof let n be Element of NAT ; ::_thesis: 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1)) (n + 1) + 1 > n + 1 by NAT_1:13; then 2 -Root (n + 2) > 2 -Root (n + 1) by PREPOWER:28; then (2 -Root (n + 2)) - (2 -Root (n + 1)) > (2 -Root (n + 1)) - (2 -Root (n + 1)) by XREAL_1:9; then (1 / ((2 -Root (n + 2)) + (2 -Root (n + 1)))) * 1 = (1 * ((2 -Root (n + 2)) - (2 -Root (n + 1)))) / (((2 -Root (n + 2)) - (2 -Root (n + 1))) * ((2 -Root (n + 2)) + (2 -Root (n + 1)))) by XCMPLX_1:91 .= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / (((2 -Root (n + 2)) |^ 2) - ((2 -Root (n + 1)) |^ 2)) by Lm4 .= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - ((2 -Root (n + 1)) |^ 2)) by PREPOWER:19 .= ((2 -Root (n + 2)) - (2 -Root (n + 1))) / ((n + 2) - (n + 1)) by PREPOWER:19 .= (2 -Root (n + 2)) - (2 -Root (n + 1)) ; hence 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1)) ; ::_thesis: verum end; theorem Th1: :: SERIES_4:1 for a, b, c being real number holds ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c) proof let a, b, c be real number ; ::_thesis: ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c) ((a + b) + c) |^ (1 + 1) = (((a + b) + c) |^ 1) * ((a + b) + c) by NEWTON:6 .= ((a + b) + c) * ((a + b) + c) by NEWTON:5 .= ((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b * b)) + (b * c))) + (((a * c) + (c * b)) + (c * c)) .= ((((a * a) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c)) by WSIERP_1:1 .= ((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c * c)) by WSIERP_1:1 .= ((((a |^ 2) + (a * b)) + (a * c)) + (((a * b) + (b |^ 2)) + (b * c))) + (((a * c) + (c * b)) + (c |^ 2)) by WSIERP_1:1 .= (((((a |^ 2) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2) ; hence ((a + b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c) ; ::_thesis: verum end; theorem Th2: :: SERIES_4:2 for a, b being real number holds (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) proof let a, b be real number ; ::_thesis: (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) (a + b) |^ (2 + 1) = ((a + b) |^ 2) * (a + b) by NEWTON:6 .= (((a |^ 2) + ((2 * a) * b)) + (b |^ 2)) * (a + b) by Lm1 .= ((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + ((b |^ 2) * b)) .= ((((a |^ 2) * a) + ((a |^ 2) * b)) + ((((2 * a) * b) * a) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ (2 + 1))) by NEWTON:6 .= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6 .= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * ((a |^ 1) * a)) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:5 .= (((a |^ 3) + ((a |^ 2) * b)) + (((2 * (a |^ (1 + 1))) * b) + (((2 * a) * b) * b))) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6 .= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + (((b |^ 2) * a) + (b |^ 3)) .= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:5 .= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + (((b |^ 2) * a) + (b |^ 3)) by NEWTON:6 .= (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) ; hence (a + b) |^ 3 = (((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3) ; ::_thesis: verum end; theorem :: SERIES_4:3 for a, b, c being real number holds ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c) proof let a, b, c be real number ; ::_thesis: ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c) ((a - b) + c) |^ (1 + 1) = (((a - b) + c) |^ 1) * ((a - b) + c) by NEWTON:6 .= ((a - b) + c) * ((a - b) + c) by NEWTON:5 .= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b * b)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) .= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1 .= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1 .= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c |^ 2)) by WSIERP_1:1 .= (((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)) + (b |^ 2) ; hence ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c) ; ::_thesis: verum end; theorem :: SERIES_4:4 for a, b, c being real number holds ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c) proof let a, b, c be real number ; ::_thesis: ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c) ((a - b) - c) |^ (1 + 1) = (((a - b) - c) |^ 1) * ((a - b) - c) by NEWTON:6 .= ((a - b) - c) * ((a - b) - c) by NEWTON:5 .= ((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b * b)) - (b * c))) - (((a * c) - (c * b)) - (c * c)) .= ((((a * a) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c)) by WSIERP_1:1 .= ((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c * c)) by WSIERP_1:1 .= ((((a |^ 2) - (a * b)) - (a * c)) - (((a * b) - (b |^ 2)) - (b * c))) - (((a * c) - (c * b)) - (c |^ 2)) by WSIERP_1:1 .= (((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)) + (b |^ 2) ; hence ((a - b) - c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c) ; ::_thesis: verum end; theorem :: SERIES_4:5 for a, b being real number holds (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) proof let a, b be real number ; ::_thesis: (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) (a - b) |^ (2 + 1) = ((a - b) |^ 2) * (a - b) by NEWTON:6 .= (((a |^ 2) - ((2 * a) * b)) + (b |^ 2)) * (a - b) by Lm5 .= ((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - ((b |^ 2) * b)) .= ((((a |^ 2) * a) - ((a |^ 2) * b)) - ((((2 * a) * b) * a) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ (2 + 1))) by NEWTON:6 .= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:6 .= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * ((a |^ 1) * a)) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:5 .= (((a |^ 3) - ((a |^ 2) * b)) - (((2 * (a |^ (1 + 1))) * b) - (((2 * a) * b) * b))) + (((b |^ 2) * a) - (b |^ 3)) by NEWTON:6 .= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3) .= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * ((b |^ 1) * b)) * a)) + ((b |^ 2) * a)) - (b |^ 3) by NEWTON:5 .= ((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((2 * (b |^ (1 + 1))) * a)) + ((b |^ 2) * a)) - (b |^ 3) by NEWTON:6 .= (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) ; hence (a - b) |^ 3 = (((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3) ; ::_thesis: verum end; theorem :: SERIES_4:6 for a, b being real number holds (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) proof let a, b be real number ; ::_thesis: (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) (a + b) |^ (3 + 1) = ((a + b) |^ 3) * (a + b) by NEWTON:6 .= ((((a |^ 3) + ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) + (b |^ 3)) * (a + b) by Th2 .= (((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + ((b |^ 3) * b)) .= (((((a |^ 3) * a) + ((a |^ 3) * b)) + ((((3 * (a |^ 2)) * b) * a) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ (3 + 1))) by NEWTON:6 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * ((a |^ 2) * a)) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ (2 + 1))) * b) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * ((b |^ 1) * b)))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:5 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ (1 + 1))))) + ((((3 * (b |^ 2)) * a) * a) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a * a)) + (((3 * (b |^ 2)) * a) * b))) + (((b |^ 3) * a) + (b |^ 4)) .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * ((a |^ 1) * a)) + (((3 * (b |^ 2)) * b) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:5 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ (1 + 1))) + ((3 * ((b |^ 2) * b)) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6 .= ((((a |^ 4) + ((a |^ 3) * b)) + (((3 * (a |^ 3)) * b) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ 2)) + ((3 * (b |^ (2 + 1))) * a))) + (((b |^ 3) * a) + (b |^ 4)) by NEWTON:6 .= ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) ; hence (a + b) |^ 4 = ((((a |^ 4) + ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) + ((4 * (b |^ 3)) * a)) + (b |^ 4) ; ::_thesis: verum end; theorem :: SERIES_4:7 for a, b, c, d being real number holds (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) proof let a, b, c, d be real number ; ::_thesis: (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) (((a + b) + c) + d) |^ (1 + 1) = ((((a + b) + c) + d) |^ 1) * (((a + b) + c) + d) by NEWTON:6 .= (((a + b) + c) + d) * (((a + b) + c) + d) by NEWTON:5 .= ((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b * b)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) .= ((((((a * a) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1 .= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c * c)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1 .= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d * d)) by WSIERP_1:1 .= ((((((a |^ 2) + (a * b)) + (a * c)) + (a * d)) + ((((a * b) + (b |^ 2)) + (b * c)) + (b * d))) + ((((a * c) + (c * b)) + (c |^ 2)) + (c * d))) + ((((a * d) + (d * b)) + (d * c)) + (d |^ 2)) by WSIERP_1:1 .= ((((((a |^ 2) + (c |^ 2)) + (b |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) ; hence (((a + b) + c) + d) |^ 2 = ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d) ; ::_thesis: verum end; theorem :: SERIES_4:8 for a, b, c being real number holds ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) proof let a, b, c be real number ; ::_thesis: ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) ((a + b) + c) |^ (2 + 1) = (((a + b) + c) |^ 2) * ((a + b) + c) by NEWTON:6 .= ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)) * ((a + b) + c) by Th1 .= ((((((((a |^ 2) * a) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)) .= (((((((a |^ (2 + 1)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + ((b |^ 2) * b)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)) by NEWTON:6 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ (2 + 1))) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + ((c |^ 2) * c))) + (((((2 * a) * b) * a) + (((2 * a) * b) * b)) + (((2 * a) * b) * c))) + (((((2 * a) * c) * a) + (((2 * a) * c) * b)) + (((2 * a) * c) * c))) + (((((2 * b) * c) * a) + (((2 * b) * c) * b)) + (((2 * b) * c) * c)) by NEWTON:6 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * ((a |^ 1) * a)) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:5 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ (1 + 1))) * b) + ((2 * a) * (b * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * ((b |^ 1) * b))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:5 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ (1 + 1)))) + (((2 * a) * b) * c))) + ((((2 * (a * a)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by NEWTON:6 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c * c)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by WSIERP_1:1 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c * c))) by WSIERP_1:1 .= (((((((a |^ 3) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + ((((b |^ 2) * a) + (b |^ 3)) + ((b |^ 2) * c))) + ((((c |^ 2) * a) + ((c |^ 2) * b)) + (c |^ 3))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b * b)) * c)) + ((2 * b) * (c |^ 2))) by WSIERP_1:1 .= (((((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + ((a |^ 2) * b)) + ((a |^ 2) * c)) + (((b |^ 2) * a) + ((b |^ 2) * c))) + (((c |^ 2) * a) + ((c |^ 2) * b))) + ((((2 * (a |^ 2)) * b) + ((2 * a) * (b |^ 2))) + (((2 * a) * b) * c))) + ((((2 * (a |^ 2)) * c) + (((2 * a) * c) * b)) + ((2 * a) * (c |^ 2)))) + (((((2 * b) * c) * a) + ((2 * (b |^ 2)) * c)) + ((2 * (c |^ 2)) * b)) by WSIERP_1:1 .= ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) ; hence ((a + b) + c) |^ 3 = ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c) ; ::_thesis: verum end; theorem :: SERIES_4:9 for n being Element of NAT for a being real number st a <> 0 holds (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 proof let n be Element of NAT ; ::_thesis: for a being real number st a <> 0 holds (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 let a be real number ; ::_thesis: ( a <> 0 implies (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ) assume A1: a <> 0 ; ::_thesis: (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ (1 + 1) = ((((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 1) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) by NEWTON:6 .= (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) * (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) by NEWTON:5 .= ((((1 / a) |^ (n + 1)) * ((1 / a) |^ (n + 1))) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))) .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) |^ (n + 1)) * (a |^ (n + 1)))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a |^ (n + 1)) * ((1 / a) |^ (n + 1))) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a |^ (n + 1)) * (a |^ (n + 1)))) by NEWTON:7 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (((1 / a) * a) |^ (n + 1))) + (((a * (1 / a)) |^ (n + 1)) + ((a * a) |^ (n + 1))) by NEWTON:7 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((((1 / a) * a) |^ (n + 1)) + ((a * a) |^ (n + 1))) by A1, XCMPLX_1:106 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (1 |^ (n + 1))) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1))) by A1, XCMPLX_1:106 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + ((1 |^ (n + 1)) + ((a * a) |^ (n + 1))) by NEWTON:10 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + 1) + (1 + ((a * a) |^ (n + 1))) by NEWTON:10 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + ((a * a) |^ (n + 1))) + 2 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + ((a |^ 2) |^ (n + 1))) + 2 by WSIERP_1:1 .= ((((1 / a) * (1 / a)) |^ (n + 1)) + (a |^ (2 * (n + 1)))) + 2 by NEWTON:9 .= ((((1 / a) |^ 2) |^ (n + 1)) + (a |^ ((2 * n) + 2))) + 2 by WSIERP_1:1 .= (((1 / a) |^ (2 * (n + 1))) + (a |^ ((2 * n) + 2))) + 2 by NEWTON:9 .= (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ; hence (((1 / a) |^ (n + 1)) + (a |^ (n + 1))) |^ 2 = (((1 / a) |^ ((2 * n) + 2)) + (a |^ ((2 * n) + 2))) + 2 ; ::_thesis: verum end; theorem :: SERIES_4:10 for n being Element of NAT for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) proof let n be Element of NAT ; ::_thesis: for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) holds (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . n = a |^ n ) implies (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (1 - (a |^ (\$1 + 1))) / (1 - a); assume a <> 1 ; ::_thesis: ( ex n being Element of NAT st not s . n = a |^ n or (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ) then A1: 1 - a <> 0 ; assume A2: for n being Element of NAT holds s . n = a |^ n ; ::_thesis: (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; ::_thesis: S1[n + 1] hence (Partial_Sums s) . (n + 1) = ((1 - (a |^ (n + 1))) / (1 - a)) + (s . (n + 1)) by SERIES_1:def_1 .= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * 1) by A2 .= ((1 - (a |^ (n + 1))) / (1 - a)) + ((a |^ (n + 1)) * ((1 - a) / (1 - a))) by A1, XCMPLX_1:60 .= ((1 - (a |^ (n + 1))) / (1 - a)) + (((a |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74 .= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62 .= ((1 - (a |^ (n + 1))) + ((a |^ (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a) by NEWTON:6 .= (1 - (a |^ ((n + 1) + 1))) / (1 - a) ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= a |^ 0 by A2 .= 1 by NEWTON:4 .= (1 - a) / (1 - a) by A1, XCMPLX_1:60 .= (1 - (a |^ (0 + 1))) / (1 - a) by NEWTON:5 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); hence (Partial_Sums s) . n = (1 - (a |^ (n + 1))) / (1 - a) ; ::_thesis: verum end; theorem :: SERIES_4:11 for a being real number for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) proof let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) let s be Real_Sequence; ::_thesis: ( a <> 1 & a <> 0 & ( for n being Element of NAT holds s . n = (1 / a) |^ n ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ) assume that A1: a <> 1 and A2: a <> 0 ; ::_thesis: ( ex n being Element of NAT st not s . n = (1 / a) |^ n or for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((1 / a) |^ \$1) - a) / (1 - a); assume A3: for n being Element of NAT holds s . n = (1 / a) |^ n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) A4: 1 - a <> 0 by A1; A5: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ; ::_thesis: S1[n + 1] hence (Partial_Sums s) . (n + 1) = ((((1 / a) |^ n) - a) / (1 - a)) + (s . (n + 1)) by SERIES_1:def_1 .= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * 1) by A3 .= ((((1 / a) |^ n) - a) / (1 - a)) + (((1 / a) |^ (n + 1)) * ((1 - a) / (1 - a))) by A4, XCMPLX_1:60 .= ((((1 / a) |^ n) - a) / (1 - a)) + ((((1 / a) |^ (n + 1)) * (1 - a)) / (1 - a)) by XCMPLX_1:74 .= ((((1 / a) |^ n) - a) + ((((1 / a) |^ (n + 1)) * 1) - (((1 / a) |^ (n + 1)) * a))) / (1 - a) by XCMPLX_1:62 .= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ (n + 1)) * a)) / (1 - a) .= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - ((((1 / a) |^ n) * (1 / a)) * a)) / (1 - a) by NEWTON:6 .= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * ((1 / a) * a))) / (1 - a) .= (((((1 / a) |^ n) - a) + ((1 / a) |^ (n + 1))) - (((1 / a) |^ n) * 1)) / (1 - a) by A2, XCMPLX_1:106 .= (((1 / a) |^ (n + 1)) - a) / (1 - a) ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (1 / a) |^ 0 by A3 .= 1 by NEWTON:4 .= (1 - a) / (1 - a) by A4, XCMPLX_1:60 .= (((1 / a) |^ 0) - a) / (1 - a) by NEWTON:4 ; then A6: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5); hence for n being Element of NAT holds (Partial_Sums s) . n = (((1 / a) |^ n) - a) / (1 - a) ; ::_thesis: verum end; theorem :: SERIES_4:12 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) holds (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) holds (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ) implies (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((10 |^ (\$1 + 1)) / 9) - (1 / 9)) + ((\$1 + 1) |^ 2); assume A1: for n being Element of NAT holds s . n = ((10 |^ n) + (2 * n)) + 1 ; ::_thesis: (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (s . (n + 1)) by SERIES_1:def_1 .= ((((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2)) + (((10 |^ (n + 1)) + (2 * (n + 1))) + 1) by A1 .= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((((n + 1) |^ 2) + (2 * n)) + 3) .= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (2 * n)) + 3) by Lm1 .= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((((n |^ 2) + (2 * n)) + 1) + (2 * n)) + 3) by NEWTON:10 .= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + (((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) by Lm1 .= ((((10 |^ (n + 1)) * 10) / 9) - (1 / 9)) + ((n + 2) |^ 2) by Lm1 .= (((10 |^ ((n + 1) + 1)) / 9) - (1 / 9)) + ((n + 2) |^ 2) by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((10 |^ 0) + (2 * 0)) + 1 by A1 .= ((10 / 9) - (1 / 9)) + 1 by NEWTON:4 .= (((10 |^ (0 + 1)) / 9) - (1 / 9)) + 1 by NEWTON:5 .= (((10 |^ (0 + 1)) / 9) - (1 / 9)) + ((0 + 1) |^ 2) by NEWTON:10 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums s) . n = (((10 |^ (n + 1)) / 9) - (1 / 9)) + ((n + 1) |^ 2) ; ::_thesis: verum end; theorem :: SERIES_4:13 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) holds (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) holds (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ) implies (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((\$1 |^ 2) + 1) - ((1 / 2) |^ \$1); assume A1: for n being Element of NAT holds s . n = ((2 * n) - 1) + ((1 / 2) |^ n) ; ::_thesis: (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((n |^ 2) + 1) - ((1 / 2) |^ n)) + (s . (n + 1)) by SERIES_1:def_1 .= (((n |^ 2) + 1) - ((1 / 2) |^ n)) + (((2 * (n + 1)) - 1) + ((1 / 2) |^ (n + 1))) by A1 .= (((((n |^ 2) + 1) - ((1 / 2) |^ n)) + ((1 / 2) |^ (n + 1))) + (2 * (n + 1))) - 1 .= (((((n |^ 2) + 1) - ((1 / 2) |^ n)) + (((1 / 2) |^ n) * (1 / 2))) + (2 * (n + 1))) - 1 by NEWTON:6 .= ((((n |^ 2) + 1) - (((1 / 2) |^ n) * (1 / 2))) + (2 * (n + 1))) - 1 .= ((((n |^ 2) + 1) - ((1 / 2) |^ (n + 1))) + (2 * (n + 1))) - 1 by NEWTON:6 .= ((((n |^ 2) + (2 * n)) + 1) + 1) - ((1 / 2) |^ (n + 1)) .= ((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + 1) - ((1 / 2) |^ (n + 1)) by NEWTON:10 .= (((n + 1) |^ 2) + 1) - ((1 / 2) |^ (n + 1)) by Lm1 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((2 * 0) - 1) + ((1 / 2) |^ 0) by A1 .= (- 1) + 1 by NEWTON:4 .= (1 - 1) + (0 |^ 2) by NEWTON:11 .= (1 - ((1 / 2) |^ 0)) + (0 |^ 2) by NEWTON:4 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums s) . n = ((n |^ 2) + 1) - ((1 / 2) |^ n) ; ::_thesis: verum end; theorem :: SERIES_4:14 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) holds (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) holds (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ) implies (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = 2 - ((2 + \$1) * ((1 / 2) |^ \$1)); assume A1: for n being Element of NAT holds s . n = n * ((1 / 2) |^ n) ; ::_thesis: (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (2 - ((2 + n) * ((1 / 2) |^ n))) + (s . (n + 1)) by SERIES_1:def_1 .= (2 - ((2 + n) * ((1 / 2) |^ n))) + ((n + 1) * ((1 / 2) |^ (n + 1))) by A1 .= (((2 - (2 * ((1 / 2) |^ n))) - (n * ((1 / 2) |^ n))) + (n * ((1 / 2) |^ (n + 1)))) + (1 * ((1 / 2) |^ (n + 1))) .= (((2 - (((4 * 1) / 2) * ((1 / 2) |^ n))) - (n * ((1 / 2) |^ n))) + (n * (((1 / 2) |^ n) * (1 / 2)))) + (1 * ((1 / 2) |^ (n + 1))) by NEWTON:6 .= (((2 - (4 * (((1 / 2) |^ n) * (1 / 2)))) - (n * ((1 / 2) |^ n))) + ((n * ((1 / 2) |^ n)) * (1 / 2))) + (1 * ((1 / 2) |^ (n + 1))) .= (((2 - (4 * ((1 / 2) |^ (n + 1)))) - (n * ((1 / 2) |^ n))) + ((n * ((1 / 2) |^ n)) * (1 / 2))) + (1 * ((1 / 2) |^ (n + 1))) by NEWTON:6 .= (2 - (3 * ((1 / 2) |^ (n + 1)))) - (n * (((1 / 2) |^ n) * (1 / 2))) .= (2 - (3 * ((1 / 2) |^ (n + 1)))) - (n * ((1 / 2) |^ (n + 1))) by NEWTON:6 .= 2 - ((3 + n) * ((1 / 2) |^ (n + 1))) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 * ((1 / 2) |^ 0) by A1 .= 2 - ((2 + 0) * 1) .= 2 - ((2 + 0) * ((1 / 2) |^ 0)) by NEWTON:4 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums s) . n = 2 - ((2 + n) * ((1 / 2) |^ n)) ; ::_thesis: verum end; theorem :: SERIES_4:15 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((- (((1 / 4) |^ \$1) / 3)) + ((4 |^ (\$1 + 1)) / 3)) + (2 * \$1)) + 3; assume A1: for n being Element of NAT holds s . n = (((1 / 2) |^ n) + (2 |^ n)) |^ 2 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + (s . (n + 1)) by SERIES_1:def_1 .= ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + ((((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2) by A1 .= ((((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3) + ((((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2) by Lm2 .= (((((- (((1 / 4) |^ n) / 3)) + ((1 / 4) |^ (n + 1))) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 .= (((((- (((1 / 4) |^ n) / 3)) + (((1 / 4) |^ n) * (1 / 4))) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6 .= ((((- ((((1 / 4) |^ n) * (1 / 4)) / 3)) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 .= ((((- (((1 / 4) |^ (n + 1)) / 3)) + ((4 |^ (n + 1)) / 3)) + (4 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6 .= (((- (((1 / 4) |^ (n + 1)) / 3)) + (((4 |^ (n + 1)) * 4) / 3)) + (2 * (n + 1))) + 3 .= (((- (((1 / 4) |^ (n + 1)) / 3)) + ((4 |^ ((n + 1) + 1)) / 3)) + (2 * (n + 1))) + 3 by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (((1 / 2) |^ 0) + (2 |^ 0)) |^ 2 by A1 .= (1 + (2 |^ 0)) |^ 2 by NEWTON:4 .= (1 + 1) |^ 2 by NEWTON:4 .= (((- (1 / 3)) + (4 / 3)) + (2 * 0)) + 3 by Lm1 .= (((- (((1 / 4) |^ 0) / 3)) + (4 / 3)) + (2 * 0)) + 3 by NEWTON:4 .= (((- (((1 / 4) |^ 0) / 3)) + ((4 |^ (0 + 1)) / 3)) + (2 * 0)) + 3 by NEWTON:5 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 4) |^ n) / 3)) + ((4 |^ (n + 1)) / 3)) + (2 * n)) + 3 ; ::_thesis: verum end; theorem :: SERIES_4:16 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((- (((1 / 9) |^ \$1) / 8)) + ((9 |^ (\$1 + 1)) / 8)) + (2 * \$1)) + 3; assume A1: for n being Element of NAT holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + (s . (n + 1)) by SERIES_1:def_1 .= ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2) by A1 .= ((((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3) + ((((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2) by Lm3 .= (((((- (((1 / 9) |^ n) / 8)) + ((1 / 9) |^ (n + 1))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 .= (((((- (((1 / 9) |^ n) / 8)) + (((1 / 9) |^ n) * (1 / 9))) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6 .= ((((- ((((1 / 9) |^ n) * (1 / 9)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 .= ((((- (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ (n + 1)) / 8)) + (9 |^ (n + 1))) + (2 * (n + 1))) + 3 by NEWTON:6 .= (((- (((1 / 9) |^ (n + 1)) / 8)) + (((9 |^ (n + 1)) * 9) / 8)) + (2 * (n + 1))) + 3 .= (((- (((1 / 9) |^ (n + 1)) / 8)) + ((9 |^ ((n + 1) + 1)) / 8)) + (2 * (n + 1))) + 3 by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (((1 / 3) |^ 0) + (3 |^ 0)) |^ 2 by A1 .= (1 + (3 |^ 0)) |^ 2 by NEWTON:4 .= (1 + 1) |^ 2 by NEWTON:4 .= (((- (1 / 8)) + (9 / 8)) + (2 * 0)) + 3 by Lm1 .= (((- (((1 / 9) |^ 0) / 8)) + (9 / 8)) + (2 * 0)) + 3 by NEWTON:4 .= (((- (((1 / 9) |^ 0) / 8)) + ((9 |^ (0 + 1)) / 8)) + (2 * 0)) + 3 by NEWTON:5 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3 ; ::_thesis: verum end; theorem :: SERIES_4:17 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * (2 |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * (2 |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((\$1 * (2 |^ (\$1 + 1))) - (2 |^ (\$1 + 1))) + 2; assume A1: for n being Element of NAT holds s . n = n * (2 |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + (s . (n + 1)) by SERIES_1:def_1 .= (((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2) + ((n + 1) * (2 |^ (n + 1))) by A1 .= (n * ((2 |^ (n + 1)) * 2)) + 2 .= (n * (2 |^ ((n + 1) + 1))) + 2 by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 * (2 |^ 0) by A1 .= ((0 * (2 |^ (0 + 1))) - 2) + 2 .= ((0 * (2 |^ (0 + 1))) - (2 |^ (0 + 1))) + 2 by NEWTON:5 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = ((n * (2 |^ (n + 1))) - (2 |^ (n + 1))) + 2 ; ::_thesis: verum end; theorem :: SERIES_4:18 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (\$1 * (3 |^ (\$1 + 1))) + 1; assume A1: for n being Element of NAT holds s . n = ((2 * n) + 1) * (3 |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((n * (3 |^ (n + 1))) + 1) + (s . (n + 1)) by SERIES_1:def_1 .= ((n * (3 |^ (n + 1))) + 1) + (((2 * (n + 1)) + 1) * (3 |^ (n + 1))) by A1 .= ((n + 1) * ((3 |^ (n + 1)) * 3)) + 1 .= ((n + 1) * (3 |^ ((n + 1) + 1))) + 1 by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((2 * 0) + 1) * (3 |^ 0) by A1 .= (0 * (3 |^ (0 + 1))) + 1 by NEWTON:4 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = (n * (3 |^ (n + 1))) + 1 ; ::_thesis: verum end; theorem :: SERIES_4:19 for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) proof let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . n = n * (a |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) ) assume that A1: a <> 1 and A2: for n being Element of NAT holds s . n = n * (a |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((a * (1 - (a |^ \$1))) / ((1 - a) |^ 2)) - ((\$1 * (a |^ (\$1 + 1))) / (1 - a)); A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (s . (n + 1)) by SERIES_1:def_1 .= (((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + ((n + 1) * (a |^ (n + 1))) by A2 .= ((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) .= ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a)) by A1, Lm6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 * (a |^ 0) by A2 .= (((1 - 1) * a) / ((1 - a) |^ 2)) - ((0 * (a |^ (0 + 1))) / (1 - a)) .= (((1 - (a |^ 0)) * a) / ((1 - a) |^ 2)) - ((0 * (a |^ (0 + 1))) / (1 - a)) by NEWTON:4 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); hence for n being Element of NAT holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a)) ; ::_thesis: verum end; theorem :: SERIES_4:20 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds (Partial_Sums s) . n = 2 -Root (n + 1) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds (Partial_Sums s) . n = 2 -Root (n + 1) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) implies (Partial_Sums s) . n = 2 -Root (n + 1) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = 2 -Root (\$1 + 1); assume A1: for n being Element of NAT holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ; ::_thesis: (Partial_Sums s) . n = 2 -Root (n + 1) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = 2 -Root (n + 1) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (2 -Root (n + 1)) + (s . (n + 1)) by SERIES_1:def_1 .= (2 -Root (n + 1)) + (1 / ((2 -Root ((n + 1) + 1)) + (2 -Root (n + 1)))) by A1 .= (2 -Root (n + 1)) + ((2 -Root (n + 2)) - (2 -Root (n + 1))) by Lm7 .= 2 -Root (n + 2) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / ((2 -Root (0 + 1)) + (2 -Root 0)) by A1 .= 1 / ((2 -Root (0 + 1)) + 0) by PREPOWER:def_2 .= 1 / 1 by PREPOWER:20 .= 2 -Root (0 + 1) by PREPOWER:20 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums s) . n = 2 -Root (n + 1) ; ::_thesis: verum end; theorem :: SERIES_4:21 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((2 |^ (\$1 + 1)) - ((1 / 2) |^ \$1)) + 1; assume A1: for n being Element of NAT holds s . n = (2 |^ n) + ((1 / 2) |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + (s . (n + 1)) by SERIES_1:def_1 .= (((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1) + ((2 |^ (n + 1)) + ((1 / 2) |^ (n + 1))) by A1 .= ((((- ((1 / 2) |^ n)) + 1) + ((1 / 2) |^ (n + 1))) + (2 |^ (n + 1))) + (2 |^ (n + 1)) .= ((((- ((1 / 2) |^ n)) + 1) + (((1 / 2) |^ n) * (1 / 2))) + (2 |^ (n + 1))) + (2 |^ (n + 1)) by NEWTON:6 .= (((- (((1 / 2) |^ n) * (1 / 2))) + 1) + (2 |^ (n + 1))) + (2 |^ (n + 1)) .= (((- ((1 / 2) |^ (n + 1))) + 1) + (2 |^ (n + 1))) + (2 |^ (n + 1)) by NEWTON:6 .= ((- ((1 / 2) |^ (n + 1))) + 1) + ((2 |^ (n + 1)) * 2) .= ((- ((1 / 2) |^ (n + 1))) + 1) + (2 |^ ((n + 1) + 1)) by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (2 |^ 0) + ((1 / 2) |^ 0) by A1 .= 1 + ((1 / 2) |^ 0) by NEWTON:4 .= (2 - 1) + 1 by NEWTON:4 .= ((2 |^ (0 + 1)) - 1) + 1 by NEWTON:5 .= ((2 |^ (0 + 1)) - ((1 / 2) |^ 0)) + 1 by NEWTON:4 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) - ((1 / 2) |^ n)) + 1 ; ::_thesis: verum end; theorem :: SERIES_4:22 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = ((\$1 + 1) !) - (1 / ((\$1 + 1) !)); assume A1: for n being Element of NAT holds s . n = ((n !) * n) + (n / ((n + 1) !)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) then A2: s . 0 = ((0 !) * 0) + (0 / ((0 + 1) !)) .= 0 ; A3: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A4: (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) ; ::_thesis: S1[n + 1] n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (((n + 1) !) - (1 / ((n + 1) !))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (((n + 1) !) - (1 / ((n + 1) !))) + ((((n + 1) !) * (n + 1)) + ((n + 1) / (((n + 1) + 1) !))) by A1 .= ((((n + 1) !) + (((n + 1) !) * (n + 1))) - (1 / ((n + 1) !))) + ((n + 1) / (((n + 1) + 1) !)) .= ((((n + 1) !) * ((n + 1) + 1)) - ((1 * (n + 2)) / (((n + 1) !) * ((n + 1) + 1)))) + ((n + 1) / ((n + 2) !)) by XCMPLX_1:91 .= ((((n + 1) !) * ((n + 1) + 1)) - ((1 * (n + 2)) / (((n + 1) + 1) !))) + ((n + 1) / ((n + 2) !)) by NEWTON:15 .= (((n + 1) !) * ((n + 1) + 1)) - (((n + 2) / (((n + 1) + 1) !)) - ((n + 1) / ((n + 2) !))) .= (((n + 1) !) * ((n + 1) + 1)) - (((n + 2) - (n + 1)) / ((n + 2) !)) by XCMPLX_1:120 .= (((n + 1) + 1) !) - (1 / (((n + 1) + 1) !)) by NEWTON:15 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1 .= 0 + (s . 1) by A2, SERIES_1:def_1 .= ((1 !) * 1) + (1 / ((1 + 1) !)) by A1 .= ((((1 + 1) !) - 1) + 1) - (1 / ((1 + 1) !)) by NEWTON:13, NEWTON:14 ; then A5: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - (1 / ((n + 1) !)) ; ::_thesis: verum end; theorem :: SERIES_4:23 for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT st n >= 1 holds ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) proof let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT st n >= 1 holds ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT st n >= 1 holds ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = a * (((a / (a - 1)) |^ \$1) - 1); assume a <> 1 ; ::_thesis: ( ex n being Element of NAT st ( n >= 1 & not ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ) or for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ) then A1: a - 1 <> 0 ; assume A2: for n being Element of NAT st n >= 1 holds ( s . n = (a / (a - 1)) |^ n & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) A3: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A4: (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; ::_thesis: S1[n + 1] A5: n + 1 >= 1 by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (a * (((a / (a - 1)) |^ n) - 1)) + (s . (n + 1)) by A4, SERIES_1:def_1 .= ((a * ((a / (a - 1)) |^ n)) - a) + ((a / (a - 1)) |^ (n + 1)) by A2, A5 .= ((a * ((a / (a - 1)) |^ n)) + ((a / (a - 1)) |^ (n + 1))) - a .= ((a * ((a / (a - 1)) |^ n)) + (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a by NEWTON:6 .= (((a / (a - 1)) |^ n) * ((a * 1) + (a / (a - 1)))) - a .= (((a / (a - 1)) |^ n) * ((a * 1) + (a * (1 / (a - 1))))) - a by XCMPLX_1:99 .= (((a / (a - 1)) |^ n) * (a * (1 + (1 / (a - 1))))) - a .= (((a / (a - 1)) |^ n) * (a * (((a - 1) / (a - 1)) + (1 / (a - 1))))) - a by A1, XCMPLX_1:60 .= (((a / (a - 1)) |^ n) * (a * (((a - 1) + 1) / (a - 1)))) - a by XCMPLX_1:62 .= (a * (((a / (a - 1)) |^ n) * (a / (a - 1)))) - a .= (a * ((a / (a - 1)) |^ (n + 1))) - a by NEWTON:6 .= a * (((a / (a - 1)) |^ (n + 1)) - 1) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . (0 + 1) = ((Partial_Sums s) . 0) + (s . (0 + 1)) by SERIES_1:def_1 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= 0 + (s . 1) by A2 .= 0 + ((a / (a - 1)) |^ 1) by A2 .= ((a / (a - 1)) + a) - a by NEWTON:5 .= ((a * (1 / (a - 1))) + (a * 1)) - a by XCMPLX_1:99 .= ((a * (1 / (a - 1))) + (a * ((a - 1) / (a - 1)))) - a by A1, XCMPLX_1:60 .= (a * ((1 / (a - 1)) + ((a - 1) / (a - 1)))) - a .= (a * ((1 + (a - 1)) / (a - 1))) - a by XCMPLX_1:62 .= a * ((a / (a - 1)) - 1) .= a * (((a / (a - 1)) |^ 1) - 1) by NEWTON:5 ; then A6: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A6, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = a * (((a / (a - 1)) |^ n) - 1) ; ::_thesis: verum end; theorem :: SERIES_4:24 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = ((2 |^ \$1) * (((3 * \$1) - 4) / 2)) + 2; assume A1: for n being Element of NAT st n >= 1 holds ( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A3: (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + (s . (n + 1)) by A3, SERIES_1:def_1 .= (((2 |^ n) * (((3 * n) - 4) / 2)) + 2) + ((2 |^ (n + 1)) * (((3 * (n + 1)) - 1) / 4)) by A1, A4 .= (((2 |^ n) * (((3 * n) - 4) / 2)) + ((2 |^ (n + 1)) * (((3 * n) + 2) / 4))) + 2 .= (((2 |^ n) * (((3 * n) - 4) / 2)) + (((2 |^ n) * 2) * (((3 * n) + 2) / 4))) + 2 by NEWTON:6 .= (((2 |^ n) * 2) * (((3 * n) - 1) / 2)) + 2 .= ((2 |^ (n + 1)) * (((3 * (n + 1)) - 4) / 2)) + 2 by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= 0 + (s . 1) by A1 .= (2 |^ 1) * (((3 * 1) - 1) / 4) by A1 .= 2 * (1 / 2) by NEWTON:5 .= (((3 - 4) / 2) * 2) + 2 .= (((3 - 4) / 2) * (2 |^ 1)) + 2 by NEWTON:5 .= (((2 |^ 1) * ((3 * 1) - 4)) / 2) + 2 ; then A5: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2 ; ::_thesis: verum end; theorem :: SERIES_4:25 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) holds (Partial_Product s) . n = 1 / (n + 2) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) holds (Partial_Product s) . n = 1 / (n + 2) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n + 1) / (n + 2) ) implies (Partial_Product s) . n = 1 / (n + 2) ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 = 1 / (\$1 + 2); assume A1: for n being Element of NAT holds s . n = (n + 1) / (n + 2) ; ::_thesis: (Partial_Product s) . n = 1 / (n + 2) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Product s) . n = 1 / (n + 2) ; ::_thesis: S1[n + 1] then (Partial_Product s) . (n + 1) = (1 / (n + 2)) * (s . (n + 1)) by SERIES_3:def_1 .= (1 / (n + 2)) * (((n + 1) + 1) / ((n + 1) + 2)) by A1 .= ((1 / (n + 2)) * (n + 2)) / ((n + 1) + 2) by XCMPLX_1:74 .= 1 / ((n + 1) + 2) by XCMPLX_1:106 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . 0 = s . 0 by SERIES_3:def_1 .= (0 + 1) / (0 + 2) by A1 .= 1 / (0 + 2) ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Product s) . n = 1 / (n + 2) ; ::_thesis: verum end; theorem :: SERIES_4:26 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n + 1) ) holds (Partial_Product s) . n = 1 / ((n + 1) !) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n + 1) ) holds (Partial_Product s) . n = 1 / ((n + 1) !) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / (n + 1) ) implies (Partial_Product s) . n = 1 / ((n + 1) !) ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 = 1 / ((\$1 + 1) !); assume A1: for n being Element of NAT holds s . n = 1 / (n + 1) ; ::_thesis: (Partial_Product s) . n = 1 / ((n + 1) !) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Product s) . n = 1 / ((n + 1) !) ; ::_thesis: S1[n + 1] then (Partial_Product s) . (n + 1) = (1 / ((n + 1) !)) * (s . (n + 1)) by SERIES_3:def_1 .= (1 / ((n + 1) !)) * (1 / ((n + 1) + 1)) by A1 .= ((1 / ((n + 1) !)) * 1) / ((n + 1) + 1) by XCMPLX_1:74 .= 1 / (((n + 1) !) * ((n + 1) + 1)) by XCMPLX_1:78 .= 1 / ((n + 2) !) by NEWTON:15 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . 0 = s . 0 by SERIES_3:def_1 .= 1 / ((0 + 1) !) by A1, NEWTON:13 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Product s) . n = 1 / ((n + 1) !) ; ::_thesis: verum end; theorem :: SERIES_4:27 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = n & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = n ! proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = n & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = n ! ) defpred S1[ Nat] means (Partial_Product s) . \$1 = \$1 ! ; assume A1: for n being Element of NAT st n >= 1 holds ( s . n = n & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = n ! A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A3: (Partial_Product s) . n = n ! ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1 .= (n !) * (n + 1) by A1, A3, A4 .= (n + 1) ! by NEWTON:15 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= 1 * (s . 1) by A1 .= 1 ! by A1, NEWTON:13 ; then A5: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = n ! ; ::_thesis: verum end; theorem :: SERIES_4:28 for a being real number for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = a / n & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = (a |^ n) / (n !) proof let a be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = a / n & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = (a |^ n) / (n !) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = a / n & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = (a |^ n) / (n !) ) defpred S1[ Nat] means (Partial_Product s) . \$1 = (a |^ \$1) / (\$1 !); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = a / n & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = (a |^ n) / (n !) A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A3: (Partial_Product s) . n = (a |^ n) / (n !) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1 .= ((a |^ n) / (n !)) * (a / (n + 1)) by A1, A3, A4 .= ((a |^ n) * a) / ((n !) * (n + 1)) by XCMPLX_1:76 .= (a |^ (n + 1)) / ((n !) * (n + 1)) by NEWTON:6 .= (a |^ (n + 1)) / ((n + 1) !) by NEWTON:15 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= 1 * (s . 1) by A1 .= (1 * a) / 1 by A1 .= (a |^ 1) / (1 !) by NEWTON:5, NEWTON:13 ; then A5: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = (a |^ n) / (n !) ; ::_thesis: verum end; theorem :: SERIES_4:29 for a being real number for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = a & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = a |^ n proof let a be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = a & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = a |^ n let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = a & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = a |^ n ) defpred S1[ Nat] means (Partial_Product s) . \$1 = a |^ \$1; assume A1: for n being Element of NAT st n >= 1 holds ( s . n = a & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = a |^ n A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that n >= 1 and A3: (Partial_Product s) . n = a |^ n ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1 .= (a |^ n) * a by A1, A3, A4 .= a |^ (n + 1) by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= (s . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= 1 * (s . 1) by A1 .= 1 * a by A1 .= a |^ 1 by NEWTON:5 ; then A5: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A5, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Product s) . n = a |^ n ; ::_thesis: verum end; theorem :: SERIES_4:30 for s being Real_Sequence st ( for n being Element of NAT st n >= 2 holds ( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ) holds for n being Element of NAT st n >= 2 holds (Partial_Product s) . n = (n + 1) / (2 * n) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 2 holds ( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ) implies for n being Element of NAT st n >= 2 holds (Partial_Product s) . n = (n + 1) / (2 * n) ) defpred S1[ Nat] means (Partial_Product s) . \$1 = (\$1 + 1) / (2 * \$1); assume A1: for n being Element of NAT st n >= 2 holds ( s . n = 1 - (1 / (n |^ 2)) & s . 0 = 1 & s . 1 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 2 holds (Partial_Product s) . n = (n + 1) / (2 * n) A2: for n being Nat st n >= 2 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 2 & S1[n] implies S1[n + 1] ) assume that A3: n >= 2 and A4: (Partial_Product s) . n = (n + 1) / (2 * n) ; ::_thesis: S1[n + 1] A5: n + 1 > 1 + 1 by A3, NAT_1:13; (n + 1) * (n + 1) <> 0 ; then A6: (n + 1) |^ 2 <> 0 by WSIERP_1:1; n in NAT by ORDINAL1:def_12; then (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by SERIES_3:def_1 .= ((n + 1) / (2 * n)) * (1 - (1 / ((n + 1) |^ 2))) by A1, A4, A5 .= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) / ((n + 1) |^ 2)) - (1 / ((n + 1) |^ 2))) by A6, XCMPLX_1:60 .= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) - 1) / ((n + 1) |^ 2)) by XCMPLX_1:120 .= ((n + 1) / (2 * n)) * ((((n + 1) |^ 2) - (1 |^ 2)) / ((n + 1) |^ 2)) by NEWTON:10 .= ((n + 1) / (2 * n)) * ((((n + 1) - 1) * ((n + 1) + 1)) / ((n + 1) |^ 2)) by Lm4 .= ((n + 1) * (n * (n + 2))) / ((2 * n) * ((n + 1) |^ 2)) by XCMPLX_1:76 .= (((n + 1) * n) * (n + 2)) / ((2 * n) * ((n + 1) * (n + 1))) by WSIERP_1:1 .= (((n + 1) * n) * (n + 2)) / ((n * (n + 1)) * (2 * (n + 1))) .= (((n + 1) * n) / (n * (n + 1))) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:76 .= (((n + 1) / (n + 1)) * (n / n)) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:76 .= (1 * (n / n)) * ((n + 2) / (2 * (n + 1))) by XCMPLX_1:60 .= (1 * 1) * ((n + 2) / (2 * (n + 1))) by A3, XCMPLX_1:60 .= (n + 2) / (2 * (n + 1)) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Product s) . (1 + 1) = ((Partial_Product s) . (1 + 0)) * (s . 2) by SERIES_3:def_1 .= (((Partial_Product s) . 0) * (s . 1)) * (s . 2) by SERIES_3:def_1 .= ((s . 0) * (s . 1)) * (s . 2) by SERIES_3:def_1 .= (1 * (s . 1)) * (s . 2) by A1 .= (1 * 1) * (s . 2) by A1 .= 1 - (1 / 4) by A1, Lm1 .= (2 + 1) / (2 * 2) ; then A7: S1[2] ; for n being Nat st n >= 2 holds S1[n] from NAT_1:sch_8(A7, A2); hence for n being Element of NAT st n >= 2 holds (Partial_Product s) . n = (n + 1) / (2 * n) ; ::_thesis: verum end;