:: SERIES_2 semantic presentation begin theorem Th1: :: SERIES_2:1 for n being Element of NAT holds abs ((- 1) |^ n) = 1 proof let n be Element of NAT ; ::_thesis: abs ((- 1) |^ n) = 1 percases ( n is even or n is odd ) ; supposeA1: n is even ; ::_thesis: abs ((- 1) |^ n) = 1 (- 1) |^ n = (- 1) to_power n by POWER:41 .= 1 to_power n by A1, POWER:47 .= 1 by POWER:26 ; hence abs ((- 1) |^ n) = 1 by ABSVALUE:def_1; ::_thesis: verum end; supposeA2: n is odd ; ::_thesis: abs ((- 1) |^ n) = 1 (- 1) |^ n = (- 1) to_power n by POWER:41 .= - (1 to_power n) by A2, POWER:48 .= - 1 by POWER:26 ; then abs ((- 1) |^ n) = - (- 1) by ABSVALUE:def_1; hence abs ((- 1) |^ n) = 1 ; ::_thesis: verum end; end; end; Lm1: for a being real number holds a |^ 3 = (a * a) * a proof let a be real number ; ::_thesis: a |^ 3 = (a * a) * a a |^ (2 + 1) = (a |^ 2) * a by NEWTON:6; hence a |^ 3 = (a * a) * a by WSIERP_1:1; ::_thesis: verum end; Lm2: for a being real number holds a |^ 3 = (a |^ 2) * a proof let a be real number ; ::_thesis: a |^ 3 = (a |^ 2) * a a |^ (2 + 1) = (a |^ 2) * a by NEWTON:6; hence a |^ 3 = (a |^ 2) * a ; ::_thesis: verum end; Lm3: 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; Lm4: for a being real number holds (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 proof let a be real number ; ::_thesis: (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 (a + 1) |^ 3 = ((a + 1) |^ 2) * (a + 1) by Lm2 .= (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) * (a + 1) by Lm3 .= (((a |^ 2) + (2 * a)) + 1) * (a + 1) by NEWTON:10 .= ((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + (2 * a))) + ((1 * a) + (1 * 1)) .= ((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + ((2 * a) * 1))) + (((1 |^ 2) * a) + 1) by NEWTON:10 .= (((a |^ (2 + 1)) + (a |^ 2)) + (((2 * a) * a) + (2 * a))) + (((1 |^ 2) * a) + 1) by NEWTON:6 .= (((a |^ 3) + (a |^ 2)) + ((2 * (a * a)) + (2 * a))) + ((1 * a) + 1) by NEWTON:10 .= (((a |^ 3) + (a |^ 2)) + ((2 * ((a |^ 1) * a)) + (2 * a))) + (a + 1) by NEWTON:5 .= (((a |^ 3) + (a |^ 2)) + ((2 * (a |^ (1 + 1))) + (2 * a))) + (a + 1) by NEWTON:6 .= ((((a |^ 3) + (a |^ 2)) + (2 * (a |^ 2))) + (2 * a)) + (a + 1) ; hence (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 ; ::_thesis: verum end; Lm5: for n being Element of NAT holds ((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) proof let n be Element of NAT ; ::_thesis: ((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) = ((n + 2) * ((2 * n) + 3)) * (((3 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) + ((3 * n) + 3)) - 1) by Lm3 .= (((n * (2 * n)) + (2 * (2 * n))) + ((n * 3) + (2 * 3))) * ((((3 * (((n |^ 2) + (2 * n)) + (1 |^ 2))) + (3 * n)) + 3) - 1) .= (((n * (2 * n)) + (2 * (2 * n))) + ((n * 3) + (2 * 3))) * ((((3 * (((n |^ 2) + (2 * n)) + 1)) + (3 * n)) + 3) - 1) by NEWTON:10 .= ((((n * n) * 2) + ((2 * 2) * n)) + ((n * 3) + 6)) * (((((((n |^ 2) * 3) + (6 * n)) + 3) + (3 * n)) + 3) - 1) .= (((2 * (n |^ 2)) + (4 * n)) + ((n * 3) + 6)) * ((((((3 * (n |^ 2)) + (6 * n)) + 3) + (3 * n)) + 3) - 1) by WSIERP_1:1 .= (((((2 * ((n |^ 2) * (n |^ 2))) * 3) + (((2 * (n |^ 2)) * n) * 9)) + (10 * (n |^ 2))) + (((((7 * n) * (n |^ 2)) * 3) + (((7 * n) * n) * 9)) + (35 * n))) + ((((6 * 3) * (n |^ 2)) + ((6 * 9) * n)) + 30) .= (((((2 * (n |^ (2 + 2))) * 3) + ((2 * ((n |^ 2) * n)) * 9)) + (10 * (n |^ 2))) + ((((7 * (n * (n |^ 2))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30) by NEWTON:8 .= (((((2 * (n |^ 4)) * 3) + ((2 * (n |^ (2 + 1))) * 9)) + (10 * (n |^ 2))) + ((((7 * (n * (n |^ 2))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30) by NEWTON:6 .= ((((6 * (n |^ 4)) + ((2 * (n |^ 3)) * 9)) + (10 * (n |^ 2))) + ((((7 * (n |^ (2 + 1))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30) by NEWTON:6 ; then A1: ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) = ((((6 * (n |^ 4)) + (18 * (n |^ 3))) + (10 * (n |^ 2))) + ((((7 * (n |^ 3)) * 3) + ((7 * (n |^ 2)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30) by WSIERP_1:1 .= ((((6 * (n |^ 4)) + (39 * (n |^ 3))) + ((73 + 18) * (n |^ 2))) + (89 * n)) + 30 ; ((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = (((2 * (n * n)) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) .= (((2 * ((n |^ 1) * n)) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) by NEWTON:5 .= (((2 * (n |^ (1 + 1))) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) by NEWTON:6 .= (((((2 * ((n |^ 2) * (n |^ 2))) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * ((n |^ 2) * n)) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30) .= (((((2 * (n |^ (2 + 2))) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * ((n |^ 2) * n)) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30) by NEWTON:8 .= (((((2 * (n |^ 4)) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * (n |^ (2 + 1))) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30) by NEWTON:6 .= (((((2 * (n |^ 4)) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * (n |^ 3)) * 3) + ((n |^ 2) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30) by WSIERP_1:1 .= ((((6 * (n |^ 4)) + ((n |^ (2 + 1)) * 3)) + ((6 * (n |^ 3)) + ((n |^ 2) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30) by NEWTON:6 .= ((((6 * (n |^ 4)) + (9 * (n |^ 3))) + (1 * (n |^ 2))) - n) + (((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * 30) by Lm4 .= ((((6 * (n |^ 4)) + (39 * (n |^ 3))) + (91 * (n |^ 2))) + ((90 - 1) * n)) + 30 ; hence ((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) by A1; ::_thesis: verum end; Lm6: for n being real number holds ( (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 ) proof let n be real number ; ::_thesis: ( (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 ) A1: (n + 1) |^ (3 + 1) = ((n + 1) |^ 3) * (n + 1) by NEWTON:6 .= ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (n + 1) by Lm4 .= (((((n |^ 3) * n) + (n |^ 3)) + ((3 * ((n |^ 2) * n)) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1) .= ((((n |^ (3 + 1)) + (n |^ 3)) + ((3 * ((n |^ 2) * n)) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1) by NEWTON:6 .= ((((n |^ (3 + 1)) + (n |^ 3)) + ((3 * (n |^ (2 + 1))) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1) by NEWTON:6 .= ((((n |^ 4) + (n |^ 3)) + ((3 * (n |^ 3)) + (3 * (n |^ 2)))) + ((3 * (n |^ 2)) + (3 * n))) + (n + 1) by WSIERP_1:1 ; (n + 1) |^ (3 + 2) = ((n + 1) |^ 3) * ((n + 1) |^ 2) by NEWTON:8 .= ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * ((n + 1) |^ 2) by Lm4 .= ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) by Lm3 .= ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (((n |^ 2) + (2 * n)) + 1) by NEWTON:10 .= ((((((n |^ 3) * (n |^ 2)) + ((2 * n) * (n |^ 3))) + ((n |^ 3) * 1)) + ((((3 * (n |^ 2)) * (n |^ 2)) + ((2 * n) * (3 * (n |^ 2)))) + ((3 * (n |^ 2)) * 1))) + ((((3 * n) * (n |^ 2)) + ((3 * n) * (2 * n))) + ((3 * n) * 1))) + (((n |^ 2) + (2 * n)) + 1) .= (((((n |^ (3 + 2)) + (2 * (n * (n |^ 3)))) + (n |^ 3)) + (((3 * ((n |^ 2) * (n |^ 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by NEWTON:8 .= (((((n |^ (3 + 2)) + (2 * (n * (n |^ 3)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by NEWTON:8 .= (((((n |^ (3 + 2)) + (2 * (n |^ (3 + 1)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((n |^ (3 + 2)) + (2 * (n |^ (3 + 1)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n |^ (2 + 1))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((n |^ 5) + (2 * (n |^ 4))) + (n |^ 3)) + (((3 * (n |^ 4)) + ((2 * (n |^ 3)) * 3)) + (3 * (n |^ 2)))) + (((3 * (n |^ 3)) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((n |^ 5) + (2 * (n |^ 4))) + (n |^ 3)) + (((3 * (n |^ 4)) + (6 * (n |^ 3))) + (3 * (n |^ 2)))) + (((3 * (n |^ 3)) + ((3 * (n |^ 2)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1) by WSIERP_1:1 ; hence ( (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 ) by A1; ::_thesis: verum end; theorem :: SERIES_2:2 for n being real number holds ( (n + 1) |^ 3 = (((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1 & (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 ) by Lm4, Lm6; Lm7: for n being Element of NAT holds ( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) ) proof let n be Element of NAT ; ::_thesis: ( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) ) n >= 0 by NAT_1:2; then n + 1 > 0 by NAT_1:13; then A1: (n + 1) + 1 > 0 by NAT_1:13; then A2: 1 / ((n + 1) !) = (1 * (n + 2)) / (((n + 1) !) * (n + 2)) by XCMPLX_1:91; (n + 1) / (n + 2) = ((n + 2) - 1) / (n + 2) .= ((n + 2) / (n + 2)) - (1 / (n + 2)) by XCMPLX_1:120 .= 1 - (1 / (n + 2)) by A1, XCMPLX_1:60 ; hence ( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) ) by A2; ::_thesis: verum end; Lm8: for n being Element of NAT holds (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3) proof let n be Element of NAT ; ::_thesis: (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3) n >= 0 by NAT_1:2; then A1: n + 1 > 0 by NAT_1:13; then (n + 1) + 1 > 0 by NAT_1:13; then (n + 2) + 1 > 0 by NAT_1:13; then (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = ((1 * (n + 3)) / ((n + 1) * (n + 3))) - (2 / ((n + 1) * (n + 3))) by XCMPLX_1:91 .= ((n + 3) - 2) / ((n + 1) * (n + 3)) by XCMPLX_1:120 .= ((n + 1) * 1) / ((n + 1) * (n + 3)) .= 1 / (n + 3) by A1, XCMPLX_1:91 ; hence (1 / (n + 1)) - (2 / ((n + 1) * (n + 3))) = 1 / (n + 3) ; ::_thesis: verum end; Lm9: for n being Element of NAT holds (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4) proof let n be Element of NAT ; ::_thesis: (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4) n >= 0 by NAT_1:2; then A1: n + 1 > 0 by NAT_1:13; then (n + 1) + 1 > 0 by NAT_1:13; then (n + 2) + 1 > 0 by NAT_1:13; then (n + 3) + 1 > 0 by NAT_1:13; then (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = ((1 * (n + 4)) / ((n + 1) * (n + 4))) - (3 / ((n + 1) * (n + 4))) by XCMPLX_1:91 .= ((n + 4) - 3) / ((n + 1) * (n + 4)) by XCMPLX_1:120 .= ((n + 1) * 1) / ((n + 1) * (n + 4)) .= 1 / (n + 4) by A1, XCMPLX_1:91 ; hence (1 / (n + 1)) - (3 / ((n + 1) * (n + 4))) = 1 / (n + 4) ; ::_thesis: verum end; Lm10: for n being Element of NAT holds ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2) proof let n be Element of NAT ; ::_thesis: ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2) (n + 1) * (n + 2) = ((n * n) + ((2 * n) + (1 * n))) + 2 .= (((n |^ 1) * n) + ((2 + 1) * n)) + 2 by NEWTON:5 .= ((n |^ (1 + 1)) + ((2 + 1) * n)) + 2 by NEWTON:6 ; hence ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2) ; ::_thesis: verum end; Lm11: for n being Element of NAT holds (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1) proof let n be Element of NAT ; ::_thesis: (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1) (n + 1) * ((4 * ((n + 1) |^ 2)) - 1) = (n + 1) * ((4 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - 1) by Lm3 .= (n + 1) * ((4 * (((n |^ 2) + (2 * n)) + 1)) - 1) by NEWTON:10 .= (((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n * n)) + (8 * n))) + ((3 * n) + (3 * 1)) .= (((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n |^ 2)) + (8 * n))) + ((3 * n) + (3 * 1)) by WSIERP_1:1 .= (((n * (4 * (n |^ 2))) + ((4 * (n |^ 2)) + (8 * (n |^ 2)))) + ((8 * n) + (3 * n))) + 3 ; hence (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1) ; ::_thesis: verum end; Lm12: for n being Element of NAT holds ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1 proof let n be Element of NAT ; ::_thesis: ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1 ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = (((n + 1) |^ 2) * (2 * ((n + 1) |^ 2))) - (((n + 1) |^ 2) * 1) .= ((((n + 1) |^ 2) * ((n + 1) |^ 2)) * 2) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) by Lm3 .= ((((n + 1) |^ 2) * ((n + 1) |^ 2)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:10 .= ((((n + 1) |^ 2) * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) * 2) - (((n |^ 2) + (2 * n)) + 1) by Lm3 .= (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) * (((n |^ 2) + (2 * n)) + (1 |^ 2))) * 2) - (((n |^ 2) + (2 * n)) + 1) by Lm3 .= (((((n |^ 2) + (2 * n)) + (1 |^ 2)) * (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:10 .= (((((n |^ 2) + (2 * n)) + 1) * (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:10 .= (((((((n |^ 2) * (n |^ 2)) + ((2 * n) * (n |^ 2))) + (n |^ 2)) + ((((2 * n) * (n |^ 2)) + (((2 * n) * n) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) .= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ (2 + 1)))) + (n |^ 2)) + (((2 * (n * (n |^ 2))) + ((2 * (n * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ (2 + 1)))) + (n |^ 2)) + (((2 * (n |^ (2 + 1))) + ((2 * (n * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * ((n |^ 1) * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:5 .= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * (n |^ (1 + 1))) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6 .= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * (n |^ 2)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) ; hence ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1 ; ::_thesis: verum end; Lm13: for n being Element of NAT holds (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2 proof let n be Element of NAT ; ::_thesis: (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2 (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (n + 2) * (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (n + 1)) - 1) by Lm3 .= (n + 2) * (((((n |^ 2) + ((2 * n) * 1)) + 1) + (n + 1)) - 1) by NEWTON:10 .= (((((n * (n |^ 2)) + (2 * (n |^ 2))) + (3 * (n * n))) + (6 * n)) + n) + 2 .= (((((n * (n |^ 2)) + (2 * (n |^ 2))) + (3 * (n |^ 2))) + (6 * n)) + n) + 2 by WSIERP_1:1 .= (((((n |^ (2 + 1)) + (2 * (n |^ 2))) + (3 * (n |^ 2))) + (6 * n)) + n) + 2 by NEWTON:6 .= (((n |^ (2 + 1)) + ((2 + 3) * (n |^ 2))) + ((6 + 1) * n)) + 2 ; hence (n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1) = (((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2 ; ::_thesis: verum end; Lm14: for a, b being real number for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b proof let a, b be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (a * n) + b ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((((a * (\$1 + 1)) * \$1) / 2) + (\$1 * b)) + b; assume A1: for n being Element of NAT holds s . n = (a * n) + b ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b 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 = ((((a * (n + 1)) * n) / 2) + (n * b)) + b ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((((a * (n + 1)) * n) / 2) + (n * b)) + b) + (s . (n + 1)) by SERIES_1:def_1 .= (((((a * (n + 1)) * n) / 2) + (n * b)) + b) + ((a * (n + 1)) + b) by A1 .= ((((a * (n + 1)) * (n + 2)) / 2) + ((n + 1) * b)) + b ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((((a * (0 + 1)) * 0) / 2) + (0 * b)) + b by A1 ; 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 = ((((a * (n + 1)) * n) / 2) + (n * b)) + b ; ::_thesis: verum end; theorem :: SERIES_2:3 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n ) holds for n being Element of NAT holds (Partial_Sums s) . n = (n * (n + 1)) / 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n ) implies for n being Element of NAT holds (Partial_Sums s) . n = (n * (n + 1)) / 2 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (\$1 * (\$1 + 1)) / 2; assume A1: for n being Element of NAT holds s . n = n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (n * (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 * (n + 1)) / 2 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((n * (n + 1)) / 2) + (s . (n + 1)) by SERIES_1:def_1 .= ((n * (n + 1)) / 2) + (n + 1) by A1 .= ((n * (n + 1)) + ((n + 1) * 2)) / 2 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (0 * (0 + 1)) / 2 by A1 ; 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 * (n + 1)) / 2 ; ::_thesis: verum end; theorem :: SERIES_2:4 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 2 * n ) holds for n being Element of NAT holds (Partial_Sums s) . n = n * (n + 1) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 2 * n ) implies for n being Element of NAT holds (Partial_Sums s) . n = n * (n + 1) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = \$1 * (\$1 + 1); assume A1: for n being Element of NAT holds s . n = 2 * n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = n * (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 = n * (n + 1) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (n * (n + 1)) + (s . (n + 1)) by SERIES_1:def_1 .= (n * (n + 1)) + (2 * (n + 1)) by A1 .= (n + 2) * (n + 1) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 2 * 0 by A1 .= 0 * (0 + 1) ; 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 * (n + 1) ; ::_thesis: verum end; theorem :: SERIES_2:5 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (2 * n) + 1 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (n + 1) |^ 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (2 * n) + 1 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (n + 1) |^ 2 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (\$1 + 1) |^ 2; assume A1: for n being Element of NAT holds s . n = (2 * n) + 1 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (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 + 1) |^ 2 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((n + 1) |^ 2) + (s . (n + 1)) by SERIES_1:def_1 .= ((n + 1) |^ 2) + ((2 * (n + 1)) + 1) by A1 .= (((n + 1) |^ 2) + (2 * n)) + 3 .= ((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) + (2 * n)) + 3 by Lm3 .= ((((n |^ 2) + (2 * n)) + 1) + (2 * n)) + 3 by NEWTON:10 .= ((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2) by Lm3 .= (n + 2) |^ 2 by Lm3 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (2 * 0) + 1 by A1 .= (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 for n being Element of NAT holds (Partial_Sums s) . n = (n + 1) |^ 2 ; ::_thesis: verum end; theorem :: SERIES_2:6 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * (n + 1) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * (n + 2)) / 3 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * (n + 1) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * (n + 2)) / 3 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((\$1 * (\$1 + 1)) * (\$1 + 2)) / 3; assume A1: for n being Element of NAT holds s . n = n * (n + 1) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * (n + 2)) / 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 = ((n * (n + 1)) * (n + 2)) / 3 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((n * (n + 1)) * (n + 2)) / 3) + (s . (n + 1)) by SERIES_1:def_1 .= (((n * (n + 1)) * (n + 2)) / 3) + ((n + 1) * ((n + 1) + 1)) by A1 .= (((n + 1) * (n + 2)) * (n + 3)) / 3 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((0 * (0 + 1)) * (0 + 2)) / 3 by A1 ; 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 * (n + 1)) * (n + 2)) / 3 ; ::_thesis: verum end; theorem :: SERIES_2:7 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (n + 1)) * (n + 2) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * (n + 3)) / 4 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n * (n + 1)) * (n + 2) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * (n + 3)) / 4 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 * (\$1 + 1)) * (\$1 + 2)) * (\$1 + 3)) / 4; assume A1: for n being Element of NAT holds s . n = (n * (n + 1)) * (n + 2) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * (n + 3)) / 4 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 * (n + 1)) * (n + 2)) * (n + 3)) / 4 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n * (n + 1)) * (n + 2)) * (n + 3)) / 4) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n * (n + 1)) * (n + 2)) * (n + 3)) / 4) + (((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2)) by A1 .= ((((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3)) / 4 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (((0 * (0 + 1)) * (0 + 2)) * (0 + 3)) / 4 by A1 ; 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 * (n + 1)) * (n + 2)) * (n + 3)) / 4 ; ::_thesis: verum end; theorem :: SERIES_2:8 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n * (n + 1)) * (n + 2)) * (n + 3) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((n * (n + 1)) * (n + 2)) * (n + 3) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((((\$1 * (\$1 + 1)) * (\$1 + 2)) * (\$1 + 3)) * (\$1 + 4)) / 5; assume A1: for n being Element of NAT holds s . n = ((n * (n + 1)) * (n + 2)) * (n + 3) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5 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 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5) + (s . (n + 1)) by SERIES_1:def_1 .= (((((n * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5) + ((((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3)) by A1 .= (((((n + 1) * (n + 2)) * (n + 3)) * (n + 4)) * (n + 5)) / 5 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((((0 * (0 + 1)) * (0 + 2)) * (0 + 3)) * (0 + 4)) / 4 by A1 ; 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 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)) / 5 ; ::_thesis: verum end; theorem :: SERIES_2:9 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (n * (n + 1)) ) holds for n being Element of NAT holds (Partial_Sums s) . n = 1 - (1 / (n + 1)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / (n * (n + 1)) ) implies for n being Element of NAT holds (Partial_Sums s) . n = 1 - (1 / (n + 1)) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = 1 - (1 / (\$1 + 1)); assume A1: for n being Element of NAT holds s . n = 1 / (n * (n + 1)) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = 1 - (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] ) A3: n + 1 <> 0 by NAT_1:5; assume (Partial_Sums s) . n = 1 - (1 / (n + 1)) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (1 - (1 / (n + 1))) + (s . (n + 1)) by SERIES_1:def_1 .= (1 - (1 / (n + 1))) + (1 / ((n + 1) * ((n + 1) + 1))) by A1 .= 1 - ((1 / (n + 1)) - (1 / ((n + 1) * (n + 2)))) .= 1 - ((1 * (1 / (n + 1))) - ((1 / (n + 1)) * (1 / (n + 2)))) by XCMPLX_1:102 .= 1 - ((1 / (n + 1)) * (1 - (1 / (n + 2)))) .= 1 - ((1 / (n + 1)) * (((1 * (n + 2)) - 1) / (n + 2))) by Lm7 .= 1 - (((1 / (n + 1)) * (n + 1)) / (n + 2)) by XCMPLX_1:74 .= 1 - (1 / (n + 2)) by A3, XCMPLX_1:87 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / (0 * (0 + 1)) by A1 .= 1 - (1 / 1) by XCMPLX_1:49 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = 1 - (1 / (n + 1)) ; ::_thesis: verum end; theorem :: SERIES_2:10 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2))) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (1 / 4) - (1 / ((2 * (\$1 + 1)) * (\$1 + 2))); assume A1: for n being Element of NAT holds s . n = 1 / ((n * (n + 1)) * (n + 2)) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (1 / 4) - (1 / ((2 * (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_Sums s) . n = (1 / 4) - (1 / ((2 * (n + 1)) * (n + 2))) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))) + (s . (n + 1)) by SERIES_1:def_1 .= ((1 / 4) - (1 / ((2 * (n + 1)) * (n + 2)))) + (1 / (((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2))) by A1 .= (1 / 4) - ((1 / ((2 * (n + 1)) * (n + 2))) - (1 / (((n + 1) * (n + 2)) * (n + 3)))) .= (1 / 4) - ((1 / ((2 * (n + 2)) * (n + 1))) - ((1 * 2) / ((((n + 2) * (n + 1)) * (n + 3)) * 2))) by XCMPLX_1:91 .= (1 / 4) - ((1 / ((2 * (n + 2)) * (n + 1))) - ((1 * 2) / (((n + 2) * 2) * ((n + 1) * (n + 3))))) .= (1 / 4) - ((1 / ((2 * (n + 2)) * (n + 1))) - ((1 / ((n + 2) * 2)) * (2 / ((n + 1) * (n + 3))))) by XCMPLX_1:76 .= (1 / 4) - (((1 / (2 * (n + 2))) * (1 / (n + 1))) - ((1 / (2 * (n + 2))) * (2 / ((n + 1) * (n + 3))))) by XCMPLX_1:102 .= (1 / 4) - ((1 / (2 * (n + 2))) * ((1 / (n + 1)) - (2 / ((n + 1) * (n + 3))))) .= (1 / 4) - ((1 / (2 * (n + 2))) * (1 / (n + 3))) by Lm8 .= (1 / 4) - (1 / ((2 * ((n + 1) + 1)) * ((n + 1) + 2))) by XCMPLX_1:102 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / ((0 * (0 + 1)) * (0 + 2)) by A1 .= (1 / 4) - (1 / ((2 * (0 + 1)) * (0 + 2))) by XCMPLX_1:49 ; 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) - (1 / ((2 * (n + 1)) * (n + 2))) ; ::_thesis: verum end; theorem :: SERIES_2:11 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (((n * (n + 1)) * (n + 2)) * (n + 3)) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / (((n * (n + 1)) * (n + 2)) * (n + 3)) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (1 / 18) - (1 / (((3 * (\$1 + 1)) * (\$1 + 2)) * (\$1 + 3))); assume A1: for n being Element of NAT holds s . n = 1 / (((n * (n + 1)) * (n + 2)) * (n + 3)) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (1 / 18) - (1 / (((3 * (n + 1)) * (n + 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 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (s . (n + 1)) by SERIES_1:def_1 .= ((1 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (1 / ((((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3))) by A1 .= (1 / 18) - ((1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) - (1 / ((((n + 1) * (n + 2)) * (n + 3)) * (n + 4)))) .= (1 / 18) - ((1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) - ((1 * 3) / (((((n + 1) * (n + 2)) * (n + 3)) * (n + 4)) * 3))) by XCMPLX_1:91 .= (1 / 18) - ((1 / (((3 * (n + 2)) * (n + 3)) * (n + 1))) - ((1 * 3) / (((3 * (n + 2)) * (n + 3)) * ((n + 1) * (n + 4))))) .= (1 / 18) - ((1 / (((3 * (n + 2)) * (n + 3)) * (n + 1))) - ((1 / ((3 * (n + 2)) * (n + 3))) * (3 / ((n + 1) * (n + 4))))) by XCMPLX_1:76 .= (1 / 18) - (((1 / ((3 * (n + 2)) * (n + 3))) * (1 / (n + 1))) - ((1 / ((3 * (n + 2)) * (n + 3))) * (3 / ((n + 1) * (n + 4))))) by XCMPLX_1:102 .= (1 / 18) - ((1 / ((3 * (n + 2)) * (n + 3))) * ((1 / (n + 1)) - (3 / ((n + 1) * (n + 4))))) .= (1 / 18) - ((1 / ((3 * (n + 2)) * (n + 3))) * (1 / (n + 4))) by Lm9 .= (1 / 18) - (1 / (((3 * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3))) by XCMPLX_1:102 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / (((0 * (0 + 1)) * (0 + 2)) * (0 + 3)) by A1 .= (1 / 18) - (1 / (((3 * (0 + 1)) * (0 + 2)) * (0 + 3))) by XCMPLX_1:49 ; 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 / 18) - (1 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ; ::_thesis: verum end; theorem :: SERIES_2:12 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 2 ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * ((2 * n) + 1)) / 6 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 2 ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * ((2 * n) + 1)) / 6 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((\$1 * (\$1 + 1)) * ((2 * \$1) + 1)) / 6; assume A1: for n being Element of NAT holds s . n = n |^ 2 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n * (n + 1)) * ((2 * n) + 1)) / 6 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 * (n + 1)) * ((2 * n) + 1)) / 6 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((n * (n + 1)) * ((2 * n) + 1)) / 6) + (s . (n + 1)) by SERIES_1:def_1 .= (((n * (n + 1)) * ((2 * n) + 1)) / 6) + ((n + 1) |^ 2) by A1 .= (((n * (n + 1)) * ((2 * n) + 1)) + (((n + 1) |^ 2) * 6)) / 6 .= ((((n + 1) * n) * ((2 * n) + 1)) + (((n + 1) * (n + 1)) * 6)) / 6 by WSIERP_1:1 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 2 by A1 .= ((0 * (0 + 1)) * ((2 * 0) + 1)) / 6 by NEWTON:11 ; 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 * (n + 1)) * ((2 * n) + 1)) / 6 ; ::_thesis: verum end; theorem :: SERIES_2:13 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 2) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 2) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((((- 1) |^ (\$1 + 1)) * \$1) * (\$1 + 1)) / 2; assume A1: for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 2) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((((- 1) |^ (n + 1)) * n) * (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 = ((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2) + (s . (n + 1)) by SERIES_1:def_1 .= (((((- 1) |^ (n + 1)) * n) * (n + 1)) / 2) + (((- 1) |^ ((n + 1) + 1)) * ((n + 1) |^ 2)) by A1 .= (((((- 1) |^ (n + 1)) * n) * (n + 1)) + ((((- 1) |^ ((n + 1) + 1)) * ((n + 1) |^ 2)) * 2)) / 2 .= (((((- 1) |^ (n + 1)) * n) * (n + 1)) + (((((- 1) |^ (n + 1)) * (- 1)) * ((n + 1) |^ 2)) * 2)) / 2 by NEWTON:6 .= ((((- 1) |^ (n + 1)) * (- 1)) * (((- 1) * (n * (n + 1))) + (((n + 1) |^ 2) * 2))) / 2 .= (((- 1) |^ ((n + 1) + 1)) * (((- 1) * (n * (n + 1))) + (((n + 1) |^ 2) * 2))) / 2 by NEWTON:6 .= (((- 1) |^ (n + 2)) * (((((- 1) * n) * n) + (((- 1) * n) * 1)) + ((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) * 2))) / 2 by Lm3 .= (((- 1) |^ (n + 2)) * (((((- 1) * n) * n) + (((- 1) * n) * 1)) + ((((n |^ 2) + (2 * n)) + 1) * 2))) / 2 by NEWTON:10 .= (((- 1) |^ (n + 2)) * ((((- 1) * (n * n)) + ((- 1) * n)) + (((2 * (n |^ 2)) + ((2 * n) * 2)) + (1 * 2)))) / 2 .= (((- 1) |^ (n + 2)) * ((((- 1) * ((n |^ 1) * n)) + ((- 1) * n)) + (((2 * (n |^ 2)) + ((2 * n) * 2)) + (1 * 2)))) / 2 by NEWTON:5 .= (((- 1) |^ (n + 2)) * ((((- 1) * (n |^ (1 + 1))) + ((- 1) * n)) + (((2 * (n |^ 2)) + ((2 * n) * 2)) + (1 * 2)))) / 2 by NEWTON:6 .= (((- 1) |^ (n + 2)) * (((1 * (n |^ 2)) + (3 * n)) + 2)) / 2 .= (((- 1) |^ (n + 2)) * ((n + 1) * (n + 2))) / 2 by Lm10 .= ((((- 1) |^ (n + 2)) * (n + 1)) * (n + 2)) / 2 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((- 1) |^ (0 + 1)) * (0 |^ 2) by A1 .= ((((- 1) |^ (0 + 1)) * 0) * (0 + 1)) / 2 by NEWTON:11 ; 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) |^ (n + 1)) * n) * (n + 1)) / 2 ; ::_thesis: verum end; theorem :: SERIES_2:14 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 2 & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 2 & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3 ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (\$1 * ((4 * (\$1 |^ 2)) - 1)) / 3; assume A1: for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 2 & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3 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 = (n * ((4 * (n |^ 2)) - 1)) / 3 ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; A5: n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((n * ((4 * (n |^ 2)) - 1)) / 3) + (s . (n + 1)) by A3, SERIES_1:def_1 .= ((n * ((4 * (n |^ 2)) - 1)) / 3) + (((2 * (n + 1)) - 1) |^ 2) by A1, A4 .= ((n * ((4 * (n |^ 2)) - 1)) + ((((2 * n) + 1) |^ 2) * 3)) / 3 .= ((n * ((4 * (n |^ 2)) - 1)) + (((((2 * n) |^ 2) + ((2 * (2 * n)) * 1)) + (1 |^ 2)) * 3)) / 3 by Lm3 .= ((((n * 4) * (n |^ 2)) - (n * 1)) + (((((2 * n) |^ 2) * 3) + ((2 * (2 * n)) * 3)) + ((1 |^ 2) * 3))) / 3 .= (((n * (4 * (n |^ 2))) - n) + (((((2 |^ 2) * (n |^ 2)) * 3) + (((2 * 2) * n) * 3)) + ((1 |^ 2) * 3))) / 3 by NEWTON:7 .= (((n * (4 * (n |^ 2))) - n) + (((((2 |^ 2) * (n |^ 2)) * 3) + ((4 * n) * 3)) + (1 * 3))) / 3 by NEWTON:10 .= (((n * (4 * (n |^ 2))) - n) + (((((2 * 2) * (n |^ 2)) * 3) + (12 * n)) + 3)) / 3 by WSIERP_1:1 .= ((((n * (4 * (n |^ 2))) + ((12 - 1) * n)) + (12 * (n |^ 2))) + 3) / 3 .= ((n + 1) * ((4 * ((n + 1) |^ 2)) - 1)) / 3 by A5, Lm11 ; 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 A1 .= 0 + (((2 * 1) - 1) |^ 2) by A1 .= (1 * ((4 * (1 * 1)) - 1)) / 3 by WSIERP_1:1 .= (1 * ((4 * (1 |^ 2)) - 1)) / 3 by WSIERP_1:1 ; then A6: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A6, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n * ((4 * (n |^ 2)) - 1)) / 3 ; ::_thesis: verum end; theorem :: SERIES_2:15 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 3 ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n |^ 2) * ((n + 1) |^ 2)) / 4 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 3 ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n |^ 2) * ((n + 1) |^ 2)) / 4 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((\$1 |^ 2) * ((\$1 + 1) |^ 2)) / 4; assume A1: for n being Element of NAT holds s . n = n |^ 3 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n |^ 2) * ((n + 1) |^ 2)) / 4 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)) / 4 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((n |^ 2) * ((n + 1) |^ 2)) / 4) + (s . (n + 1)) by SERIES_1:def_1 .= (((n |^ 2) * ((n + 1) |^ 2)) / 4) + ((n + 1) |^ 3) by A1 .= (((n |^ 2) * ((n + 1) |^ 2)) + (((n + 1) |^ 3) * 4)) / 4 .= (((n |^ 2) * ((n + 1) |^ 2)) + ((((n + 1) |^ 2) * (n + 1)) * 4)) / 4 by Lm2 .= (((n + 1) |^ 2) * ((n |^ 2) + (((2 * 2) * n) + 4))) / 4 .= (((n + 1) |^ 2) * ((n + 2) |^ 2)) / 4 by Lm3 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 3 by A1 .= (0 * ((0 + 1) |^ 2)) / 4 by NEWTON:11 .= ((0 |^ 2) * ((0 + 1) |^ 2)) / 4 by NEWTON:11 ; 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)) / 4 ; ::_thesis: verum end; theorem :: SERIES_2:16 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (\$1 |^ 2) * ((2 * (\$1 |^ 2)) - 1); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1) 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 = (n |^ 2) * ((2 * (n |^ 2)) - 1) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; A5: n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((n |^ 2) * ((2 * (n |^ 2)) - 1)) + (s . (n + 1)) by A3, SERIES_1:def_1 .= ((n |^ 2) * ((2 * (n |^ 2)) - 1)) + (((2 * (n + 1)) - 1) |^ 3) by A1, A4 .= ((n |^ 2) * ((2 * (n |^ 2)) - 1)) + (((2 * n) + 1) |^ 3) .= ((n |^ 2) * ((2 * (n |^ 2)) - 1)) + (((((2 * n) |^ 3) + (3 * ((2 * n) |^ 2))) + (3 * (2 * n))) + 1) by Lm4 .= (((((((n |^ 2) * 2) * (n |^ 2)) - (n |^ 2)) + ((2 * n) |^ 3)) + (3 * ((2 * n) |^ 2))) + ((3 * 2) * n)) + 1 .= (((((((n |^ 2) * 2) * (n |^ 2)) - (n |^ 2)) + ((2 * n) |^ 3)) + (3 * ((2 |^ 2) * (n |^ 2)))) + (6 * n)) + 1 by NEWTON:7 .= (((((((n |^ 2) * 2) * (n |^ 2)) - (n |^ 2)) + ((2 |^ 3) * (n |^ 3))) + (3 * ((2 |^ 2) * (n |^ 2)))) + (6 * n)) + 1 by NEWTON:7 .= (((((((n |^ 2) * 2) * (n |^ 2)) - (n |^ 2)) + ((2 |^ 3) * (n |^ 3))) + (3 * ((2 * 2) * (n |^ 2)))) + (6 * n)) + 1 by WSIERP_1:1 .= (((((((n |^ 2) * 2) * (n |^ 2)) - (n |^ 2)) + (((2 * 2) * 2) * (n |^ 3))) + (3 * ((2 * 2) * (n |^ 2)))) + (6 * n)) + 1 by Lm1 .= ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1 .= ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) by A5, Lm12 ; 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 .= (s . 1) + 0 by A1 .= ((2 * 1) - 1) |^ 3 by A1 .= 1 |^ (2 + 1) .= (1 |^ 2) * ((2 * (1 * 1)) - 1) by NEWTON:6 .= (1 |^ 2) * ((2 * (1 |^ 2)) - 1) by WSIERP_1:1 ; then A6: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A6, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1) ; ::_thesis: verum end; theorem :: SERIES_2:17 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 4 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 4 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 * (\$1 + 1)) * ((2 * \$1) + 1)) * (((3 * (\$1 |^ 2)) + (3 * \$1)) - 1)) / 30; assume A1: for n being Element of NAT holds s . n = n |^ 4 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30 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 * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30) + ((n + 1) |^ 4) by A1 .= ((((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ (3 + 1)) * 30)) / 30 .= ((((n * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + ((((n + 1) |^ 3) * (n + 1)) * 30)) / 30 by NEWTON:6 .= ((n + 1) * (((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30))) / 30 .= ((n + 1) * (((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1))) / 30 by Lm5 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 4 by A1 .= (((0 * (0 + 1)) * ((2 * 0) + 1)) * (((3 * (0 |^ 2)) + (3 * 0)) - 1)) / 30 by NEWTON:11 ; 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 * (n + 1)) * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) / 30 ; ::_thesis: verum end; theorem :: SERIES_2:18 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((((- 1) |^ (\$1 + 1)) * \$1) * (\$1 + 1)) * (((\$1 |^ 2) + \$1) - 1)) / 2; assume A1: for n being Element of NAT holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 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 = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2) + (s . (n + 1)) by SERIES_1:def_1 .= ((((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2) + (((- 1) |^ ((n + 1) + 1)) * ((n + 1) |^ 4)) by A1 .= ((((((((- 1) |^ (n + 1)) * (- 1)) * (- 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) + ((((- 1) |^ (n + 2)) * ((n + 1) |^ 4)) * 2)) / 2 .= (((((((- 1) |^ ((n + 1) + 1)) * (- 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) + ((((- 1) |^ (n + 2)) * ((n + 1) |^ 4)) * 2)) / 2 by NEWTON:6 .= (((- 1) |^ (n + 2)) * (((((- 1) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) + (((n + 1) |^ (3 + 1)) * 2))) / 2 .= (((- 1) |^ (n + 2)) * (((((- 1) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) + ((((n + 1) |^ 3) * (n + 1)) * 2))) / 2 by NEWTON:6 .= ((((- 1) |^ (n + 2)) * (n + 1)) * (((- 1) * (((n * (n |^ 2)) + (n * n)) - (n * 1))) + (((n + 1) |^ 3) * 2))) / 2 .= ((((- 1) |^ (n + 2)) * (n + 1)) * (((- 1) * (((n |^ (2 + 1)) + (n * n)) - (n * 1))) + (((n + 1) |^ 3) * 2))) / 2 by NEWTON:6 .= ((((- 1) |^ (n + 2)) * (n + 1)) * (((- 1) * (((n |^ 3) + (n |^ 2)) - n)) + (((n + 1) |^ 3) * 2))) / 2 by WSIERP_1:1 .= ((((- 1) |^ (n + 2)) * (n + 1)) * (((- 1) * (((n |^ 3) + (n |^ 2)) - n)) + (((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * 2))) / 2 by Lm4 .= ((((- 1) |^ (n + 2)) * (n + 1)) * ((((n |^ 3) + (5 * (n |^ 2))) + (7 * n)) + 2)) / 2 .= ((((- 1) |^ (n + 2)) * (n + 1)) * ((n + 2) * ((((n + 1) |^ 2) + (n + 1)) - 1))) / 2 by Lm13 .= (((((- 1) |^ (n + 2)) * (n + 1)) * (n + 2)) * ((((n + 1) |^ 2) + (n + 1)) - 1)) / 2 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((- 1) |^ (0 + 1)) * (0 |^ 4) by A1 .= (((((- 1) |^ (0 + 1)) * 0) * (0 + 1)) * (((0 |^ 2) + 0) - 1)) / 2 by NEWTON:11 ; 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) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2 ; ::_thesis: verum end; Lm15: for n being Element of NAT holds ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1) proof let n be Element of NAT ; ::_thesis: ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1) A1: ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = (((2 * ((n |^ 2) * (n |^ 2))) + (2 * (n * (n |^ 2)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12) .= (((2 * (n |^ (2 + 2))) + (2 * (n * (n |^ 2)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12) by NEWTON:8 .= (((2 * (n |^ (2 + 2))) + (2 * (n |^ (2 + 1)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12) by NEWTON:6 .= (((2 * (n |^ 4)) + (2 * (n |^ 3))) - (n |^ 2)) + (((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * 12) by Lm4 .= ((((((2 * (n |^ 4)) + (2 * (n |^ 3))) - (n |^ 2)) + ((n |^ 3) * 12)) + (36 * (n |^ 2))) + (36 * n)) + 12 ; ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1) = ((n + 2) |^ 2) * (((2 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) + (2 * (n + 1))) - 1) by Lm3 .= (((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) * (((((2 * (n |^ 2)) + ((2 * n) * 2)) + (2 * (1 |^ 2))) + ((2 * n) + (2 * 1))) - 1) by Lm3 .= (((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) * (((((2 * (n |^ 2)) + (4 * n)) + (2 * 1)) + ((2 * n) + 2)) - 1) by NEWTON:10 .= (((n |^ 2) + (4 * n)) + (2 * 2)) * ((((((2 * (n |^ 2)) + (4 * n)) + 2) + (2 * n)) + 2) - 1) by WSIERP_1:1 .= ((((2 * ((n |^ 2) * (n |^ 2))) + (6 * (n * (n |^ 2)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12) .= ((((2 * (n |^ (2 + 2))) + (6 * (n * (n |^ 2)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12) by NEWTON:8 .= ((((2 * (n |^ (2 + 2))) + (6 * (n |^ (2 + 1)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12) by NEWTON:6 .= ((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n * (n |^ 2))) * 2) + ((4 * (n * n)) * 6)) + ((4 * n) * 3))) + (((8 * (n |^ 2)) + (24 * n)) + 12) .= ((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n |^ (2 + 1))) * 2) + (24 * (n * n))) + ((4 * n) * 3))) + (((8 * (n |^ 2)) + (24 * n)) + 12) by NEWTON:6 .= ((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n |^ 3)) * 2) + (24 * (n |^ 2))) + (12 * n))) + (((8 * (n |^ 2)) + (24 * n)) + 12) by WSIERP_1:1 .= ((((((2 * (n |^ 4)) + (14 * (n |^ 3))) + (27 * (n |^ 2))) + (12 * n)) + (8 * (n |^ 2))) + (24 * n)) + 12 ; hence ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1) by A1; ::_thesis: verum end; theorem :: SERIES_2:19 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 5 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 5 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 |^ 2) * ((\$1 + 1) |^ 2)) * (((2 * (\$1 |^ 2)) + (2 * \$1)) - 1)) / 12; assume A1: for n being Element of NAT holds s . n = n |^ 5 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12 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)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12) + ((n + 1) |^ 5) by A1 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ (3 + 2)) * 12)) / 12 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + ((((n + 1) |^ 3) * ((n + 1) |^ 2)) * 12)) / 12 by NEWTON:8 .= (((n + 1) |^ 2) * (((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12))) / 12 .= (((n + 1) |^ 2) * (((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1))) / 12 by Lm15 .= ((((n + 1) |^ 2) * ((n + 2) |^ 2)) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1)) / 12 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 5 by A1 .= ((0 * ((0 + 1) |^ 2)) * (((2 * (0 |^ 2)) + (2 * 0)) - 1)) / 12 by NEWTON:11 .= (((0 |^ 2) * ((0 + 1) |^ 2)) * (((2 * (0 |^ 2)) + (2 * 0)) - 1)) / 12 by NEWTON:11 ; 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)) * (((2 * (n |^ 2)) + (2 * n)) - 1)) / 12 ; ::_thesis: verum end; Lm16: for n being Element of NAT holds ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42 proof let n be Element of NAT ; ::_thesis: ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42 ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((n + 2) * ((2 * n) + 3)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * n)) - 2) .= ((n + 2) * ((2 * n) + 3)) * ((((3 * (((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1)) + (6 * ((n + 1) |^ 3))) - (3 * n)) - 2) by Lm6 .= ((n + 2) * ((2 * n) + 3)) * ((((((((3 * (n |^ 4)) + (12 * (n |^ 3))) + (18 * (n |^ 2))) + (12 * n)) + 3) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (3 * n)) - 2) by Lm4 .= (((2 * (n * n)) + (3 * n)) + ((4 * n) + 6)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (36 * (n |^ 2))) + (27 * n)) + 7) .= (((2 * (n |^ 2)) + (3 * n)) + ((4 * n) + 6)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (36 * (n |^ 2))) + (27 * n)) + 7) by WSIERP_1:1 .= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((27 * (n * (n |^ 2))) * 2) + ((27 * (n * n)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42) .= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((27 * (n |^ (2 + 1))) * 2) + ((27 * (n * n)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42) by NEWTON:6 .= (((((3 * (n |^ 4)) * (((2 * (n |^ 2)) + (7 * n)) + 6)) + ((18 * (n |^ 3)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + (((54 * (n |^ 3)) + ((27 * (n |^ 2)) * 7)) + (162 * n))) + (((14 * (n |^ 2)) + (49 * n)) + 42) by WSIERP_1:1 .= ((((((3 * ((n |^ 4) * (n |^ 2))) * 2) + ((3 * ((n |^ 4) * n)) * 7)) + (18 * (n |^ 4))) + ((((18 * ((n |^ 3) * (n |^ 2))) * 2) + ((18 * ((n |^ 3) * n)) * 7)) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) .= ((((((3 * (n |^ (4 + 2))) * 2) + ((3 * ((n |^ 4) * n)) * 7)) + (18 * (n |^ 4))) + ((((18 * ((n |^ 3) * (n |^ 2))) * 2) + ((18 * ((n |^ 3) * n)) * 7)) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8 .= (((((6 * (n |^ (4 + 2))) + ((3 * (n |^ (4 + 1))) * 7)) + (18 * (n |^ 4))) + (((36 * ((n |^ 3) * (n |^ 2))) + (126 * ((n |^ 3) * n))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6 .= (((((6 * (n |^ (4 + 2))) + (21 * (n |^ (4 + 1)))) + (18 * (n |^ 4))) + (((36 * ((n |^ 3) * (n |^ 2))) + (126 * (n |^ (3 + 1)))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6 .= (((((6 * (n |^ (4 + 2))) + (21 * (n |^ (4 + 1)))) + (18 * (n |^ 4))) + (((36 * (n |^ (3 + 2))) + (126 * (n |^ (3 + 1)))) + (108 * (n |^ 3)))) + ((36 * (n |^ 2)) * (((2 * (n |^ 2)) + (7 * n)) + 6))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8 .= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + ((((36 * ((n |^ 2) * (n |^ 2))) * 2) + ((36 * ((n |^ 2) * n)) * 7)) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) .= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + ((((36 * (n |^ (2 + 2))) * 2) + (252 * ((n |^ 2) * n))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:8 .= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + (((72 * (n |^ (2 + 2))) + (252 * (n |^ (2 + 1)))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) by NEWTON:6 .= (((((6 * (n |^ 6)) + (21 * (n |^ 5))) + (18 * (n |^ 4))) + (((36 * (n |^ 5)) + (126 * (n |^ 4))) + (108 * (n |^ 3)))) + (((72 * (n |^ 4)) + (252 * (n |^ 3))) + (216 * (n |^ 2)))) + ((((54 * (n |^ 3)) + (203 * (n |^ 2))) + (211 * n)) + 42) ; hence ((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1) = ((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42 ; ::_thesis: verum end; theorem :: SERIES_2:20 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 6 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 6 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 * (\$1 + 1)) * ((2 * \$1) + 1)) * ((((3 * (\$1 |^ 4)) + (6 * (\$1 |^ 3))) - (3 * \$1)) + 1)) / 42; assume A1: for n being Element of NAT holds s . n = n |^ 6 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42 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 * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42) + ((n + 1) |^ 6) by A1 .= ((((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) + (((n + 1) |^ (5 + 1)) * 42)) / 42 .= ((((n * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) + ((((n + 1) |^ 5) * (n + 1)) * 42)) / 42 by NEWTON:6 .= ((n + 1) * ((((2 * (n * n)) + n) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) + (((n + 1) |^ 5) * 42))) / 42 .= ((n + 1) * ((((2 * (n |^ 2)) + n) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) + (((n + 1) |^ 5) * 42))) / 42 by WSIERP_1:1 .= ((n + 1) * (((((((3 * ((n |^ 4) * (n |^ 2))) * 2) + (3 * ((n |^ 4) * n))) + (((6 * ((n |^ 3) * (n |^ 2))) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n * (n |^ 2))) * 2) + (3 * (n * n)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 .= ((n + 1) * (((((((3 * (n |^ (4 + 2))) * 2) + (3 * ((n |^ 4) * n))) + (((6 * ((n |^ 3) * (n |^ 2))) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n * (n |^ 2))) * 2) + (3 * (n * n)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by NEWTON:8 .= ((n + 1) * (((((((3 * (n |^ (4 + 2))) * 2) + (3 * ((n |^ 4) * n))) + (((6 * (n |^ (3 + 2))) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n * (n |^ 2))) * 2) + (3 * (n * n)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by NEWTON:8 .= ((n + 1) * (((((((3 * (n |^ (4 + 2))) * 2) + (3 * (n |^ (4 + 1)))) + (((6 * (n |^ (3 + 2))) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n * (n |^ 2))) * 2) + (3 * (n * n)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by NEWTON:6 .= ((n + 1) * (((((((3 * (n |^ (4 + 2))) * 2) + (3 * (n |^ (4 + 1)))) + (((6 * (n |^ (3 + 2))) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n |^ (2 + 1))) * 2) + (3 * (n * n)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by NEWTON:6 .= ((n + 1) * (((((((3 * (n |^ 6)) * 2) + (3 * (n |^ 5))) + (((6 * (n |^ 5)) * 2) + (6 * ((n |^ 3) * n)))) - (((3 * (n |^ 3)) * 2) + (3 * (n |^ 2)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by WSIERP_1:1 .= ((n + 1) * ((((((6 * (n |^ 6)) + (3 * (n |^ 5))) + ((12 * (n |^ 5)) + (6 * (n |^ (3 + 1))))) - ((6 * (n |^ 3)) + (3 * (n |^ 2)))) + ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 5) * 42))) / 42 by NEWTON:6 .= ((n + 1) * (((((((6 * (n |^ 6)) + (6 * (n |^ 4))) + (15 * (n |^ 5))) - (6 * (n |^ 3))) - (1 * (n |^ 2))) + n) + (((((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1) * 42))) / 42 by Lm6 .= ((n + 1) * (((((((6 * (n |^ 6)) + (57 * (n |^ 5))) + (216 * (n |^ 4))) + (414 * (n |^ 3))) + (419 * (n |^ 2))) + (211 * n)) + 42)) / 42 .= ((n + 1) * (((n + 2) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1))) / 42 by Lm16 .= ((((n + 1) * ((n + 1) + 1)) * ((2 * (n + 1)) + 1)) * ((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (3 * (n + 1))) + 1)) / 42 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 6 by A1 .= (((0 * (0 + 1)) * ((2 * 0) + 1)) * ((((3 * (0 |^ 4)) + (6 * (0 |^ 3))) - (3 * 0)) + 1)) / 42 by NEWTON:11 ; 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 * (n + 1)) * ((2 * n) + 1)) * ((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (3 * n)) + 1)) / 42 ; ::_thesis: verum end; Lm17: for n being Element of NAT holds ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24) proof let n be Element of NAT ; ::_thesis: ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24) A1: ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24) = (((((3 * ((n |^ 4) * (n |^ 2))) + (6 * ((n |^ 3) * (n |^ 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24) .= (((((3 * (n |^ (4 + 2))) + (6 * ((n |^ 3) * (n |^ 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24) by NEWTON:8 .= (((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24) by NEWTON:8 .= (((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - (n |^ (2 + 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24) by NEWTON:8 .= (((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - (n |^ (2 + 2))) - (4 * (n |^ (2 + 1)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24) by NEWTON:6 .= (((((3 * (n |^ 6)) + (6 * (n |^ 5))) - (n |^ 4)) - (4 * (n |^ 3))) + ((n |^ 2) * 2)) + (((((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1) * 24) by Lm6 .= ((((((3 * (n |^ 6)) + (30 * (n |^ 5))) + (119 * (n |^ 4))) + (236 * (n |^ 3))) + ((n |^ 2) * 242)) + (120 * n)) + 24 ; ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n + 2) |^ 2) * ((((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * n)) - 4) + 2) .= ((n + 2) |^ 2) * ((((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - (4 * n)) - 4) + 2) by Lm3 .= ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - (4 * n)) - 2) .= ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (((n |^ 2) + (2 * n)) + (1 |^ 2))) - (4 * n)) - 2) by Lm4 .= ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (((n |^ 2) + (2 * n)) + 1)) - (4 * n)) - 2) by NEWTON:10 .= ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * (n |^ 3))) + ((18 - 1) * (n |^ 2))) + (((18 - 2) - 4) * n)) + 3) .= ((n + 2) |^ 2) * (((((3 * (((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1)) + (6 * (n |^ 3))) + (17 * (n |^ 2))) + (12 * n)) + 3) by Lm6 .= (((n |^ 2) + ((2 * n) * 2)) + (2 * 2)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6) by Lm3 .= ((((((3 * ((n |^ 4) * (n |^ 2))) + (18 * ((n |^ 3) * (n |^ 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) .= ((((((3 * (n |^ (4 + 2))) + (18 * ((n |^ 3) * (n |^ 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:8 .= ((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:8 .= ((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * (n |^ (2 + 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:8 .= ((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * (n |^ (2 + 2)))) + (24 * (n |^ (2 + 1)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:6 .= ((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * ((n |^ 4) * n)) + (72 * ((n |^ 3) * n))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) .= ((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * ((n |^ 3) * n))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:6 .= ((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * (n |^ (3 + 1)))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:6 .= ((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * (n |^ (3 + 1)))) + (140 * (n |^ (2 + 1)))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by NEWTON:6 .= ((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ 5)) + (72 * (n |^ 4))) + (140 * (n |^ 3))) + (96 * (n |^ 2))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24) by WSIERP_1:1 .= ((((((3 * (n |^ 6)) + (30 * (n |^ 5))) + (119 * (n |^ 4))) + (236 * (n |^ 3))) + (242 * (n |^ 2))) + (120 * n)) + 24 ; hence ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24) by A1; ::_thesis: verum end; Lm18: for n being Element of NAT holds (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 proof let n be Element of NAT ; ::_thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 A1: ( (- 1) |^ (n + 2) = abs ((- 1) |^ (n + 2)) or - ((- 1) |^ (n + 2)) = abs ((- 1) |^ (n + 2)) ) by ABSVALUE:1; A2: abs ((- 1) |^ (n + 2)) = 1 by Th1; n + 2 >= 2 by NAT_1:11; then n + 2 > 0 by XXREAL_0:2; then 2 |^ (n + 2) > 1 by PEPIN:25; then A3: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 1 + ((- 1) |^ (n + 2)) by XREAL_1:8; percases ( (- 1) |^ (n + 2) = - 1 or (- 1) |^ (n + 2) = 1 ) by A2, A1; suppose (- 1) |^ (n + 2) = - 1 ; ::_thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 hence (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by A3; ::_thesis: verum end; suppose (- 1) |^ (n + 2) = 1 ; ::_thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 hence (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by A3, XXREAL_0:2; ::_thesis: verum end; end; end; Lm19: for n being Element of NAT holds (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 proof let n be Element of NAT ; ::_thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 A1: ( (- 1) |^ (n + 3) = abs ((- 1) |^ (n + 3)) or - ((- 1) |^ (n + 3)) = abs ((- 1) |^ (n + 3)) ) by ABSVALUE:1; A2: abs ((- 1) |^ (n + 3)) = 1 by Th1; n + 3 >= 3 by NAT_1:11; then n + 3 > 0 by XXREAL_0:2; then 2 |^ (n + 3) > 1 by PEPIN:25; then A3: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 1 + ((- 1) |^ (n + 3)) by XREAL_1:8; percases ( (- 1) |^ (n + 3) = - 1 or (- 1) |^ (n + 3) = 1 ) by A2, A1; suppose (- 1) |^ (n + 3) = - 1 ; ::_thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 hence (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 by A3; ::_thesis: verum end; suppose (- 1) |^ (n + 3) = 1 ; ::_thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 hence (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 by A3, XXREAL_0:2; ::_thesis: verum end; end; end; theorem :: SERIES_2:21 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n |^ 7 ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n |^ 7 ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 |^ 2) * ((\$1 + 1) |^ 2)) * (((((3 * (\$1 |^ 4)) + (6 * (\$1 |^ 3))) - (\$1 |^ 2)) - (4 * \$1)) + 2)) / 24; assume A1: for n being Element of NAT holds s . n = n |^ 7 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24 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)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24) + ((n + 1) |^ 7) by A1 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ (5 + 2)) * 24)) / 24 .= ((((n |^ 2) * ((n + 1) |^ 2)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + ((((n + 1) |^ 5) * ((n + 1) |^ 2)) * 24)) / 24 by NEWTON:8 .= (((n + 1) |^ 2) * (((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24))) / 24 .= (((n + 1) |^ 2) * (((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2))) / 24 by Lm17 .= ((((n + 1) |^ 2) * (((n + 1) + 1) |^ 2)) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2)) / 24 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 |^ 7 by A1 .= ((0 * ((0 + 1) |^ 2)) * (((((3 * (0 |^ 4)) + (6 * (0 |^ 3))) - (0 |^ 2)) - (4 * 0)) + 2)) / 24 by NEWTON:11 .= (((0 |^ 2) * ((0 + 1) |^ 2)) * (((((3 * (0 |^ 4)) + (6 * (0 |^ 3))) - (0 |^ 2)) - (4 * 0)) + 2)) / 24 by NEWTON:11 ; 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)) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) / 24 ; ::_thesis: verum end; theorem :: SERIES_2:22 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n * ((n + 1) |^ 2) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n * ((n + 1) |^ 2) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (((\$1 * (\$1 + 1)) * (\$1 + 2)) * ((3 * \$1) + 5)) / 12; assume A1: for n being Element of NAT holds s . n = n * ((n + 1) |^ 2) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12 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 * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = ((((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12) + (s . (n + 1)) by SERIES_1:def_1 .= ((((n * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12) + ((n + 1) * (((n + 1) + 1) |^ 2)) by A1 .= ((n + 1) * (((n * (n + 2)) * ((3 * n) + 5)) + (((n + 2) |^ 2) * 12))) / 12 .= ((n + 1) * (((n * (n + 2)) * ((3 * n) + 5)) + (((n + 2) * (n + 2)) * 12))) / 12 by WSIERP_1:1 .= ((((n + 1) * (n + 2)) * (n + 3)) * ((3 * (n + 1)) + 5)) / 12 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 0 * ((0 + 1) |^ 2) by A1 .= (((0 * (0 + 1)) * (0 + 2)) * ((3 * 0) + 5)) / 12 ; 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 * (n + 1)) * (n + 2)) * ((3 * n) + 5)) / 12 ; ::_thesis: verum end; theorem :: SERIES_2:23 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * ((n + 1) |^ 2)) * (n + 2) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n * ((n + 1) |^ 2)) * (n + 2) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((((\$1 * (\$1 + 1)) * (\$1 + 2)) * (\$1 + 3)) * ((2 * \$1) + 3)) / 10; assume A1: for n being Element of NAT holds s . n = (n * ((n + 1) |^ 2)) * (n + 2) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10 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 * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10) + (s . (n + 1)) by SERIES_1:def_1 .= (((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10) + (((n + 1) * (((n + 1) + 1) |^ 2)) * ((n + 1) + 2)) by A1 .= (((((n * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10) + (((((n + 1) * ((n + 2) * (n + 2))) * (n + 3)) * 10) / 10) by WSIERP_1:1 .= (((((n + 1) * (n + 2)) * (n + 3)) * (n + 4)) * ((2 * (n + 1)) + 3)) / 10 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (0 * ((0 + 1) |^ 2)) * (0 + 2) by A1 .= ((((0 * (0 + 1)) * (0 + 2)) * (0 + 3)) * ((2 * 0) + 3)) / 10 ; 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 * (n + 1)) * (n + 2)) * (n + 3)) * ((2 * n) + 3)) / 10 ; ::_thesis: verum end; theorem :: SERIES_2:24 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (n + 1)) * (2 |^ n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n * (n + 1)) * (2 |^ n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((2 |^ (\$1 + 1)) * (((\$1 |^ 2) - \$1) + 2)) - 4; assume A1: for n being Element of NAT holds s . n = (n * (n + 1)) * (2 |^ n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4 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)) * (((n |^ 2) - n) + 2)) - 4 ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4) + (s . (n + 1)) by SERIES_1:def_1 .= (((2 |^ (n + 1)) * (((n |^ 2) - n) + 2)) - 4) + (((n + 1) * ((n + 1) + 1)) * (2 |^ (n + 1))) by A1 .= ((((2 |^ (n + 1)) * 2) * ((((n |^ 2) - n) + 2) + ((n + 1) * (n + 2)))) / 2) - 4 .= (((2 |^ ((n + 1) + 1)) * ((((n |^ 2) - n) + 2) + ((n + 1) * (n + 2)))) / 2) - 4 by NEWTON:6 .= (((2 |^ (n + 2)) * (((((((n |^ 2) - n) + 2) + (n * n)) + (1 * n)) + (n * 2)) + 2)) / 2) - 4 .= (((2 |^ (n + 2)) * (((((((n |^ 2) - n) + 2) + (n |^ 2)) + (1 * n)) + (n * 2)) + 2)) / 2) - 4 by WSIERP_1:1 .= ((2 |^ (n + 2)) * ((((((n |^ 2) + (2 * n)) + 1) - 1) - n) + 2)) - 4 .= ((2 |^ (n + 2)) * ((((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) - 1) - n) + 2)) - 4 by NEWTON:10 .= ((2 |^ (n + 2)) * (((((n + 1) |^ 2) - 1) - n) + 2)) - 4 by Lm3 .= ((2 |^ (n + 2)) * ((((n + 1) |^ 2) - (1 + n)) + 2)) - 4 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (0 * (0 + 1)) * (2 |^ 0) by A1 .= (2 * 2) - 4 .= ((2 |^ (0 + 1)) * ((0 - 0) + 2)) - 4 by NEWTON:5 .= ((2 |^ (0 + 1)) * (((0 |^ 2) - 0) + 2)) - 4 by NEWTON:11 ; 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)) * (((n |^ 2) - n) + 2)) - 4 ; ::_thesis: verum end; theorem :: SERIES_2:25 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 2 holds (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 2 holds (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = ((3 / 4) - (1 / (2 * \$1))) - (1 / (2 * (\$1 + 1))); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((n - 1) * (n + 1)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 2 holds (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) then A2: s . 1 = 1 / ((1 - 1) * (1 + 1)) .= 0 by XCMPLX_1:49 ; A3: 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 A4: n >= 2 and A5: (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) ; ::_thesis: S1[n + 1] A6: n > 0 by A4, XXREAL_0:2; then A7: n + 1 > 1 by XREAL_1:29; A8: n + 2 >= n by NAT_1:11; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))) + (s . (n + 1)) by A5, SERIES_1:def_1 .= (((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1)))) + (1 / (((n + 1) - 1) * ((n + 1) + 1))) by A1, A7 .= ((3 / 4) - (1 / (2 * (n + 1)))) + ((1 / (n * (n + 2))) - (1 / (2 * n))) .= ((3 / 4) - (1 / (2 * (n + 1)))) + ((1 / (n * (n + 2))) - ((1 / 2) * (1 / n))) by XCMPLX_1:102 .= ((3 / 4) - (1 / (2 * (n + 1)))) + (((1 / n) * (1 / (n + 2))) - ((1 / 2) * (1 / n))) by XCMPLX_1:102 .= ((3 / 4) - (1 / (2 * (n + 1)))) + (((1 / (n + 2)) - (1 / 2)) * (1 / n)) .= ((3 / 4) - (1 / (2 * (n + 1)))) + ((((1 * 2) - (1 * (n + 2))) / ((n + 2) * 2)) * (1 / n)) by A6, A8, XCMPLX_1:130 .= ((3 / 4) - (1 / (2 * (n + 1)))) + (((- n) / n) * (1 / ((n + 2) * 2))) by XCMPLX_1:85 .= ((3 / 4) - (1 / (2 * (n + 1)))) + ((- 1) * (1 / ((n + 2) * 2))) by A6, XCMPLX_1:197 .= ((3 / 4) - (1 / (2 * (n + 1)))) + (- (1 / (2 * ((n + 1) + 1)))) ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . (1 + 1) = ((Partial_Sums s) . (1 + 0)) + (s . 2) by SERIES_1:def_1 .= (((Partial_Sums s) . 0) + (s . 1)) + (s . 2) by SERIES_1:def_1 .= ((s . 0) + (s . 1)) + (s . 2) by SERIES_1:def_1 .= (0 + (s . 1)) + (s . 2) by A1 .= 1 / ((2 - 1) * (2 + 1)) by A1, A2 .= ((3 / 4) - (1 / (2 * 2))) - (1 / (2 * (2 + 1))) ; then A9: S1[2] ; for n being Nat st n >= 2 holds S1[n] from NAT_1:sch_8(A9, A3); hence for n being Element of NAT st n >= 2 holds (Partial_Sums s) . n = ((3 / 4) - (1 / (2 * n))) - (1 / (2 * (n + 1))) ; ::_thesis: verum end; theorem :: SERIES_2:26 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((2 * n) - 1) * ((2 * n) + 1)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((2 * n) + 1) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((2 * n) - 1) * ((2 * n) + 1)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((2 * n) + 1) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = \$1 / ((2 * \$1) + 1); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((2 * n) - 1) * ((2 * n) + 1)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((2 * n) + 1) 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 = n / ((2 * n) + 1) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; (2 * n) + 1 >= 1 by NAT_1:11; then A5: (2 * n) + 1 > 0 by XXREAL_0:2; (2 * n) + 3 >= 3 by NAT_1:11; then A6: (2 * n) + 3 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (n / ((2 * n) + 1)) + (s . (n + 1)) by A3, SERIES_1:def_1 .= (n / ((2 * n) + 1)) + (1 / (((2 * (n + 1)) - 1) * ((2 * (n + 1)) + 1))) by A1, A4 .= (n / ((2 * n) + 1)) + ((1 / ((2 * n) + 1)) * (1 / ((2 * n) + 3))) by XCMPLX_1:102 .= (n * (1 / ((2 * n) + 1))) + ((1 / ((2 * n) + 1)) * (1 / ((2 * n) + 3))) by XCMPLX_1:99 .= (n + (1 / ((2 * n) + 3))) * (1 / ((2 * n) + 1)) .= (((n * ((2 * n) + 3)) + 1) / ((2 * n) + 3)) * (1 / ((2 * n) + 1)) by A6, XCMPLX_1:113 .= (((n + 1) * ((2 * n) + 1)) / ((2 * n) + 3)) * (1 / ((2 * n) + 1)) .= (((2 * n) + 1) * ((n + 1) / ((2 * n) + 3))) * (1 / ((2 * n) + 1)) by XCMPLX_1:74 .= (n + 1) / ((2 * (n + 1)) + 1) by A5, XCMPLX_1:107 ; 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 .= 1 / (((2 * 1) - 1) * ((2 * 1) + 1)) by A1 .= 1 / ((2 * 1) + 1) ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((2 * n) + 1) ; ::_thesis: verum end; theorem :: SERIES_2:27 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((3 * n) - 2) * ((3 * n) + 1)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((3 * n) + 1) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((3 * n) - 2) * ((3 * n) + 1)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((3 * n) + 1) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = \$1 / ((3 * \$1) + 1); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = 1 / (((3 * n) - 2) * ((3 * n) + 1)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((3 * n) + 1) 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 = n / ((3 * n) + 1) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; (3 * n) + 1 >= 1 by NAT_1:11; then A5: (3 * n) + 1 > 0 by XXREAL_0:2; (3 * n) + 4 >= 4 by NAT_1:11; then A6: (3 * n) + 4 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (n / ((3 * n) + 1)) + (s . (n + 1)) by A3, SERIES_1:def_1 .= (n / ((3 * n) + 1)) + (1 / (((3 * (n + 1)) - 2) * ((3 * (n + 1)) + 1))) by A1, A4 .= (n / ((3 * n) + 1)) + ((1 / ((3 * n) + 1)) * (1 / ((3 * n) + 4))) by XCMPLX_1:102 .= (n * (1 / ((3 * n) + 1))) + ((1 / ((3 * n) + 1)) * (1 / ((3 * n) + 4))) by XCMPLX_1:99 .= (n + (1 / ((3 * n) + 4))) * (1 / ((3 * n) + 1)) .= (((n * ((3 * n) + 4)) + 1) / ((3 * n) + 4)) * (1 / ((3 * n) + 1)) by A6, XCMPLX_1:113 .= (((n + 1) * ((3 * n) + 1)) / ((3 * n) + 4)) * (1 / ((3 * n) + 1)) .= (((3 * n) + 1) * ((n + 1) / ((3 * n) + 4))) * (1 / ((3 * n) + 1)) by XCMPLX_1:74 .= (n + 1) / ((3 * (n + 1)) + 1) by A5, XCMPLX_1:107 ; 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 .= 1 / (((3 * 1) - 2) * ((3 * 1) + 1)) by A1 .= 1 / ((3 * 1) + 1) ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = n / ((3 * n) + 1) ; ::_thesis: verum end; theorem :: SERIES_2:28 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((2 * n) - 1) * ((2 * n) + 1)) * ((2 * n) + 3)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((2 * n) - 1) * ((2 * n) + 1)) * ((2 * n) + 3)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (1 / 12) - (1 / ((4 * ((2 * \$1) + 1)) * ((2 * \$1) + 3))); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((2 * n) - 1) * ((2 * n) + 1)) * ((2 * n) + 3)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3))) 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 = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3))) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; (2 * n) + 1 >= 1 by NAT_1:11; then A5: (2 * n) + 1 > 0 by XXREAL_0:2; (2 * n) + 5 >= 5 by NAT_1:11; then A6: (2 * n) + 5 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3)))) + (s . (n + 1)) by A3, SERIES_1:def_1 .= ((1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3)))) + (1 / ((((2 * (n + 1)) - 1) * ((2 * (n + 1)) + 1)) * ((2 * (n + 1)) + 3))) by A1, A4 .= ((1 / 12) - (1 / (4 * (((2 * n) + 1) * ((2 * n) + 3))))) + (1 / ((((2 * n) + 1) * ((2 * n) + 3)) * ((2 * n) + 5))) .= ((1 / 12) - ((1 / 4) * (1 / (((2 * n) + 1) * ((2 * n) + 3))))) + (1 / ((((2 * n) + 1) * ((2 * n) + 3)) * ((2 * n) + 5))) by XCMPLX_1:102 .= ((1 / 12) - ((1 / 4) * (1 / (((2 * n) + 1) * ((2 * n) + 3))))) + ((1 / (((2 * n) + 1) * ((2 * n) + 3))) * (1 / ((2 * n) + 5))) by XCMPLX_1:102 .= (1 / 12) - ((1 / (((2 * n) + 1) * ((2 * n) + 3))) * ((1 / 4) - (1 / ((2 * n) + 5)))) .= (1 / 12) - ((1 / (((2 * n) + 1) * ((2 * n) + 3))) * (((1 * ((2 * n) + 5)) - (1 * 4)) / (4 * ((2 * n) + 5)))) by A6, XCMPLX_1:130 .= (1 / 12) - (((1 / ((2 * n) + 1)) * (1 / ((2 * n) + 3))) * (((2 * n) + 1) / (4 * ((2 * n) + 5)))) by XCMPLX_1:102 .= (1 / 12) - ((((1 / ((2 * n) + 1)) * (1 / ((2 * n) + 3))) * ((2 * n) + 1)) / (4 * ((2 * n) + 5))) by XCMPLX_1:74 .= (1 / 12) - ((1 / ((2 * n) + 3)) / (4 * ((2 * n) + 5))) by A5, XCMPLX_1:109 .= (1 / 12) - (1 / (((2 * n) + 3) * (4 * ((2 * n) + 5)))) by XCMPLX_1:78 .= (1 / 12) - (1 / ((4 * ((2 * (n + 1)) + 1)) * ((2 * (n + 1)) + 3))) ; 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 .= 1 / ((((2 * 1) - 1) * ((2 * 1) + 1)) * ((2 * 1) + 3)) by A1 .= (1 / 12) - (1 / ((4 * ((2 * 1) + 1)) * ((2 * 1) + 3))) ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 12) - (1 / ((4 * ((2 * n) + 1)) * ((2 * n) + 3))) ; ::_thesis: verum end; theorem :: SERIES_2:29 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((3 * n) - 2) * ((3 * n) + 1)) * ((3 * n) + 4)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((3 * n) - 2) * ((3 * n) + 1)) * ((3 * n) + 4)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (1 / 24) - (1 / ((6 * ((3 * \$1) + 1)) * ((3 * \$1) + 4))); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = 1 / ((((3 * n) - 2) * ((3 * n) + 1)) * ((3 * n) + 4)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4))) 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 = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4))) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; (3 * n) + 1 >= 1 by NAT_1:11; then A5: (3 * n) + 1 > 0 by XXREAL_0:2; (3 * n) + 7 >= 7 by NAT_1:11; then A6: (3 * n) + 7 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4)))) + (s . (n + 1)) by A3, SERIES_1:def_1 .= ((1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4)))) + (1 / ((((3 * (n + 1)) - 2) * ((3 * (n + 1)) + 1)) * ((3 * (n + 1)) + 4))) by A1, A4 .= ((1 / 24) - (1 / (6 * (((3 * n) + 1) * ((3 * n) + 4))))) + (1 / ((((3 * n) + 1) * ((3 * n) + 4)) * ((3 * n) + 7))) .= ((1 / 24) - ((1 / 6) * (1 / (((3 * n) + 1) * ((3 * n) + 4))))) + (1 / ((((3 * n) + 1) * ((3 * n) + 4)) * ((3 * n) + 7))) by XCMPLX_1:102 .= ((1 / 24) - ((1 / 6) * (1 / (((3 * n) + 1) * ((3 * n) + 4))))) + ((1 / (((3 * n) + 1) * ((3 * n) + 4))) * (1 / ((3 * n) + 7))) by XCMPLX_1:102 .= (1 / 24) - ((1 / (((3 * n) + 1) * ((3 * n) + 4))) * ((1 / 6) - (1 / ((3 * n) + 7)))) .= (1 / 24) - ((1 / (((3 * n) + 1) * ((3 * n) + 4))) * (((1 * ((3 * n) + 7)) - (1 * 6)) / (6 * ((3 * n) + 7)))) by A6, XCMPLX_1:130 .= (1 / 24) - (((1 / ((3 * n) + 4)) * (1 / ((3 * n) + 1))) * (((3 * n) + 1) / (6 * ((3 * n) + 7)))) by XCMPLX_1:102 .= (1 / 24) - ((((1 / ((3 * n) + 4)) * (1 / ((3 * n) + 1))) * ((3 * n) + 1)) / (6 * ((3 * n) + 7))) by XCMPLX_1:74 .= (1 / 24) - ((1 / ((3 * n) + 4)) / (6 * ((3 * n) + 7))) by A5, XCMPLX_1:109 .= (1 / 24) - (1 / (((3 * n) + 4) * (6 * ((3 * n) + 7)))) by XCMPLX_1:78 .= (1 / 24) - (1 / ((6 * ((3 * (n + 1)) + 1)) * ((3 * (n + 1)) + 4))) ; 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 .= 1 / ((((3 * 1) - 2) * ((3 * 1) + 1)) * ((3 * 1) + 4)) by A1 .= (1 / 24) - (1 / ((6 * ((3 * 1) + 1)) * ((3 * 1) + 4))) ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 24) - (1 / ((6 * ((3 * n) + 1)) * ((3 * n) + 4))) ; ::_thesis: verum end; theorem :: SERIES_2:30 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) - 1) / ((n * (n + 1)) * (n + 2)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) - 1) / ((n * (n + 1)) * (n + 2)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = ((3 / 4) - (2 / (\$1 + 2))) + (1 / ((2 * (\$1 + 1)) * (\$1 + 2))); assume A1: for n being Element of NAT holds s . n = ((2 * n) - 1) / ((n * (n + 1)) * (n + 2)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2))) then A2: s . 0 = ((2 * 0) - 1) / ((0 * (0 + 1)) * (0 + 2)) .= 0 by XCMPLX_1:49 ; 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 = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2))) ; ::_thesis: S1[n + 1] n + 1 >= 1 + 0 by NAT_1:11; then A5: n + 1 > 0 by NAT_1:13; n + 2 >= 2 by NAT_1:11; then n + 2 > 0 by XXREAL_0:2; then A6: (n + 1) * (n + 2) > 0 by A5, XREAL_1:129; n + 3 >= 3 by NAT_1:11; then A7: n + 3 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2)))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2)))) + (((2 * (n + 1)) - 1) / (((n + 1) * ((n + 1) + 1)) * ((n + 1) + 2))) by A1 .= ((3 / 4) - ((2 / (n + 2)) - (1 / (2 * ((n + 1) * (n + 2)))))) + (((2 * n) + 1) / (((n + 1) * (n + 2)) * (n + 3))) .= ((3 / 4) - (((2 * (n + 1)) / ((n + 2) * (n + 1))) - (1 / (2 * ((n + 1) * (n + 2)))))) + (((2 * n) + 1) / (((n + 1) * (n + 2)) * (n + 3))) by A5, XCMPLX_1:91 .= ((3 / 4) - ((((2 * (n + 1)) * 2) / ((2 * (n + 2)) * (n + 1))) - (1 / (2 * ((n + 1) * (n + 2)))))) + (((2 * n) + 1) / (((n + 1) * (n + 2)) * (n + 3))) by XCMPLX_1:91 .= ((3 / 4) - (((4 * (n + 1)) - 1) / (2 * ((n + 2) * (n + 1))))) + (((2 * n) + 1) / (((n + 1) * (n + 2)) * (n + 3))) by XCMPLX_1:120 .= ((3 / 4) - ((((4 * n) + 3) * (n + 3)) / ((2 * ((n + 2) * (n + 1))) * (n + 3)))) + (((2 * n) + 1) / (((n + 1) * (n + 2)) * (n + 3))) by A7, XCMPLX_1:91 .= ((3 / 4) - ((((4 * n) + 3) * (n + 3)) / ((2 * ((n + 2) * (n + 1))) * (n + 3)))) + ((((2 * n) + 1) * 2) / ((((n + 1) * (n + 2)) * (n + 3)) * 2)) by XCMPLX_1:91 .= (3 / 4) - (((((4 * n) + 3) * (n + 3)) / ((2 * ((n + 2) * (n + 1))) * (n + 3))) - ((((2 * n) + 1) * 2) / ((((n + 1) * (n + 2)) * (n + 3)) * 2))) .= (3 / 4) - (((((4 * n) + 3) * (n + 3)) - (((2 * n) + 1) * 2)) / ((2 * ((n + 2) * (n + 1))) * (n + 3))) by XCMPLX_1:120 .= (3 / 4) - ((((4 * (n + 1)) * (n + 2)) - (n + 1)) / ((2 * ((n + 2) * (n + 1))) * (n + 3))) .= (3 / 4) - (((4 * ((n + 1) * (n + 2))) / ((2 * (n + 3)) * ((n + 2) * (n + 1)))) - ((n + 1) / ((2 * ((n + 2) * (n + 1))) * (n + 3)))) by XCMPLX_1:120 .= (3 / 4) - ((4 / (2 * (n + 3))) - ((1 * (n + 1)) / (((2 * (n + 2)) * (n + 3)) * (n + 1)))) by A6, XCMPLX_1:91 .= (3 / 4) - (((2 * 2) / ((n + 3) * 2)) - (1 / ((2 * (n + 2)) * (n + 3)))) by A5, XCMPLX_1:91 .= (3 / 4) - ((2 / ((n + 1) + 2)) - (1 / ((2 * ((n + 1) + 1)) * ((n + 1) + 2)))) by XCMPLX_1:91 ; 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 .= ((2 * 1) - 1) / ((1 * (1 + 1)) * (1 + 2)) by A1, A2 .= ((3 / 4) - (2 / (1 + 2))) + (1 / ((2 * (1 + 1)) * (1 + 2))) ; then A8: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A8, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((3 / 4) - (2 / (n + 2))) + (1 / ((2 * (n + 1)) * (n + 2))) ; ::_thesis: verum end; theorem :: SERIES_2:31 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (((29 / 36) - (1 / (\$1 + 3))) - (3 / ((2 * (\$1 + 2)) * (\$1 + 3)))) - (4 / (((3 * (\$1 + 1)) * (\$1 + 2)) * (\$1 + 3))); assume A1: for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (n + 3)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) then A2: s . 0 = (0 + 2) / ((0 * (0 + 1)) * (0 + 3)) .= 0 by XCMPLX_1:49 ; 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 = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ; ::_thesis: S1[n + 1] n + 4 >= 4 by NAT_1:11; then A5: n + 4 > 0 by XXREAL_0:2; n + 1 >= 1 + 0 by NAT_1:11; then A6: n + 1 > 0 by NAT_1:13; then A7: 2 * (n + 1) > 0 by XREAL_1:129; n + 2 >= 2 by NAT_1:11; then A8: n + 2 > 0 by XXREAL_0:2; then A9: (n + 1) * (n + 2) > 0 by A6, XREAL_1:129; then A10: ((n + 1) * (n + 2)) * 3 > 0 by XREAL_1:129; n + 3 >= 3 by NAT_1:11; then A11: n + 3 > 0 by XXREAL_0:2; then ((n + 1) * (n + 2)) * (n + 3) > 0 by A9, XREAL_1:129; then A12: (((n + 1) * (n + 2)) * (n + 3)) * 6 > 0 by XREAL_1:129; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= ((((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + (((n + 1) + 2) / (((n + 1) * ((n + 1) + 1)) * ((n + 1) + 3))) by A1 .= ((((29 / 36) - ((1 * (n + 2)) / ((n + 3) * (n + 2)))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by A8, XCMPLX_1:91 .= ((((29 / 36) - (((n + 2) * 2) / (((n + 2) * (n + 3)) * 2))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by XCMPLX_1:91 .= (((29 / 36) - ((((n + 2) * 2) / (((n + 2) * (n + 3)) * 2)) + (3 / ((2 * (n + 2)) * (n + 3))))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) .= (((29 / 36) - ((((n + 2) * 2) + 3) / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by XCMPLX_1:62 .= (((29 / 36) - ((((n * 2) + 7) * (n + 1)) / (((2 * (n + 2)) * (n + 3)) * (n + 1)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by A6, XCMPLX_1:91 .= (((29 / 36) - (((((n * 2) + 7) * (n + 1)) * 3) / ((((2 * (n + 2)) * (n + 3)) * (n + 1)) * 3))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by XCMPLX_1:91 .= (((29 / 36) - (((((n * 2) + 7) * (n + 1)) * 3) / ((((2 * (n + 2)) * (n + 3)) * (n + 1)) * 3))) - ((4 * 2) / ((((3 * (n + 1)) * (n + 2)) * (n + 3)) * 2))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by XCMPLX_1:91 .= ((29 / 36) - ((((((n * 2) + 7) * (n + 1)) * 3) / (((6 * (n + 2)) * (n + 3)) * (n + 1))) + (8 / (((6 * (n + 1)) * (n + 2)) * (n + 3))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) .= ((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) / ((((6 * (n + 2)) * (n + 3)) * (n + 1)) * (n + 4))) + (8 / (((6 * (n + 1)) * (n + 2)) * (n + 3))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by A5, XCMPLX_1:91 .= ((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) + ((8 * (n + 4)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by A5, XCMPLX_1:91 .= ((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((n + 3) / (((n + 1) * (n + 2)) * (n + 4))) by XCMPLX_1:62 .= ((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + (((n + 3) * 6) / ((((n + 1) * (n + 2)) * (n + 4)) * 6)) by XCMPLX_1:91 .= ((29 / 36) - (((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((((n + 3) * 6) * (n + 3)) / (((((n + 1) * (n + 2)) * (n + 4)) * 6) * (n + 3))) by A11, XCMPLX_1:91 .= (29 / 36) - ((((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) - ((((n + 3) * 6) * (n + 3)) / (((((n + 1) * (n + 2)) * (n + 4)) * 6) * (n + 3)))) .= (29 / 36) - ((((((((n * 2) + 7) * (n + 1)) * 3) * (n + 4)) + (8 * (n + 4))) - (((n + 3) * 6) * (n + 3))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) by XCMPLX_1:120 .= (29 / 36) - ((((((6 * (n + 1)) * (n + 2)) * (n + 3)) + ((9 * (n + 1)) * (n + 2))) + (8 * (n + 1))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) .= (29 / 36) - ((((((6 * (n + 1)) * (n + 2)) * (n + 3)) + ((9 * (n + 1)) * (n + 2))) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) by XCMPLX_1:62 .= (29 / 36) - ((((1 * (((6 * (n + 1)) * (n + 2)) * (n + 3))) / ((n + 4) * (((6 * (n + 1)) * (n + 2)) * (n + 3)))) + (((9 * (n + 1)) * (n + 2)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) by XCMPLX_1:62 .= (29 / 36) - (((1 / (n + 4)) + ((3 * ((3 * (n + 1)) * (n + 2))) / (((2 * (n + 3)) * (n + 4)) * ((3 * (n + 1)) * (n + 2))))) + ((8 * (n + 1)) / ((((6 * (n + 1)) * (n + 2)) * (n + 3)) * (n + 4)))) by A12, XCMPLX_1:91 .= (29 / 36) - (((1 / (n + 4)) + (3 / ((2 * (n + 3)) * (n + 4)))) + ((4 * (2 * (n + 1))) / ((((3 * (n + 2)) * (n + 3)) * (n + 4)) * (2 * (n + 1))))) by A10, XCMPLX_1:91 .= (29 / 36) - (((1 / (n + 4)) + (3 / ((2 * (n + 3)) * (n + 4)))) + (4 / (((3 * (n + 2)) * (n + 3)) * (n + 4)))) by A7, XCMPLX_1:91 .= (((29 / 36) - (1 / ((n + 1) + 3))) - (3 / ((2 * ((n + 1) + 2)) * ((n + 1) + 3)))) - (4 / (((3 * ((n + 1) + 1)) * ((n + 1) + 2)) * ((n + 1) + 3))) ; 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 .= (1 + 2) / ((1 * (1 + 1)) * (1 + 3)) by A1, A2 .= (((29 / 36) - (1 / (1 + 3))) - (3 / ((2 * (1 + 2)) * (1 + 3)))) - (4 / (((3 * (1 + 1)) * (1 + 2)) * (1 + 3))) ; then A13: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A13, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (((29 / 36) - (1 / (n + 3))) - (3 / ((2 * (n + 2)) * (n + 3)))) - (4 / (((3 * (n + 1)) * (n + 2)) * (n + 3))) ; ::_thesis: verum end; theorem :: SERIES_2:32 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = ((2 |^ (\$1 + 1)) / (\$1 + 3)) - (1 / 2); assume A1: for n being Element of NAT holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (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] ) n + 3 >= 3 by NAT_1:11; then A3: n + 3 > 0 by XXREAL_0:2; n + 4 >= 4 by NAT_1:11; then A4: n + 4 > 0 by XXREAL_0:2; assume (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2) ; ::_thesis: S1[n + 1] then (Partial_Sums s) . (n + 1) = (((2 |^ (n + 1)) / (n + 3)) - (1 / 2)) + (s . (n + 1)) by SERIES_1:def_1 .= (((2 |^ (n + 1)) / (n + 3)) - (1 / 2)) + ((((n + 1) + 1) * (2 |^ (n + 1))) / (((n + 1) + 2) * ((n + 1) + 3))) by A1 .= (((2 |^ (n + 1)) / (n + 3)) + (((n + 2) * (2 |^ (n + 1))) / ((n + 3) * (n + 4)))) - (1 / 2) .= ((((2 |^ (n + 1)) * (n + 4)) / ((n + 3) * (n + 4))) + (((n + 2) * (2 |^ (n + 1))) / ((n + 3) * (n + 4)))) - (1 / 2) by A4, XCMPLX_1:91 .= ((((2 |^ (n + 1)) * (n + 4)) + ((n + 2) * (2 |^ (n + 1)))) / ((n + 3) * (n + 4))) - (1 / 2) by XCMPLX_1:62 .= ((((2 |^ (n + 1)) * 2) * (n + 3)) / ((n + 4) * (n + 3))) - (1 / 2) .= (((2 |^ (n + 1)) * 2) / (n + 4)) - (1 / 2) by A3, XCMPLX_1:91 .= ((2 |^ ((n + 1) + 1)) / ((n + 1) + 3)) - (1 / 2) by NEWTON:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= ((0 + 1) * (2 |^ 0)) / ((0 + 2) * (0 + 3)) by A1 .= (1 * 1) / 6 by NEWTON:4 .= (2 / 3) - (1 / 2) .= ((2 |^ (0 + 1)) / (0 + 3)) - (1 / 2) by NEWTON:5 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2) ; ::_thesis: verum end; theorem :: SERIES_2:33 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((n |^ 2) * (4 |^ n)) / ((n + 1) * (n + 2)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((n |^ 2) * (4 |^ n)) / ((n + 1) * (n + 2)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (2 / 3) + (((\$1 - 1) * (4 |^ (\$1 + 1))) / (3 * (\$1 + 2))); assume A1: for n being Element of NAT holds s . n = ((n |^ 2) * (4 |^ n)) / ((n + 1) * (n + 2)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2))) then A2: s . 0 = ((0 |^ 2) * (4 |^ 0)) / ((0 + 1) * (0 + 2)) .= (0 * (4 |^ 0)) / (1 * 2) by NEWTON:11 .= 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 = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2))) ; ::_thesis: S1[n + 1] n + 2 >= 2 by NAT_1:11; then A5: n + 2 > 0 by XXREAL_0:2; n + 3 >= 3 by NAT_1:11; then A6: n + 3 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2)))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= ((2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2)))) + ((((n + 1) |^ 2) * (4 |^ (n + 1))) / (((n + 1) + 1) * ((n + 1) + 2))) by A1 .= ((2 / 3) + ((((n - 1) * (4 |^ (n + 1))) * (n + 3)) / ((3 * (n + 2)) * (n + 3)))) + ((((n + 1) |^ 2) * (4 |^ (n + 1))) / ((n + 2) * (n + 3))) by A6, XCMPLX_1:91 .= ((2 / 3) + ((((n - 1) * (4 |^ (n + 1))) * (n + 3)) / ((3 * (n + 2)) * (n + 3)))) + (((((n + 1) |^ 2) * (4 |^ (n + 1))) * 3) / (((n + 2) * (n + 3)) * 3)) by XCMPLX_1:91 .= (2 / 3) + (((((n - 1) * (4 |^ (n + 1))) * (n + 3)) / ((3 * (n + 2)) * (n + 3))) + (((((n + 1) |^ 2) * (4 |^ (n + 1))) * 3) / ((3 * (n + 2)) * (n + 3)))) .= (2 / 3) + (((((n - 1) * (4 |^ (n + 1))) * (n + 3)) + ((((n + 1) |^ 2) * (4 |^ (n + 1))) * 3)) / ((3 * (n + 2)) * (n + 3))) by XCMPLX_1:62 .= (2 / 3) + (((((n - 1) * (n + 3)) + (((n + 1) |^ 2) * 3)) * (4 |^ (n + 1))) / ((3 * (n + 2)) * (n + 3))) .= (2 / 3) + (((((n - 1) * (n + 3)) + (((n + 1) * (n + 1)) * 3)) * (4 |^ (n + 1))) / ((3 * (n + 2)) * (n + 3))) by WSIERP_1:1 .= (2 / 3) + ((((4 * (4 |^ (n + 1))) * n) * (n + 2)) / ((3 * (n + 3)) * (n + 2))) .= (2 / 3) + ((((4 |^ (n + 1)) * 4) * n) / (3 * (n + 3))) by A5, XCMPLX_1:91 .= (2 / 3) + ((((n + 1) - 1) * (4 |^ ((n + 1) + 1))) / (3 * ((n + 1) + 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 .= ((1 |^ 2) * (4 |^ 1)) / ((1 + 1) * (1 + 2)) by A1, A2 .= (1 * (4 |^ 1)) / ((1 + 1) * (1 + 2)) by NEWTON:10 .= (1 * 4) / ((1 + 1) * (1 + 2)) by NEWTON:5 .= (2 / 3) + (((1 - 1) * (4 |^ (1 + 1))) / (3 * (1 + 2))) ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (2 / 3) + (((n - 1) * (4 |^ (n + 1))) / (3 * (n + 2))) ; ::_thesis: verum end; theorem :: SERIES_2:34 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (2 |^ n)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (2 |^ n)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = 1 - (1 / ((\$1 + 1) * (2 |^ \$1))); assume A1: for n being Element of NAT holds s . n = (n + 2) / ((n * (n + 1)) * (2 |^ n)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n))) then A2: s . 0 = (0 + 2) / ((0 * (0 + 1)) * (2 |^ 0)) .= 0 by XCMPLX_1:49 ; 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 = 1 - (1 / ((n + 1) * (2 |^ n))) ; ::_thesis: S1[n + 1] n + 1 >= 1 + 0 by NAT_1:11; then A5: n + 1 > 0 by NAT_1:13; n + 2 >= 2 by NAT_1:11; then A6: n + 2 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (1 - (1 / ((n + 1) * (2 |^ n)))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (1 - (1 / ((n + 1) * (2 |^ n)))) + (((n + 1) + 2) / (((n + 1) * ((n + 1) + 1)) * (2 |^ (n + 1)))) by A1 .= 1 - ((1 / ((n + 1) * (2 |^ n))) - ((n + 3) / (((n + 1) * (n + 2)) * (2 |^ (n + 1))))) .= 1 - (((1 * 2) / (((n + 1) * (2 |^ n)) * 2)) - ((n + 3) / (((n + 1) * (n + 2)) * (2 |^ (n + 1))))) by XCMPLX_1:91 .= 1 - (((1 * 2) / ((n + 1) * ((2 |^ n) * 2))) - ((n + 3) / (((n + 1) * (n + 2)) * (2 |^ (n + 1))))) .= 1 - (((1 * 2) / ((n + 1) * (2 |^ (n + 1)))) - ((n + 3) / (((n + 1) * (n + 2)) * (2 |^ (n + 1))))) by NEWTON:6 .= 1 - (((2 * (n + 2)) / (((n + 1) * (2 |^ (n + 1))) * (n + 2))) - ((n + 3) / (((n + 1) * (n + 2)) * (2 |^ (n + 1))))) by A6, XCMPLX_1:91 .= 1 - (((2 * (n + 2)) - (n + 3)) / (((n + 1) * (n + 2)) * (2 |^ (n + 1)))) by XCMPLX_1:120 .= 1 - ((1 * (n + 1)) / (((n + 2) * (2 |^ (n + 1))) * (n + 1))) .= 1 - (1 / (((n + 1) + 1) * (2 |^ (n + 1)))) by A5, XCMPLX_1:91 ; 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 .= (1 + 2) / ((1 * (1 + 1)) * (2 |^ 1)) by A1, A2 .= (1 + 2) / ((1 * (1 + 1)) * 2) by NEWTON:5 .= 1 - (1 / ((1 + 1) * 2)) .= 1 - (1 / ((1 + 1) * (2 |^ 1))) by NEWTON:5 ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (2 |^ n))) ; ::_thesis: verum end; theorem :: SERIES_2:35 for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 3) / ((n * (n + 1)) * (3 |^ n)) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) + 3) / ((n * (n + 1)) * (3 |^ n)) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n))) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = 1 - (1 / ((\$1 + 1) * (3 |^ \$1))); assume A1: for n being Element of NAT holds s . n = ((2 * n) + 3) / ((n * (n + 1)) * (3 |^ n)) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n))) then A2: s . 0 = ((2 * 0) + 3) / ((0 * (0 + 1)) * (3 |^ 0)) .= 0 by XCMPLX_1:49 ; 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 = 1 - (1 / ((n + 1) * (3 |^ n))) ; ::_thesis: S1[n + 1] n + 1 >= 1 + 0 by NAT_1:11; then A5: n + 1 > 0 by NAT_1:13; n + 2 >= 2 by NAT_1:11; then A6: n + 2 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (1 - (1 / ((n + 1) * (3 |^ n)))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (1 - (1 / ((n + 1) * (3 |^ n)))) + (((2 * (n + 1)) + 3) / (((n + 1) * ((n + 1) + 1)) * (3 |^ (n + 1)))) by A1 .= (1 - ((1 * 3) / (((n + 1) * (3 |^ n)) * 3))) + (((2 * n) + 5) / (((n + 1) * (n + 2)) * (3 |^ (n + 1)))) by XCMPLX_1:91 .= (1 - (3 / ((n + 1) * ((3 |^ n) * 3)))) + (((2 * n) + 5) / (((n + 1) * (n + 2)) * (3 |^ (n + 1)))) .= (1 - (3 / ((n + 1) * (3 |^ (n + 1))))) + (((2 * n) + 5) / (((n + 1) * (n + 2)) * (3 |^ (n + 1)))) by NEWTON:6 .= (1 - ((3 * (n + 2)) / (((n + 1) * (3 |^ (n + 1))) * (n + 2)))) + (((2 * n) + 5) / (((n + 1) * (n + 2)) * (3 |^ (n + 1)))) by A6, XCMPLX_1:91 .= 1 - (((3 * (n + 2)) / (((n + 1) * (3 |^ (n + 1))) * (n + 2))) - (((2 * n) + 5) / (((n + 1) * (n + 2)) * (3 |^ (n + 1))))) .= 1 - (((3 * (n + 2)) - ((2 * n) + 5)) / (((n + 1) * (n + 2)) * (3 |^ (n + 1)))) by XCMPLX_1:120 .= 1 - ((1 * (n + 1)) / (((n + 2) * (3 |^ (n + 1))) * (n + 1))) .= 1 - (1 / (((n + 1) + 1) * (3 |^ (n + 1)))) by A5, XCMPLX_1:91 ; 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 .= ((2 * 1) + 3) / ((1 * (1 + 1)) * (3 |^ 1)) by A1, A2 .= ((2 * 1) + 3) / ((1 * (1 + 1)) * 3) by NEWTON:5 .= 1 - (1 / ((1 + 1) * 3)) .= 1 - (1 / ((1 + 1) * (3 |^ 1))) by NEWTON:5 ; then A7: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A7, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) * (3 |^ n))) ; ::_thesis: verum end; theorem :: SERIES_2:36 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) ) holds for n being Element of NAT holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) ) implies for n being Element of NAT holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 = (1 / 3) + (((- 1) |^ (\$1 + 2)) / (3 * ((2 |^ (\$1 + 2)) + ((- 1) |^ (\$1 + 2))))); assume A1: for n being Element of NAT holds s . n = (((- 1) |^ n) * (2 |^ (n + 1))) / (((2 |^ (n + 1)) + ((- 1) |^ (n + 1))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 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] ) set b = (2 |^ (n + 2)) + ((- 1) |^ (n + 2)); set p = (2 |^ (n + 3)) + ((- 1) |^ (n + 3)); A3: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by Lm18; assume (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) ; ::_thesis: S1[n + 1] then A4: (Partial_Sums s) . (n + 1) = ((1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))) + (s . (n + 1)) by SERIES_1:def_1 .= ((1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))) + ((((- 1) |^ (n + 1)) * (2 |^ ((n + 1) + 1))) / (((2 |^ ((n + 1) + 1)) + ((- 1) |^ ((n + 1) + 1))) * ((2 |^ ((n + 1) + 2)) + ((- 1) |^ ((n + 1) + 2))))) by A1 .= ((1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))))) + ((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) / (((2 |^ (n + 2)) + ((- 1) |^ (n + 2))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) ; (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 by Lm19; then (Partial_Sums s) . (n + 1) = ((1 / 3) + ((((- 1) |^ (n + 2)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))))) + ((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) / (((2 |^ (n + 2)) + ((- 1) |^ (n + 2))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by A4, XCMPLX_1:91 .= ((1 / 3) + ((((- 1) |^ (n + 2)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))))) + (((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) * 3) / ((((2 |^ (n + 2)) + ((- 1) |^ (n + 2))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) * 3)) by XCMPLX_1:91 .= (1 / 3) + (((((- 1) |^ (n + 2)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) + (((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) * 3) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))))) .= (1 / 3) + (((((((- 1) |^ (n + 2)) * (- 1)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + ((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by XCMPLX_1:62 .= (1 / 3) + ((((((- 1) |^ ((n + 2) + 1)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + ((((- 1) |^ (n + 1)) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by NEWTON:6 .= (1 / 3) + ((((((- 1) |^ (n + 3)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + ((((((- 1) |^ (n + 1)) * (- 1)) / (- 1)) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) .= (1 / 3) + ((((((- 1) |^ (n + 3)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + (((((- 1) |^ ((n + 1) + 1)) / (- 1)) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by NEWTON:6 .= (1 / 3) + ((((((- 1) |^ (n + 3)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + ((((((- 1) |^ (n + 2)) * (- 1)) / ((- 1) * (- 1))) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) .= (1 / 3) + ((((((- 1) |^ (n + 3)) / (- 1)) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) + (((((- 1) |^ ((n + 2) + 1)) / ((- 1) * (- 1))) * (2 |^ (n + 2))) * 3)) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by NEWTON:6 .= (1 / 3) + ((((- 1) |^ (n + 3)) * ((((2 |^ (n + 2)) + ((2 |^ (n + 2)) * 2)) - (2 |^ (n + 3))) - ((- 1) |^ (n + 3)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) .= (1 / 3) + ((((- 1) |^ (n + 3)) * ((((2 |^ (n + 2)) + (2 |^ ((n + 2) + 1))) - (2 |^ (n + 3))) - ((- 1) |^ (n + 3)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by NEWTON:6 .= (1 / 3) + ((((- 1) |^ (n + 3)) * ((2 |^ (n + 2)) - (((- 1) |^ (n + 2)) * (- 1)))) / ((3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3))))) by NEWTON:6 .= (1 / 3) + ((((- 1) |^ (n + 3)) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2)))) / ((3 * ((2 |^ (n + 3)) + ((- 1) |^ (n + 3)))) * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) .= (1 / 3) + (((- 1) |^ ((n + 2) + 1)) / (3 * ((2 |^ ((n + 2) + 1)) + ((- 1) |^ ((n + 2) + 1))))) by A3, XCMPLX_1:91 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (((- 1) |^ 0) * (2 |^ (0 + 1))) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))) by A1 .= (1 * (2 |^ (0 + 1))) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))) by NEWTON:4 .= (1 * 2) / (((2 |^ (0 + 1)) + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))) by NEWTON:5 .= (1 * 2) / ((2 + ((- 1) |^ (0 + 1))) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))) by NEWTON:5 .= (1 * 2) / ((2 + (- 1)) * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2)))) by NEWTON:5 .= (1 * 2) / ((2 + (- 1)) * ((2 * 2) + ((- 1) |^ (0 + 2)))) by WSIERP_1:1 .= (1 * 2) / ((2 + (- 1)) * ((2 * 2) + ((- 1) * (- 1)))) by WSIERP_1:1 .= (1 / 3) + (((- 1) * (- 1)) / (3 * ((2 * 2) + ((- 1) * (- 1))))) .= (1 / 3) + (((- 1) |^ 2) / (3 * ((2 * 2) + ((- 1) * (- 1))))) by WSIERP_1:1 .= (1 / 3) + (((- 1) |^ 2) / (3 * ((2 * 2) + ((- 1) |^ 2)))) by WSIERP_1:1 .= (1 / 3) + (((- 1) |^ (0 + 2)) / (3 * ((2 |^ (0 + 2)) + ((- 1) |^ (0 + 2))))) by WSIERP_1:1 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); hence for n being Element of NAT holds (Partial_Sums s) . n = (1 / 3) + (((- 1) |^ (n + 2)) / (3 * ((2 |^ (n + 2)) + ((- 1) |^ (n + 2))))) ; ::_thesis: verum end; theorem :: SERIES_2:37 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n !) * n ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - 1 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n !) * n ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - 1 ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = ((\$1 + 1) !) - 1; assume A1: for n being Element of NAT holds s . n = (n !) * n ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = ((n + 1) !) - 1 then A2: s . 0 = (0 !) * 0 .= 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 ; ::_thesis: S1[n + 1] n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (((n + 1) !) - 1) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (((n + 1) !) - 1) + (((n + 1) !) * (n + 1)) by A1 .= (((n + 1) !) * ((n + 1) + 1)) - 1 .= (((n + 1) + 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 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= (1 !) * 1 by A1, A2 .= ((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 ; ::_thesis: verum end; theorem :: SERIES_2:38 for s being Real_Sequence st ( for n being Element of NAT holds s . n = n / ((n + 1) !) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) !)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = n / ((n + 1) !) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) !)) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = 1 - (1 / ((\$1 + 1) !)); assume A1: for n being Element of NAT holds s . n = n / ((n + 1) !) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - (1 / ((n + 1) !)) then A2: s . 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 = 1 - (1 / ((n + 1) !)) ; ::_thesis: S1[n + 1] n + 2 >= 2 by NAT_1:11; then A5: n + 2 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (1 - (1 / ((n + 1) !))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (1 - (1 / ((n + 1) !))) + ((n + 1) / (((n + 1) + 1) !)) by A1 .= (1 - ((1 * (n + 2)) / (((n + 1) !) * ((n + 1) + 1)))) + ((n + 1) / ((n + 2) !)) by A5, XCMPLX_1:91 .= (1 - ((1 * (n + 2)) / (((n + 1) + 1) !))) + ((n + 1) / ((n + 2) !)) by NEWTON:15 .= 1 - (((n + 2) / (((n + 1) + 1) !)) - ((n + 1) / ((n + 2) !))) .= 1 - (((n + 2) - (n + 1)) / ((n + 2) !)) by XCMPLX_1:120 .= 1 - (1 / (((n + 1) + 1) !)) ; 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 .= 1 - (1 / ((1 + 1) !)) by A1, A2, NEWTON:14 ; 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 = 1 - (1 / ((n + 1) !)) ; ::_thesis: verum end; theorem :: SERIES_2:39 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = (((n |^ 2) + n) - 1) / ((n + 2) !) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 2) !)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = (((n |^ 2) + n) - 1) / ((n + 2) !) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 2) !)) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = (1 / 2) - ((\$1 + 1) / ((\$1 + 2) !)); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = (((n |^ 2) + n) - 1) / ((n + 2) !) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 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 = (1 / 2) - ((n + 1) / ((n + 2) !)) ; ::_thesis: S1[n + 1] A4: n + 1 >= 1 by NAT_1:11; n + 3 >= 3 by NAT_1:11; then A5: n + 3 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = ((1 / 2) - ((n + 1) / ((n + 2) !))) + (s . (n + 1)) by A3, SERIES_1:def_1 .= ((1 / 2) - ((n + 1) / ((n + 2) !))) + (((((n + 1) |^ 2) + (n + 1)) - 1) / (((n + 1) + 2) !)) by A1, A4 .= ((1 / 2) - (((n + 1) * (n + 3)) / (((n + 2) !) * ((n + 2) + 1)))) + ((((n + 1) |^ 2) + n) / ((n + 3) !)) by A5, XCMPLX_1:91 .= ((1 / 2) - (((n + 1) * (n + 3)) / (((n + 2) + 1) !))) + ((((n + 1) |^ 2) + n) / ((n + 3) !)) by NEWTON:15 .= (1 / 2) - ((((n + 1) * (n + 3)) / ((n + 3) !)) - ((((n + 1) |^ 2) + n) / ((n + 3) !))) .= (1 / 2) - ((((n + 1) * (n + 3)) - (((n + 1) |^ 2) + n)) / ((n + 3) !)) by XCMPLX_1:120 .= (1 / 2) - (((((n + 1) * (n + 3)) - ((n + 1) |^ 2)) - n) / ((n + 3) !)) .= (1 / 2) - (((((n + 1) * (n + 3)) - ((n + 1) * (n + 1))) - n) / ((n + 3) !)) by WSIERP_1:1 .= (1 / 2) - (((n + 1) + 1) / (((n + 1) + 2) !)) ; 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 .= (((1 |^ 2) + 1) - 1) / ((1 + 2) !) by A1 .= (1 * 1) / ((2 + 1) !) by WSIERP_1:1 .= 1 / (2 * 3) by NEWTON:14, NEWTON:15 .= (1 / 2) - (2 / ((2 !) * (2 + 1))) by NEWTON:14 .= (1 / 2) - (2 / ((2 + 1) !)) by NEWTON:15 ; then A6: S1[1] ; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A6, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = (1 / 2) - ((n + 1) / ((n + 2) !)) ; ::_thesis: verum end; theorem :: SERIES_2:40 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (n * (2 |^ n)) / ((n + 2) !) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (n * (2 |^ n)) / ((n + 2) !) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !)) ) defpred S1[ Nat] means (Partial_Sums s) . \$1 = 1 - ((2 |^ (\$1 + 1)) / ((\$1 + 2) !)); assume A1: for n being Element of NAT holds s . n = (n * (2 |^ n)) / ((n + 2) !) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n = 1 - ((2 |^ (n + 1)) / ((n + 2) !)) then A2: s . 0 = (0 * (2 |^ 0)) / ((0 + 2) !) .= 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 = 1 - ((2 |^ (n + 1)) / ((n + 2) !)) ; ::_thesis: S1[n + 1] n + 3 >= 3 by NAT_1:11; then A5: n + 3 > 0 by XXREAL_0:2; n in NAT by ORDINAL1:def_12; then (Partial_Sums s) . (n + 1) = (1 - ((2 |^ (n + 1)) / ((n + 2) !))) + (s . (n + 1)) by A4, SERIES_1:def_1 .= (1 - ((2 |^ (n + 1)) / ((n + 2) !))) + (((n + 1) * (2 |^ (n + 1))) / (((n + 1) + 2) !)) by A1 .= (1 - (((2 |^ (n + 1)) * (n + 3)) / (((n + 2) !) * ((n + 2) + 1)))) + (((n + 1) * (2 |^ (n + 1))) / ((n + 3) !)) by A5, XCMPLX_1:91 .= (1 - (((2 |^ (n + 1)) * (n + 3)) / (((n + 2) + 1) !))) + (((n + 1) * (2 |^ (n + 1))) / ((n + 3) !)) by NEWTON:15 .= 1 - ((((2 |^ (n + 1)) * (n + 3)) / (((n + 2) + 1) !)) - (((n + 1) * (2 |^ (n + 1))) / ((n + 3) !))) .= 1 - ((((2 |^ (n + 1)) * (n + 3)) - ((2 |^ (n + 1)) * (n + 1))) / ((n + 3) !)) by XCMPLX_1:120 .= 1 - (((2 |^ (n + 1)) * 2) / ((n + 3) !)) .= 1 - ((2 |^ ((n + 1) + 1)) / (((n + 1) + 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 .= (1 * (2 |^ 1)) / ((1 + 2) !) by A1, A2 .= 2 / ((2 + 1) !) by NEWTON:5 .= 2 / (2 * 3) by NEWTON:14, NEWTON:15 .= 1 - ((2 * 2) / ((2 !) * (2 + 1))) by NEWTON:14 .= 1 - ((2 |^ 2) / ((2 !) * (2 + 1))) by WSIERP_1:1 .= 1 - ((2 |^ (1 + 1)) / ((1 + 2) !)) by NEWTON:15 ; 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 = 1 - ((2 |^ (n + 1)) / ((n + 2) !)) ; ::_thesis: verum end; theorem :: SERIES_2:41 for a, b being real number for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by Lm14; theorem :: SERIES_2:42 for a, b being real number for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 proof let a, b be real number ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (a * n) + b ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (a * n) + b ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 ) assume A1: for n being Element of NAT holds s . n = (a * n) + b ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by A1, Lm14 .= ((n + 1) * (((n * a) + b) + b)) / 2 .= ((n + 1) * ((s . n) + ((a * 0) + b))) / 2 by A1 .= ((n + 1) * ((s . n) + (s . 0))) / 2 by A1 ; hence (Partial_Sums s) . n = ((n + 1) * ((s . 0) + (s . n))) / 2 ; ::_thesis: verum end;