:: SERIES_3 semantic presentation begin registration let x be real number ; cluster|.x.| -> non negative ; coherence not abs x is negative ; end; Lm1: for x being real number holds x ^2 = x |^ 2 proof let x be real number ; ::_thesis: x ^2 = x |^ 2 x ^2 = (x |^ 1) * x by NEWTON:5 .= x |^ (1 + 1) by NEWTON:6 .= x |^ 2 ; hence x ^2 = x |^ 2 ; ::_thesis: verum end; Lm2: 1 |^ 3 = 1 by NEWTON:10; Lm3: 2 |^ 3 = 8 proof 2 |^ 3 = 2 |^ (2 + 1) .= (2 |^ 2) * 2 by NEWTON:6 .= (2 ^2) * 2 by Lm1 .= 8 ; hence 2 |^ 3 = 8 ; ::_thesis: verum end; Lm4: 3 |^ 3 = 27 proof 3 |^ 3 = 3 |^ (2 + 1) .= (3 |^ 2) * 3 by NEWTON:6 .= (3 ^2) * 3 by Lm1 .= 27 ; hence 3 |^ 3 = 27 ; ::_thesis: verum end; Lm5: for x being real number holds (- x) |^ 3 = - (x |^ 3) proof let x be real number ; ::_thesis: (- x) |^ 3 = - (x |^ 3) 3 = (2 * 1) + 1 ; then 3 is odd by ABIAN:1; hence (- x) |^ 3 = - (x |^ 3) by POWER:2; ::_thesis: verum end; Lm6: for x, y being real number holds (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) proof let x, y be real number ; ::_thesis: (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) (x + y) |^ 3 = ((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3) by POLYEQ_1:14 .= (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) ; hence (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) ; ::_thesis: verum end; Lm7: for x, y being real number holds (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) proof let x, y be real number ; ::_thesis: (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) (((x ^2) - (x * y)) + (y ^2)) * (x + y) = ((((x ^2) * x) + (y * (x ^2))) - ((x * (x * y)) + (y * (x * y)))) + (((x * (y ^2)) + (y * (y ^2))) + (0 * (y ^2))) .= (((x |^ 3) + (y * (x ^2))) - ((x * (x * y)) + (y * (x * y)))) + ((x * (y ^2)) + (y * (y ^2))) by POLYEQ_2:4 .= (((x |^ 3) + (y * (x ^2))) - (((x ^2) * y) + ((y * y) * x))) + ((x * (y ^2)) + (y |^ 3)) by POLYEQ_2:4 .= (x |^ 3) + (y |^ 3) ; hence (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) ; ::_thesis: verum end; Lm8: for x, y, z being real number st x ^2 <= y * z holds abs x <= sqrt (y * z) proof let x, y, z be real number ; ::_thesis: ( x ^2 <= y * z implies abs x <= sqrt (y * z) ) A1: x ^2 >= 0 by XREAL_1:63; assume x ^2 <= y * z ; ::_thesis: abs x <= sqrt (y * z) then A2: sqrt (x ^2) <= sqrt (y * z) by A1, SQUARE_1:26; percases ( x >= 0 or x < 0 ) ; supposeA3: x >= 0 ; ::_thesis: abs x <= sqrt (y * z) then x <= sqrt (y * z) by A2, SQUARE_1:22; hence abs x <= sqrt (y * z) by A3, ABSVALUE:def_1; ::_thesis: verum end; supposeA4: x < 0 ; ::_thesis: abs x <= sqrt (y * z) then - x <= sqrt (y * z) by A2, SQUARE_1:23; hence abs x <= sqrt (y * z) by A4, ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem :: SERIES_3:1 for y, x, m being real number st y > x & x >= 0 & m >= 0 holds x / y <= (x + m) / (y + m) proof let y, x, m be real number ; ::_thesis: ( y > x & x >= 0 & m >= 0 implies x / y <= (x + m) / (y + m) ) assume that A1: y > x and A2: x >= 0 and A3: m >= 0 ; ::_thesis: x / y <= (x + m) / (y + m) y - x > 0 by A1, XREAL_1:50; then m * (y - x) >= 0 by A3; then ((y * (x + m)) - (x * (m + y))) / (y * (y + m)) >= 0 by A1, A2, A3; then ((x + m) / (y + m)) - (x / y) >= 0 by A1, A2, A3, XCMPLX_1:130; then (((x + m) / (y + m)) - (x / y)) + (x / y) >= 0 + (x / y) by XREAL_1:6; hence x / y <= (x + m) / (y + m) ; ::_thesis: verum end; theorem Th2: :: SERIES_3:2 for a, b being real positive number holds (a + b) / 2 >= sqrt (a * b) proof let a, b be real positive number ; ::_thesis: (a + b) / 2 >= sqrt (a * b) (a + b) / 2 >= (2 * (sqrt (a * b))) / 2 by SIN_COS2:1, XREAL_1:72; hence (a + b) / 2 >= sqrt (a * b) ; ::_thesis: verum end; theorem :: SERIES_3:3 for b, a being real positive number holds (b / a) + (a / b) >= 2 proof let b, a be real positive number ; ::_thesis: (b / a) + (a / b) >= 2 (a - b) ^2 >= 0 by XREAL_1:63; then (((a ^2) - ((2 * a) * b)) + (b ^2)) + ((2 * a) * b) >= 0 + ((2 * a) * b) by XREAL_1:7; then ((a ^2) + (b ^2)) / (a * b) >= (2 * (a * b)) / (1 * (a * b)) by XREAL_1:72; then A1: ((a ^2) + (b ^2)) / (a * b) >= 2 / 1 by XCMPLX_1:91; (b / a) + (a / b) = ((b * b) / (a * b)) + (a / b) by XCMPLX_1:91 .= ((b * b) / (a * b)) + ((a * a) / (a * b)) by XCMPLX_1:91 .= ((b ^2) + (a ^2)) / (a * b) ; hence (b / a) + (a / b) >= 2 by A1; ::_thesis: verum end; theorem Th4: :: SERIES_3:4 for x, y being real number holds ((x + y) / 2) ^2 >= x * y proof let x, y be real number ; ::_thesis: ((x + y) / 2) ^2 >= x * y (x - y) ^2 >= 0 by XREAL_1:63; then (((x ^2) - ((2 * x) * y)) + (y ^2)) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:7; then ((x ^2) + (y ^2)) + ((2 * x) * y) >= ((2 * x) * y) + ((2 * x) * y) by XREAL_1:7; then ((x + y) ^2) / (2 * 2) >= (4 * (x * y)) / 4 by XREAL_1:72; hence ((x + y) / 2) ^2 >= x * y ; ::_thesis: verum end; theorem :: SERIES_3:5 for x, y being real number holds ((x ^2) + (y ^2)) / 2 >= ((x + y) / 2) ^2 proof let x, y be real number ; ::_thesis: ((x ^2) + (y ^2)) / 2 >= ((x + y) / 2) ^2 (x - y) ^2 >= 0 by XREAL_1:63; then (((x ^2) - ((2 * x) * y)) + (y ^2)) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:7; then ((x ^2) + (y ^2)) + ((x ^2) + (y ^2)) >= ((2 * x) * y) + ((x ^2) + (y ^2)) by XREAL_1:7; then (2 * ((x ^2) + (y ^2))) / 4 >= ((x + y) ^2) / 4 by XREAL_1:72; hence ((x ^2) + (y ^2)) / 2 >= ((x + y) / 2) ^2 ; ::_thesis: verum end; theorem Th6: :: SERIES_3:6 for x, y being real number holds (x ^2) + (y ^2) >= (2 * x) * y proof let x, y be real number ; ::_thesis: (x ^2) + (y ^2) >= (2 * x) * y (x - y) ^2 >= 0 by XREAL_1:63; then (((x ^2) - ((2 * x) * y)) + (y ^2)) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:6; hence (x ^2) + (y ^2) >= (2 * x) * y ; ::_thesis: verum end; theorem Th7: :: SERIES_3:7 for x, y being real number holds ((x ^2) + (y ^2)) / 2 >= x * y proof let x, y be real number ; ::_thesis: ((x ^2) + (y ^2)) / 2 >= x * y ((x ^2) + (y ^2)) / 2 >= ((2 * x) * y) / 2 by Th6, XREAL_1:72; hence ((x ^2) + (y ^2)) / 2 >= x * y ; ::_thesis: verum end; theorem Th8: :: SERIES_3:8 for x, y being real number holds (x ^2) + (y ^2) >= (2 * (abs x)) * (abs y) proof let x, y be real number ; ::_thesis: (x ^2) + (y ^2) >= (2 * (abs x)) * (abs y) A1: ( x ^2 >= 0 & y ^2 >= 0 ) by XREAL_1:63; then (x ^2) + (y ^2) >= 2 * (sqrt ((x ^2) * (y ^2))) by SIN_COS2:1; then (x ^2) + (y ^2) >= 2 * ((sqrt (x ^2)) * (sqrt (y ^2))) by A1, SQUARE_1:29; then (x ^2) + (y ^2) >= 2 * ((sqrt ((abs x) ^2)) * (sqrt (y ^2))) by COMPLEX1:75; then (x ^2) + (y ^2) >= 2 * ((sqrt ((abs x) ^2)) * (sqrt ((abs y) ^2))) by COMPLEX1:75; then (x ^2) + (y ^2) >= 2 * ((abs x) * (sqrt ((abs y) ^2))) by SQUARE_1:22; then (x ^2) + (y ^2) >= 2 * ((abs x) * (abs y)) by SQUARE_1:22; hence (x ^2) + (y ^2) >= (2 * (abs x)) * (abs y) ; ::_thesis: verum end; theorem Th9: :: SERIES_3:9 for x, y being real number holds (x + y) ^2 >= (4 * x) * y proof let x, y be real number ; ::_thesis: (x + y) ^2 >= (4 * x) * y 2 * (((x ^2) + (y ^2)) / 2) >= 2 * (x * y) by Th7, XREAL_1:64; then ((x ^2) + (y ^2)) + ((2 * x) * y) >= ((2 * x) * y) + ((2 * x) * y) by XREAL_1:6; hence (x + y) ^2 >= (4 * x) * y ; ::_thesis: verum end; theorem Th10: :: SERIES_3:10 for x, y, z being real number holds ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) proof let x, y, z be real number ; ::_thesis: ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) ( (x ^2) + (y ^2) >= (2 * x) * y & (y ^2) + (z ^2) >= (2 * y) * z ) by Th6; then A1: ((x ^2) + (y ^2)) + ((y ^2) + (z ^2)) >= ((2 * x) * y) + ((2 * y) * z) by XREAL_1:7; (z ^2) + (x ^2) >= (2 * z) * x by Th6; then (((x ^2) + (y ^2)) + ((y ^2) + (z ^2))) + ((z ^2) + (x ^2)) >= (((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x) by A1, XREAL_1:7; then (2 * (((x ^2) + (y ^2)) + (z ^2))) / 2 >= (2 * (((x * y) + (y * z)) + (z * x))) / 2 by XREAL_1:72; hence ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) ; ::_thesis: verum end; theorem :: SERIES_3:11 for x, y, z being real number holds ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z)) proof let x, y, z be real number ; ::_thesis: ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z)) ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) by Th10; then (((x ^2) + (y ^2)) + (z ^2)) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x)) >= (((x * y) + (y * z)) + (x * z)) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x)) by XREAL_1:6; hence ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z)) ; ::_thesis: verum end; theorem Th12: :: SERIES_3:12 for a, b, c being real positive number holds ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c proof let a, b, c be real positive number ; ::_thesis: ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c A1: ((a + c) |^ 3) - (((3 * (a ^2)) * c) + ((3 * a) * (c ^2))) = ((((a |^ 3) + ((3 * (a ^2)) * c)) + ((3 * a) * (c ^2))) + (c |^ 3)) - (((3 * (a ^2)) * c) + ((3 * a) * (c ^2))) by Lm6; ( a * ((b ^2) + (c ^2)) >= a * ((2 * b) * c) & b * ((a ^2) + (c ^2)) >= b * ((2 * a) * c) ) by Th6, XREAL_1:64; then A2: (b * ((a ^2) + (c ^2))) + (a * ((b ^2) + (c ^2))) >= (((2 * a) * b) * c) + (((2 * a) * b) * c) by XREAL_1:7; ((a + c) ^2) * (a + c) >= ((4 * a) * c) * (a + c) by Th9, XREAL_1:64; then ((a + c) |^ 2) * (a + c) >= ((4 * a) * c) * (a + c) by Lm1; then A3: (a + c) |^ (2 + 1) >= ((4 * a) * c) * (a + c) by NEWTON:6; ((b + c) ^2) * (b + c) >= ((4 * b) * c) * (b + c) by Th9, XREAL_1:64; then ((b + c) |^ 2) * (b + c) >= ((4 * b) * c) * (b + c) by Lm1; then A4: (b + c) |^ (2 + 1) >= ((4 * b) * c) * (b + c) by NEWTON:6; ((a + b) ^2) * (a + b) >= ((4 * a) * b) * (a + b) by Th9, XREAL_1:64; then ((a + b) |^ 2) * (a + b) >= ((4 * a) * b) * (a + b) by Lm1; then (a + b) |^ (2 + 1) >= ((4 * a) * b) * (a + b) by NEWTON:6; then ((a + b) |^ 3) + ((b + c) |^ 3) >= (((4 * (a ^2)) * b) + ((4 * a) * (b ^2))) + (((4 * (b ^2)) * c) + ((4 * b) * (c ^2))) by A4, XREAL_1:7; then (((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3) >= (((((4 * (a ^2)) * b) + ((4 * a) * (b ^2))) + ((4 * (b ^2)) * c)) + ((4 * b) * (c ^2))) + (((4 * (a ^2)) * c) + ((4 * a) * (c ^2))) by A3, XREAL_1:7; then A5: ((((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3)) + ((((((- ((3 * (a ^2)) * b)) - ((3 * a) * (b ^2))) - ((3 * (b ^2)) * c)) - ((3 * b) * (c ^2))) - ((3 * (a ^2)) * c)) - ((3 * a) * (c ^2))) >= (((((((4 * (a ^2)) * b) + ((4 * a) * (b ^2))) + ((4 * (b ^2)) * c)) + ((4 * b) * (c ^2))) + ((4 * (a ^2)) * c)) + ((4 * a) * (c ^2))) + ((((((- ((3 * (a ^2)) * b)) - ((3 * a) * (b ^2))) - ((3 * (b ^2)) * c)) - ((3 * b) * (c ^2))) - ((3 * (a ^2)) * c)) - ((3 * a) * (c ^2))) by XREAL_1:6; c * ((a ^2) + (b ^2)) >= ((2 * a) * b) * c by Th6, XREAL_1:64; then A6: ((b * ((a ^2) + (c ^2))) + (a * ((b ^2) + (c ^2)))) + (c * ((a ^2) + (b ^2))) >= (((4 * a) * b) * c) + (((2 * a) * b) * c) by A2, XREAL_1:7; ( ((a + b) |^ 3) - (((3 * (a ^2)) * b) + ((3 * a) * (b ^2))) = ((((a |^ 3) + ((3 * (a ^2)) * b)) + ((3 * a) * (b ^2))) + (b |^ 3)) - (((3 * (a ^2)) * b) + ((3 * a) * (b ^2))) & ((b + c) |^ 3) - (((3 * (b ^2)) * c) + ((3 * b) * (c ^2))) = ((((b |^ 3) + ((3 * (b ^2)) * c)) + ((3 * b) * (c ^2))) + (c |^ 3)) - (((3 * (b ^2)) * c) + ((3 * b) * (c ^2))) ) by Lm6; then 2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3)) >= ((6 * a) * b) * c by A1, A5, A6, XXREAL_0:2; then (2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3))) / 2 >= (((6 * a) * b) * c) / 2 by XREAL_1:72; hence ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c ; ::_thesis: verum end; theorem Th13: :: SERIES_3:13 for a, b, c being real positive number holds (((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3 >= (a * b) * c proof let a, b, c be real positive number ; ::_thesis: (((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3 >= (a * b) * c (((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3 >= (((3 * a) * b) * c) / 3 by Th12, XREAL_1:72; hence (((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3 >= (a * b) * c ; ::_thesis: verum end; theorem :: SERIES_3:14 for a, b, c being real positive number holds (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c) proof let a, b, c be real positive number ; ::_thesis: (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c) A1: 1 = ((a / a) * 1) * 1 by XCMPLX_1:60 .= ((a / a) * (b / b)) * 1 by XCMPLX_1:60 .= ((a / a) * (b / b)) * (c / c) by XCMPLX_1:60 .= ((a / b) * (b / a)) * (c / c) .= (a / b) * ((b / a) * (c / c)) .= (a / b) * ((b / c) * (c / a)) .= ((a / b) * (b / c)) * (c / a) ; c / b = (c / b) * 1 .= (c / b) * (a / a) by XCMPLX_1:60 .= ((a / b) * (c / a)) * 1 ; then A2: c / b <= ((((a / b) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3 by Th13; a / c = (a / c) * 1 .= (a / c) * (b / b) by XCMPLX_1:60 .= ((a / b) * (b / c)) * 1 ; then A3: a / c <= ((((a / b) |^ 3) + ((b / c) |^ 3)) + (1 |^ 3)) / 3 by Th13; b / a = (b / a) * 1 .= (b / a) * (c / c) by XCMPLX_1:60 .= ((b / c) * (c / a)) * 1 ; then b / a <= ((((b / c) |^ 3) + ((c / a) |^ 3)) + (1 |^ 3)) / 3 by Th13; then (b / a) + (c / b) <= (((((b / c) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3)) + (((((a / b) |^ 3) / 3) + (((c / a) |^ 3) / 3)) + (1 / 3)) by A2, Lm2, XREAL_1:7; then A4: ((b / a) + (c / b)) + (a / c) <= ((((((b / c) |^ 3) / 3) + (((a / b) |^ 3) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + (2 / 3)) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (1 / 3)) by A3, Lm2, XREAL_1:7; ((a / b) * (b / c)) * (c / a) <= ((((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3)) / 3 by Th13; then (((b / a) + (c / b)) + (a / c)) + 1 <= (((((2 * ((b / c) |^ 3)) / 3) + ((2 * ((a / b) |^ 3)) / 3)) + ((2 * ((c / a) |^ 3)) / 3)) + 1) + (((((a / b) |^ 3) / 3) + (((b / c) |^ 3) / 3)) + (((c / a) |^ 3) / 3)) by A1, A4, XREAL_1:7; then ((((b / a) + (c / b)) + (a / c)) + 1) - 1 <= (((((b / c) |^ 3) + ((a / b) |^ 3)) + ((c / a) |^ 3)) + 1) - 1 by XREAL_1:9; hence (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c) ; ::_thesis: verum end; theorem Th15: :: SERIES_3:15 for a, b, c being real positive number holds (a + b) + c >= 3 * (3 -root ((a * b) * c)) proof let a, b, c be real positive number ; ::_thesis: (a + b) + c >= 3 * (3 -root ((a * b) * c)) A1: 3 -Root c > 0 by PREPOWER:def_2; ( 3 -Root a > 0 & 3 -Root b > 0 ) by PREPOWER:def_2; then (((3 -Root a) |^ 3) + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by A1, Th12; then (a + ((3 -Root b) |^ 3)) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by PREPOWER:19; then (a + b) + ((3 -Root c) |^ 3) >= ((3 * (3 -Root a)) * (3 -Root b)) * (3 -Root c) by PREPOWER:19; then (a + b) + c >= (3 * ((3 -Root a) * (3 -Root b))) * (3 -Root c) by PREPOWER:19; then (a + b) + c >= (3 * (3 -Root (a * b))) * (3 -Root c) by PREPOWER:22; then (a + b) + c >= 3 * ((3 -Root (a * b)) * (3 -Root c)) ; then (a + b) + c >= 3 * (3 -Root ((a * b) * c)) by PREPOWER:22; hence (a + b) + c >= 3 * (3 -root ((a * b) * c)) by POWER:def_1; ::_thesis: verum end; theorem :: SERIES_3:16 for a, b, c being real positive number holds ((a + b) + c) / 3 >= 3 -root ((a * b) * c) proof let a, b, c be real positive number ; ::_thesis: ((a + b) + c) / 3 >= 3 -root ((a * b) * c) ((a + b) + c) / 3 >= (3 * (3 -root ((a * b) * c))) / 3 by Th15, XREAL_1:72; hence ((a + b) + c) / 3 >= 3 -root ((a * b) * c) ; ::_thesis: verum end; theorem :: SERIES_3:17 for x, y, z being real number st (x + y) + z = 1 holds ((x * y) + (y * z)) + (x * z) <= 1 / 3 proof let x, y, z be real number ; ::_thesis: ( (x + y) + z = 1 implies ((x * y) + (y * z)) + (x * z) <= 1 / 3 ) ( (x ^2) + (y ^2) >= (2 * x) * y & (x ^2) + (z ^2) >= (2 * x) * z ) by Th6; then A1: ((x ^2) + (y ^2)) + ((x ^2) + (z ^2)) >= ((2 * x) * y) + ((2 * x) * z) by XREAL_1:7; (y ^2) + (z ^2) >= (2 * y) * z by Th6; then ((((x ^2) + (y ^2)) + (x ^2)) + (z ^2)) + ((y ^2) + (z ^2)) >= (((2 * x) * y) + ((2 * x) * z)) + ((2 * y) * z) by A1, XREAL_1:7; then (2 * (((x ^2) + (y ^2)) + (z ^2))) / 2 >= (2 * (((x * y) + (x * z)) + (y * z))) / 2 by XREAL_1:72; then A2: (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * z) + (y * z)) + (x * y))) >= (((x * y) + (x * z)) + (y * z)) + (2 * (((x * z) + (y * z)) + (x * y))) by XREAL_1:7; assume (x + y) + z = 1 ; ::_thesis: ((x * y) + (y * z)) + (x * z) <= 1 / 3 then 1 ^2 = (((x + y) ^2) + ((2 * (x + y)) * z)) + (z ^2) by SQUARE_1:4 .= (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * z) + (y * z)) + (x * y))) ; then 1 / 3 >= (3 * (((x * z) + (y * z)) + (x * y))) / 3 by A2, XREAL_1:72; hence ((x * y) + (y * z)) + (x * z) <= 1 / 3 ; ::_thesis: verum end; theorem Th18: :: SERIES_3:18 for x, y being real number st x + y = 1 holds x * y <= 1 / 4 proof let x, y be real number ; ::_thesis: ( x + y = 1 implies x * y <= 1 / 4 ) (x - y) ^2 >= 0 by XREAL_1:63; then A1: (((x ^2) - ((2 * x) * y)) + (y ^2)) - (((x ^2) + ((2 * x) * y)) + (y ^2)) >= 0 - (((x ^2) + ((2 * x) * y)) + (y ^2)) by XREAL_1:9; assume x + y = 1 ; ::_thesis: x * y <= 1 / 4 then 1 ^2 = ((x ^2) + ((2 * x) * y)) + (y ^2) by SQUARE_1:4; then - ((4 * x) * y) >= - 1 by A1; then 4 * (x * y) <= 1 by XREAL_1:24; then (4 * (x * y)) / 4 <= 1 / 4 by XREAL_1:72; hence x * y <= 1 / 4 ; ::_thesis: verum end; theorem :: SERIES_3:19 for x, y being real number st x + y = 1 holds (x ^2) + (y ^2) >= 1 / 2 proof let x, y be real number ; ::_thesis: ( x + y = 1 implies (x ^2) + (y ^2) >= 1 / 2 ) (x - y) ^2 >= 0 by XREAL_1:63; then A1: (((x ^2) - ((2 * x) * y)) + (y ^2)) + (((x ^2) + ((2 * x) * y)) + (y ^2)) >= 0 + (((x ^2) + ((2 * x) * y)) + (y ^2)) by XREAL_1:7; assume x + y = 1 ; ::_thesis: (x ^2) + (y ^2) >= 1 / 2 then 1 ^2 = ((x ^2) + ((2 * x) * y)) + (y ^2) by SQUARE_1:4; then (2 * ((x ^2) + (y ^2))) / 2 >= 1 / 2 by A1, XREAL_1:72; hence (x ^2) + (y ^2) >= 1 / 2 ; ::_thesis: verum end; theorem :: SERIES_3:20 for a, b being real positive number st a + b = 1 holds (1 + (1 / a)) * (1 + (1 / b)) >= 9 proof let a, b be real positive number ; ::_thesis: ( a + b = 1 implies (1 + (1 / a)) * (1 + (1 / b)) >= 9 ) assume A1: a + b = 1 ; ::_thesis: (1 + (1 / a)) * (1 + (1 / b)) >= 9 then 1 / (a * b) >= 1 / (1 / 4) by Th18, XREAL_1:85; then (1 / (a * b)) * (- 2) <= 4 * (- 2) by XREAL_1:65; then - ((1 / (a * b)) * 2) <= - 8 ; then (1 / (a * b)) * 2 >= 8 by XREAL_1:24; then A2: 1 + (2 * (1 / (a * b))) >= 1 + 8 by XREAL_1:7; (1 + (1 / a)) * (1 + (1 / b)) = (((1 * 1) + (1 * (1 / b))) + ((1 / a) * (1 / b))) + ((1 / a) * 1) .= ((1 + (1 / b)) + (1 / (a * b))) + (1 / a) by XCMPLX_1:102 .= (1 + ((1 / b) + (1 / a))) + (1 / (a * b)) .= (1 + (((1 * a) + (b * 1)) / (a * b))) + (1 / (a * b)) by XCMPLX_1:116 .= (1 + (1 / (a * b))) + (1 / (a * b)) by A1 .= 1 + (2 * (1 / (a * b))) ; hence (1 + (1 / a)) * (1 + (1 / b)) >= 9 by A2; ::_thesis: verum end; theorem :: SERIES_3:21 for x, y being real number st x + y = 1 holds (x |^ 3) + (y |^ 3) >= 1 / 4 proof let x, y be real number ; ::_thesis: ( x + y = 1 implies (x |^ 3) + (y |^ 3) >= 1 / 4 ) assume A1: x + y = 1 ; ::_thesis: (x |^ 3) + (y |^ 3) >= 1 / 4 then (x * y) * (- 3) >= (1 / 4) * (- 3) by Th18, XREAL_1:65; then A2: 1 + ((x * y) * (- 3)) >= ((1 / 4) * (- 3)) + 1 by XREAL_1:7; (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) by Lm7; then (x |^ 3) + (y |^ 3) = (((x ^2) + ((2 * x) * y)) + (y ^2)) - ((3 * x) * y) by A1 .= (1 ^2) - (3 * (x * y)) by A1, SQUARE_1:4 ; hence (x |^ 3) + (y |^ 3) >= 1 / 4 by A2; ::_thesis: verum end; theorem :: SERIES_3:22 for a, b being real positive number st a + b = 1 holds (a |^ 3) + (b |^ 3) < 1 proof let a, b be real positive number ; ::_thesis: ( a + b = 1 implies (a |^ 3) + (b |^ 3) < 1 ) assume A1: a + b = 1 ; ::_thesis: (a |^ 3) + (b |^ 3) < 1 A2: 1 + ((a * b) * (- 3)) < 0 + 1 by XREAL_1:8; (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) by Lm7; then (a |^ 3) + (b |^ 3) = (((a ^2) + ((2 * a) * b)) + (b ^2)) - ((3 * a) * b) by A1 .= (1 ^2) - (3 * (a * b)) by A1, SQUARE_1:4 ; hence (a |^ 3) + (b |^ 3) < 1 by A2; ::_thesis: verum end; theorem :: SERIES_3:23 for a, b being real positive number st a + b = 1 holds (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 proof let a, b be real positive number ; ::_thesis: ( a + b = 1 implies (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 ) assume A1: a + b = 1 ; ::_thesis: (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 then A2: a * b <= (1 / 2) ^2 by Th4; then 1 - (a * b) >= 1 - (1 / 4) by XREAL_1:10; then (1 - (a * b)) ^2 >= (3 / 4) ^2 by SQUARE_1:15; then 1 + ((1 - (a * b)) ^2) >= 1 + (9 / 16) by XREAL_1:6; then A3: 4 * (1 + ((1 - (a * b)) ^2)) >= 4 * (25 / 16) by XREAL_1:64; (1 - (a * b)) ^2 >= 0 by XREAL_1:63; then A4: (1 + ((1 - (a * b)) ^2)) / (a * b) >= (1 + ((1 - (a * b)) ^2)) / (1 / 4) by A2, XREAL_1:118; (a ^2) + (b ^2) = (((a ^2) + ((2 * a) * b)) + (b ^2)) - ((2 * a) * b) ; then A5: (a ^2) + (b ^2) = (1 ^2) - ((2 * a) * b) by A1, SQUARE_1:4; (a + (1 / a)) * (b + (1 / b)) = ((1 + (a ^2)) / a) * (b + (1 / b)) by XCMPLX_1:113 .= ((1 + (a ^2)) / a) * ((1 + (b ^2)) / b) by XCMPLX_1:113 .= ((1 + (a ^2)) * (1 + (b ^2))) / (a * b) by XCMPLX_1:76 .= (1 + (((1 ^2) - (2 * (a * b))) + ((a ^2) * (b ^2)))) / (a * b) by A5 .= (1 + ((1 - (a * b)) ^2)) / (a * b) ; hence (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 by A4, A3, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_3:24 for x, a being real number st abs x <= a holds x ^2 <= a ^2 proof let x, a be real number ; ::_thesis: ( abs x <= a implies x ^2 <= a ^2 ) assume A1: abs x <= a ; ::_thesis: x ^2 <= a ^2 percases ( x >= 0 or x < 0 ) ; supposeA2: x >= 0 ; ::_thesis: x ^2 <= a ^2 x <= a by A1, ABSVALUE:def_1; hence x ^2 <= a ^2 by A2, SQUARE_1:15; ::_thesis: verum end; supposeA3: x < 0 ; ::_thesis: x ^2 <= a ^2 then - x <= a by A1, ABSVALUE:def_1; then (- x) ^2 <= a ^2 by A3, SQUARE_1:15; hence x ^2 <= a ^2 ; ::_thesis: verum end; end; end; theorem :: SERIES_3:25 for a being real positive number for x being real number st abs x >= a holds x ^2 >= a ^2 proof let a be real positive number ; ::_thesis: for x being real number st abs x >= a holds x ^2 >= a ^2 let x be real number ; ::_thesis: ( abs x >= a implies x ^2 >= a ^2 ) assume A1: abs x >= a ; ::_thesis: x ^2 >= a ^2 percases ( x >= 0 or x < 0 ) ; suppose x >= 0 ; ::_thesis: x ^2 >= a ^2 then x >= a by A1, ABSVALUE:def_1; hence x ^2 >= a ^2 by SQUARE_1:15; ::_thesis: verum end; suppose x < 0 ; ::_thesis: x ^2 >= a ^2 then - x >= a by A1, ABSVALUE:def_1; then (- x) ^2 >= a ^2 by SQUARE_1:15; hence x ^2 >= a ^2 ; ::_thesis: verum end; end; end; theorem :: SERIES_3:26 for x, y being real number holds abs ((abs x) - (abs y)) <= (abs x) + (abs y) proof let x, y be real number ; ::_thesis: abs ((abs x) - (abs y)) <= (abs x) + (abs y) ( abs ((abs x) - (abs y)) <= abs (x - y) & abs (x - y) <= (abs x) + (abs y) ) by COMPLEX1:57, COMPLEX1:64; hence abs ((abs x) - (abs y)) <= (abs x) + (abs y) by XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_3:27 for a, b, c being real positive number st (a * b) * c = 1 holds ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c) proof let a, b, c be real positive number ; ::_thesis: ( (a * b) * c = 1 implies ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c) ) assume A1: (a * b) * c = 1 ; ::_thesis: ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c) ((1 / a) + (1 / b)) / 2 >= sqrt ((1 / a) * (1 / b)) by Th2; then ((1 / a) + (1 / b)) / 2 >= sqrt (1 / (a * b)) by XCMPLX_1:102; then A2: ((1 / a) + (1 / b)) / 2 >= sqrt ((1 * c) / ((a * b) * c)) by XCMPLX_1:91; ((1 / c) + (1 / a)) / 2 >= sqrt ((1 / c) * (1 / a)) by Th2; then ((1 / c) + (1 / a)) / 2 >= sqrt (1 / (c * a)) by XCMPLX_1:102; then A3: ((1 / c) + (1 / a)) / 2 >= sqrt ((1 * b) / ((c * a) * b)) by XCMPLX_1:91; ((1 / b) + (1 / c)) / 2 >= sqrt ((1 / b) * (1 / c)) by Th2; then ((1 / b) + (1 / c)) / 2 >= sqrt (1 / (b * c)) by XCMPLX_1:102; then ((1 / b) + (1 / c)) / 2 >= sqrt ((1 * a) / ((b * c) * a)) by XCMPLX_1:91; then (((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2) >= (sqrt a) + (sqrt b) by A1, A3, XREAL_1:7; then ((((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2)) + (((1 / a) + (1 / b)) / 2) >= ((sqrt a) + (sqrt b)) + (sqrt c) by A1, A2, XREAL_1:7; hence ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c) ; ::_thesis: verum end; theorem :: SERIES_3:28 for x, y, z being real number st x > 0 & y > 0 & z < 0 & (x + y) + z = 0 holds (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) proof let x, y, z be real number ; ::_thesis: ( x > 0 & y > 0 & z < 0 & (x + y) + z = 0 implies (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) ) assume that A1: ( x > 0 & y > 0 ) and A2: z < 0 and A3: (x + y) + z = 0 ; ::_thesis: (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) 3 -Root ((((x ^2) * (y ^2)) * (z ^2)) / 4) > 0 by A1, A2, PREPOWER:def_2; then A4: 3 -root ((((x ^2) * (y ^2)) * (z ^2)) / 4) > 0 by A1, A2, POWER:def_1; (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x * (x + y)) / 2) * ((y * (x + y)) / 2)) * (x * y))) by A1, Th15; then (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x ^2) * (y ^2)) * ((x + y) * (x + y))) / 4)) ; then A5: (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x ^2) * (y ^2)) * ((- z) ^2)) / 4)) by A3; (3 * (3 -root ((((x ^2) * (y ^2)) * (z ^2)) / 4))) |^ 3 = (3 |^ 3) * ((3 -root ((((x ^2) * (y ^2)) * (z ^2)) / 4)) |^ 3) by NEWTON:7 .= 27 * ((3 -Root ((((x ^2) * (y ^2)) * (z ^2)) / 4)) |^ 3) by A1, A2, Lm4, POWER:def_1 .= 27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4) by A1, A2, PREPOWER:19 ; then ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 >= 27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4) by A5, A4, PREPOWER:9; then A6: 8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) >= 8 * (27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4)) by XREAL_1:64; ((x ^2) + (y ^2)) / 2 >= x * y by Th7; then ((x |^ 2) + (y ^2)) / 2 >= x * y by Lm1; then ((x |^ 2) + (y |^ 2)) / 2 >= x * y by Lm1; then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y) by XREAL_1:6; then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x ^2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y) by Lm1; then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x * x) + (x * y)) / 2) + (((x * y) + (y ^2)) / 2)) + (x * y) by Lm1; then (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3 >= ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 by A1, PREPOWER:9; then 8 * ((((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3) >= 8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) by XREAL_1:64; then 8 * ((((x |^ 2) + (x * y)) + (y |^ 2)) |^ 3) >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by A6, XXREAL_0:2; then (2 * (((x |^ 2) + (x * y)) + (y |^ 2))) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by Lm3, NEWTON:7; then (((((x |^ 2) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) ; then (((((x ^2) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by Lm1; then (((((x ^2) + ((2 * x) * y)) + (y |^ 2)) + (x ^2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by Lm1; then (((((x ^2) + ((2 * x) * y)) + (y ^2)) + (x ^2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by Lm1; then A7: (((((x ^2) + ((2 * x) * y)) + (y ^2)) + (x ^2)) + (y ^2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2)) by Lm1; A8: z = - (x + y) by A3; then z |^ 3 = - ((x + y) |^ 3) by Lm5 .= - ((((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3)) by Lm6 ; then (((z |^ 2) + (x ^2)) + (y ^2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) by A8, A7, Lm1; then (((z |^ 2) + (x |^ 2)) + (y ^2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) by Lm1; then (((z |^ 2) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) by Lm1; hence (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2) ; ::_thesis: verum end; theorem :: SERIES_3:29 for a, b, c being real positive number st a >= 1 holds (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) proof let a, b, c be real positive number ; ::_thesis: ( a >= 1 implies (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) ) A1: (b + c) / 2 >= (2 * (sqrt (b * c))) / 2 by SIN_COS2:1, XREAL_1:72; set p = a to_power c; set o = a to_power b; ( a to_power b > 0 & a to_power c > 0 ) by POWER:34; then (a to_power b) + (a to_power c) >= 2 * (sqrt ((a to_power b) * (a to_power c))) by SIN_COS2:1; then ( a to_power (b + c) > 0 & (a to_power b) + (a to_power c) >= 2 * (sqrt (a to_power (b + c))) ) by POWER:27, POWER:34; then (a to_power b) + (a to_power c) >= 2 * ((a to_power (b + c)) to_power (1 / 2)) by ASYMPT_1:83; then A2: (a to_power b) + (a to_power c) >= 2 * (a to_power ((1 / 2) * (b + c))) by POWER:33; assume a >= 1 ; ::_thesis: (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) then a #R ((b + c) / 2) >= a #R (sqrt (b * c)) by A1, PREPOWER:82; then a to_power ((b + c) / 2) >= a #R (sqrt (b * c)) by POWER:def_2; then a to_power ((b + c) / 2) >= a to_power (sqrt (b * c)) by POWER:def_2; then 2 * (a to_power ((b + c) / 2)) >= 2 * (a to_power (sqrt (b * c))) by XREAL_1:64; hence (a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c))) by A2, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_3:30 for a, b, c being real positive number st a >= b & b >= c holds ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) proof let a, b, c be real positive number ; ::_thesis: ( a >= b & b >= c implies ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) ) assume that A1: a >= b and A2: b >= c ; ::_thesis: ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) A3: (b / c) to_power ((b - c) / 3) = (b / c) #R ((b - c) / 3) by POWER:def_2; ( b / c >= 1 & b - c >= c - c ) by A2, XREAL_1:9, XREAL_1:181; then A4: (b / c) to_power ((b - c) / 3) >= 1 by A3, PREPOWER:85; A5: (a / b) to_power ((a - b) / 3) = (a / b) #R ((a - b) / 3) by POWER:def_2; ( a / b >= 1 & a - b >= b - b ) by A1, XREAL_1:9, XREAL_1:181; then (a / b) to_power ((a - b) / 3) >= 1 by A5, PREPOWER:85; then A6: ((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3)) >= 1 * 1 by A4, XREAL_1:66; a >= c by A1, A2, XXREAL_0:2; then A7: ( a / c >= 1 & a - c >= c - c ) by XREAL_1:9, XREAL_1:181; (a / c) to_power ((a - c) / 3) = (a / c) #R ((a - c) / 3) by POWER:def_2; then (a / c) to_power ((a - c) / 3) >= 1 by A7, PREPOWER:85; then (((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3)) >= 1 by A6, XREAL_1:66; then (((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3)) >= 1 by POWER:31; then A8: (((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a / c) to_power ((a - c) / 3)) >= 1 by POWER:31; set t = b to_power (((a + b) + c) / 3); set s = b to_power b; set r = c to_power (((a + b) + c) / 3); set q = c to_power c; set p = a to_power (((a + b) + c) / 3); set o = a to_power a; set j = c to_power ((a - c) / 3); set i = a to_power ((a - c) / 3); set h = c to_power ((b - c) / 3); set w = b to_power ((b - c) / 3); set v = b to_power ((a - b) / 3); set u = a to_power ((a - b) / 3); A9: ( a to_power (((a + b) + c) / 3) > 0 & c to_power (((a + b) + c) / 3) > 0 ) by POWER:34; A10: b to_power (((a + b) + c) / 3) > 0 by POWER:34; (((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a to_power ((a - c) / 3)) / (c to_power ((a - c) / 3))) = (((a to_power ((a - b) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * (c to_power ((b - c) / 3)))) * ((a to_power ((a - c) / 3)) / (c to_power ((a - c) / 3))) by XCMPLX_1:76 .= (((a to_power ((a - b) / 3)) * (b to_power ((b - c) / 3))) * (a to_power ((a - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((b - c) / 3))) * (c to_power ((a - c) / 3))) by XCMPLX_1:76 .= (((a to_power ((a - b) / 3)) * (a to_power ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3))) .= ((a to_power (((a - b) / 3) + ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3))) by POWER:27 .= ((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * ((c to_power ((a - c) / 3)) * (c to_power ((b - c) / 3)))) .= ((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * (c to_power (((a - c) / 3) + ((b - c) / 3)))) by POWER:27 .= ((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * ((b to_power ((b - c) / 3)) / (b to_power ((a - b) / 3))) by XCMPLX_1:76 .= ((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power (((b - c) / 3) - ((a - b) / 3))) by POWER:29 .= ((1 / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3)) .= ((c to_power (- (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3)) by POWER:28 .= ((a to_power (((3 * a) / 3) - (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3))) .= (((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3))) by POWER:29 .= (((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * ((c to_power ((3 * c) / 3)) / (c to_power (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3))) by POWER:29 .= (((a to_power a) / (a to_power (((a + b) + c) / 3))) * ((c to_power c) / (c to_power (((a + b) + c) / 3)))) * ((b to_power b) / (b to_power (((a + b) + c) / 3))) by POWER:29 .= (((a to_power a) * (c to_power c)) / ((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3)))) * ((b to_power b) / (b to_power (((a + b) + c) / 3))) by XCMPLX_1:76 .= (((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) by XCMPLX_1:76 ; then (((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) >= 1 by A8, POWER:31; then ((((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)))) * (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) >= 1 * (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) by A9, A10, XREAL_1:64; then ((a to_power a) * (c to_power c)) * (b to_power b) >= ((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)) by A9, A10, XCMPLX_1:87; then ((a to_power a) * (c to_power c)) * (b to_power b) >= ((a * c) to_power (((a + b) + c) / 3)) * (b to_power (((a + b) + c) / 3)) by POWER:30; then (a to_power a) * ((b to_power b) * (c to_power c)) >= ((a * c) * b) to_power (((a + b) + c) / 3) by POWER:30; hence ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) ; ::_thesis: verum end; theorem Th31: :: SERIES_3:31 for n being Element of NAT for a, b being real non negative number holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) proof let n be Element of NAT ; ::_thesis: for a, b being real non negative number holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) let a, b be real non negative number ; ::_thesis: (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) defpred S1[ Element of NAT ] means (a + b) |^ (\$1 + 2) >= (a |^ (\$1 + 2)) + (((\$1 + 2) * (a |^ (\$1 + 1))) * b); A1: 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] ) a |^ (n + 1) >= 0 proof percases ( a = 0 or a > 0 ) ; suppose a = 0 ; ::_thesis: a |^ (n + 1) >= 0 hence a |^ (n + 1) >= 0 ; ::_thesis: verum end; suppose a > 0 ; ::_thesis: a |^ (n + 1) >= 0 hence a |^ (n + 1) >= 0 by PREPOWER:6; ::_thesis: verum end; end; end; then A2: (a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b) <= (((n + 2) * (a |^ (n + 1))) * (b ^2)) + ((a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b)) by XREAL_1:31; assume (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) ; ::_thesis: S1[n + 1] then ((a + b) |^ (n + 2)) * (a + b) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b) by XREAL_1:64; then (a + b) |^ ((n + 2) + 1) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b) by NEWTON:6; then (a + b) |^ (n + 3) >= (((a |^ (n + 2)) * a) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b) ; then (a + b) |^ (n + 3) >= ((a |^ ((n + 2) + 1)) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b) by NEWTON:6; then (a + b) |^ (n + 3) >= (((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a * (a |^ (n + 1)))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b)) ; then (a + b) |^ (n + 3) >= (((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a |^ ((n + 1) + 1))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b)) by NEWTON:6; hence S1[n + 1] by A2, XXREAL_0:2; ::_thesis: verum end; A3: (a |^ (0 + 2)) + (((0 + 2) * (a |^ (0 + 1))) * b) = (a ^2) + ((2 * (a |^ 1)) * b) by Lm1 .= (a ^2) + ((2 * a) * b) by NEWTON:5 ; (a + b) |^ (0 + 2) = (a + b) ^2 by Lm1 .= ((a ^2) + ((2 * a) * b)) + (b ^2) ; then A4: S1[ 0 ] by A3, XREAL_1:31; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); hence (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) ; ::_thesis: verum end; theorem :: SERIES_3:32 for a, b being real positive number for n being Element of NAT holds ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n proof let a, b be real positive number ; ::_thesis: for n being Element of NAT holds ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n let n be Element of NAT ; ::_thesis: ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n defpred S1[ Element of NAT ] means ((a |^ \$1) + (b |^ \$1)) / 2 >= ((a + b) / 2) |^ \$1; A1: 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 S1[n] ; ::_thesis: S1[n + 1] then A2: (((a |^ n) + (b |^ n)) / 2) * (a + b) >= (((a + b) / 2) |^ n) * (a + b) by XREAL_1:64; percases ( a - b >= 0 or a - b < 0 ) ; supposeA3: a - b >= 0 ; ::_thesis: S1[n + 1] then (a - b) + b >= 0 + b by XREAL_1:6; then a |^ n >= b |^ n by PREPOWER:9; then (a |^ n) - (b |^ n) >= 0 by XREAL_1:48; then (a - b) * ((a |^ n) - (b |^ n)) >= 0 by A3; then (((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 ; then ((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 by NEWTON:6; then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b) >= 0 ; then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1)) >= 0 by NEWTON:6; then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a)) >= 0 + (((a |^ n) * b) + ((b |^ n) * a)) by XREAL_1:6; then ((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1))) by XREAL_1:6; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= (((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) ; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) by NEWTON:6; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:6; then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:72; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A2, XXREAL_0:2; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:8; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) * (a + b)) / (2 |^ n) ; then (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a + b) |^ (n + 1)) / (2 |^ n) by NEWTON:6; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:72; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:78; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:6; hence S1[n + 1] by PREPOWER:8; ::_thesis: verum end; supposeA4: a - b < 0 ; ::_thesis: S1[n + 1] then (a - b) + b < 0 + b by XREAL_1:6; then a |^ n <= b |^ n by PREPOWER:9; then (a |^ n) - (b |^ n) <= 0 by XREAL_1:47; then (a - b) * ((a |^ n) - (b |^ n)) >= 0 by A4; then (((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 ; then ((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 by NEWTON:6; then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b) >= 0 ; then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1)) >= 0 by NEWTON:6; then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a)) >= 0 + (((a |^ n) * b) + ((b |^ n) * a)) by XREAL_1:6; then ((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1))) by XREAL_1:6; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= (((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) ; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) by NEWTON:6; then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:6; then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:72; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A2, XXREAL_0:2; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:8; then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) * (a + b)) / (2 |^ n) ; then (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a + b) |^ (n + 1)) / (2 |^ n) by NEWTON:6; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:72; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:78; then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:6; hence S1[n + 1] by PREPOWER:8; ::_thesis: verum end; end; end; ((a |^ 0) + (b |^ 0)) / 2 = (1 + (b |^ 0)) / 2 by NEWTON:4 .= (1 + 1) / 2 by NEWTON:4 .= ((a + b) / 2) |^ 0 by NEWTON:4 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1); hence ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n ; ::_thesis: verum end; theorem Th33: :: SERIES_3:33 for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds for n being Element of NAT holds (Partial_Sums s) . n > 0 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n > 0 ) implies for n being Element of NAT holds (Partial_Sums s) . n > 0 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 > 0 ; assume A1: for n being Element of NAT holds s . n > 0 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n > 0 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: (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1; assume (Partial_Sums s) . n > 0 ; ::_thesis: S1[n + 1] hence S1[n + 1] by A1, A3, XREAL_1:34; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1; then A4: S1[ 0 ] by A1; 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 > 0 ; ::_thesis: verum end; theorem Th34: :: SERIES_3:34 for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 0 ) holds for n being Element of NAT holds (Partial_Sums s) . n >= 0 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n >= 0 ) implies for n being Element of NAT holds (Partial_Sums s) . n >= 0 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 >= 0 ; assume A1: for n being Element of NAT holds s . n >= 0 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n >= 0 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 A3: (Partial_Sums s) . n >= 0 ; ::_thesis: S1[n + 1] ( (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) & s . (n + 1) >= 0 ) by A1, SERIES_1:def_1; hence S1[n + 1] by A3; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1; then A4: S1[ 0 ] by A1; 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 >= 0 ; ::_thesis: verum end; theorem Th35: :: SERIES_3:35 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n < 0 ) holds (Partial_Sums s) . n < 0 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n < 0 ) holds (Partial_Sums s) . n < 0 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n < 0 ) implies (Partial_Sums s) . n < 0 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 < 0 ; assume A1: for n being Element of NAT holds s . n < 0 ; ::_thesis: (Partial_Sums s) . n < 0 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 A3: (Partial_Sums s) . n < 0 ; ::_thesis: S1[n + 1] ( (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) & s . (n + 1) < 0 ) by A1, SERIES_1:def_1; hence S1[n + 1] by A3; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1; then A4: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Sums s) . n < 0 ; ::_thesis: verum end; theorem Th36: :: SERIES_3:36 for s, s1 being Real_Sequence st s = s1 (#) s1 holds for n being Element of NAT holds (Partial_Sums s) . n >= 0 proof let s, s1 be Real_Sequence; ::_thesis: ( s = s1 (#) s1 implies for n being Element of NAT holds (Partial_Sums s) . n >= 0 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 >= 0 ; assume A1: s = s1 (#) s1 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n >= 0 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 A3: (Partial_Sums s) . n >= 0 ; ::_thesis: S1[n + 1] A4: (s1 . (n + 1)) ^2 >= 0 by XREAL_1:63; (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1 .= ((Partial_Sums s) . n) + ((s1 . (n + 1)) ^2) by A1, SEQ_1:8 ; hence S1[n + 1] by A3, A4; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (s1 . 0) ^2 by A1, SEQ_1:8 ; then A5: S1[ 0 ] by XREAL_1:63; 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 >= 0 ; ::_thesis: verum end; theorem :: SERIES_3:37 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n > s . (n - 1) ) ) holds (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n > s . (n - 1) ) ) holds (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s . n > s . (n - 1) ) ) implies (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n ) defpred S1[ Element of NAT ] means (\$1 + 1) * (s . (\$1 + 1)) > (Partial_Sums s) . \$1; assume A1: for n being Element of NAT holds ( s . n > 0 & s . n > s . (n - 1) ) ; ::_thesis: (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n ; ::_thesis: S1[n + 1] then A3: ((Partial_Sums s) . n) + (s . (n + 1)) < ((n + 1) * (s . (n + 1))) + (s . (n + 1)) by XREAL_1:6; s . (n + 2) > s . ((n + 2) - 1) by A1; then (n + 2) * (s . (n + 2)) > (n + 2) * (s . (n + 1)) by XREAL_1:68; then ((Partial_Sums s) . n) + (s . (n + 1)) < (n + 2) * (s . (n + 2)) by A3, XXREAL_0:2; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; s . 1 > s . (1 - 1) by A1; then A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (n + 1) * (s . (n + 1)) > (Partial_Sums s) . n ; ::_thesis: verum end; theorem Th38: :: SERIES_3:38 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) implies (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n ) defpred S1[ Element of NAT ] means (\$1 + 1) * (s . (\$1 + 1)) >= (Partial_Sums s) . \$1; assume A1: for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ; ::_thesis: (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n ; ::_thesis: S1[n + 1] then A3: ((Partial_Sums s) . n) + (s . (n + 1)) <= ((n + 1) * (s . (n + 1))) + (s . (n + 1)) by XREAL_1:6; s . (n + 2) >= s . ((n + 2) - 1) by A1; then (n + 2) * (s . (n + 2)) >= (n + 2) * (s . (n + 1)) by XREAL_1:64; then ((Partial_Sums s) . n) + (s . (n + 1)) <= (n + 2) * (s . (n + 2)) by A3, XXREAL_0:2; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; s . 1 >= s . (1 - 1) by A1; then A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n ; ::_thesis: verum end; theorem :: SERIES_3:39 for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ) holds for n being Element of NAT holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) proof let s, s1, s2 be Real_Sequence; ::_thesis: ( s = s1 (#) s2 & ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ) implies for n being Element of NAT holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ) assume that A1: s = s1 (#) s2 and A2: for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 <= ((Partial_Sums s1) . \$1) * ((Partial_Sums s2) . \$1); A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set j = (Partial_Sums s) . n; set u = (Partial_Sums s1) . n; set v = (Partial_Sums s2) . n; set w = s1 . (n + 1); set h = s2 . (n + 1); A4: ((Partial_Sums s1) . (n + 1)) * ((Partial_Sums s2) . (n + 1)) = (((Partial_Sums s1) . n) + (s1 . (n + 1))) * ((Partial_Sums s2) . (n + 1)) by SERIES_1:def_1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) * (((Partial_Sums s2) . n) + (s2 . (n + 1))) by SERIES_1:def_1 .= (((((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + (((Partial_Sums s1) . n) * (s2 . (n + 1)))) + ((s1 . (n + 1)) * ((Partial_Sums s2) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1))) ; assume (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ; ::_thesis: S1[n + 1] then A5: ((Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= (((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1))) by XREAL_1:6; A6: ( s1 . (n + 1) >= 0 & s2 . (n + 1) >= 0 ) by A2; ( (Partial_Sums s1) . n >= 0 & (Partial_Sums s2) . n >= 0 ) by A2, Th34; then A7: (((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= ((((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1)))) + ((((Partial_Sums s1) . n) * (s2 . (n + 1))) + ((s1 . (n + 1)) * ((Partial_Sums s2) . n))) by A6, XREAL_1:31; (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1 .= ((Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) by A1, SEQ_1:8 ; hence S1[n + 1] by A4, A5, A7, XXREAL_0:2; ::_thesis: verum end; A8: ((Partial_Sums s1) . 0) * ((Partial_Sums s2) . 0) = (s1 . 0) * ((Partial_Sums s2) . 0) by SERIES_1:def_1 .= (s1 . 0) * (s2 . 0) by SERIES_1:def_1 ; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (s1 . 0) * (s2 . 0) by A1, SEQ_1:8 ; then A9: S1[ 0 ] by A8; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A3); hence for n being Element of NAT holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ; ::_thesis: verum end; theorem :: SERIES_3:40 for n being Element of NAT for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Element of NAT holds ( s1 . n < 0 & s2 . n < 0 ) ) holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) proof let n be Element of NAT ; ::_thesis: for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Element of NAT holds ( s1 . n < 0 & s2 . n < 0 ) ) holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) let s, s1, s2 be Real_Sequence; ::_thesis: ( s = s1 (#) s2 & ( for n being Element of NAT holds ( s1 . n < 0 & s2 . n < 0 ) ) implies (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ) assume that A1: s = s1 (#) s2 and A2: for n being Element of NAT holds ( s1 . n < 0 & s2 . n < 0 ) ; ::_thesis: (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 <= ((Partial_Sums s1) . \$1) * ((Partial_Sums s2) . \$1); A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set j = (Partial_Sums s) . n; set u = (Partial_Sums s1) . n; set v = (Partial_Sums s2) . n; set w = s1 . (n + 1); set h = s2 . (n + 1); A4: ((Partial_Sums s1) . (n + 1)) * ((Partial_Sums s2) . (n + 1)) = (((Partial_Sums s1) . n) + (s1 . (n + 1))) * ((Partial_Sums s2) . (n + 1)) by SERIES_1:def_1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) * (((Partial_Sums s2) . n) + (s2 . (n + 1))) by SERIES_1:def_1 .= (((((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + (((Partial_Sums s1) . n) * (s2 . (n + 1)))) + ((s1 . (n + 1)) * ((Partial_Sums s2) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1))) ; assume (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ; ::_thesis: S1[n + 1] then A5: ((Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= (((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1))) by XREAL_1:6; A6: ( s1 . (n + 1) < 0 & s2 . (n + 1) < 0 ) by A2; ( (Partial_Sums s1) . n < 0 & (Partial_Sums s2) . n < 0 ) by A2, Th35; then A7: (((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= ((((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)) + ((s1 . (n + 1)) * (s2 . (n + 1)))) + ((((Partial_Sums s1) . n) * (s2 . (n + 1))) + ((s1 . (n + 1)) * ((Partial_Sums s2) . n))) by A6, XREAL_1:31; (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1 .= ((Partial_Sums s) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) by A1, SEQ_1:8 ; hence S1[n + 1] by A4, A5, A7, XXREAL_0:2; ::_thesis: verum end; A8: ((Partial_Sums s1) . 0) * ((Partial_Sums s2) . 0) = (s1 . 0) * ((Partial_Sums s2) . 0) by SERIES_1:def_1 .= (s1 . 0) * (s2 . 0) by SERIES_1:def_1 ; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= (s1 . 0) * (s2 . 0) by A1, SEQ_1:8 ; then A9: S1[ 0 ] by A8; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A3); hence (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n) ; ::_thesis: verum end; theorem Th41: :: SERIES_3:41 for s being Real_Sequence for n being Element of NAT holds abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n proof let s be Real_Sequence; ::_thesis: for n being Element of NAT holds abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n set s1 = abs s; defpred S1[ Element of NAT ] means abs ((Partial_Sums s) . \$1) <= (Partial_Sums (abs s)) . \$1; let n be Element of NAT ; ::_thesis: abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n A1: 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 abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ; ::_thesis: S1[n + 1] then A2: (abs ((Partial_Sums s) . n)) + (abs (s . (n + 1))) <= ((Partial_Sums (abs s)) . n) + (abs (s . (n + 1))) by XREAL_1:6; (Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + ((abs s) . (n + 1)) by SERIES_1:def_1; then A3: (Partial_Sums (abs s)) . (n + 1) = ((Partial_Sums (abs s)) . n) + (abs (s . (n + 1))) by SEQ_1:12; ( abs ((Partial_Sums s) . (n + 1)) = abs (((Partial_Sums s) . n) + (s . (n + 1))) & abs (((Partial_Sums s) . n) + (s . (n + 1))) <= (abs ((Partial_Sums s) . n)) + (abs (s . (n + 1))) ) by COMPLEX1:56, SERIES_1:def_1; hence S1[n + 1] by A3, A2, XXREAL_0:2; ::_thesis: verum end; (abs s) . 0 = abs (s . 0) by SEQ_1:12; then (Partial_Sums (abs s)) . 0 = abs (s . 0) by SERIES_1:def_1; then A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); hence abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ; ::_thesis: verum end; theorem :: SERIES_3:42 for n being Element of NAT for s being Real_Sequence holds (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence holds (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n let s be Real_Sequence; ::_thesis: (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n set s1 = abs s; ( (Partial_Sums s) . n <= abs ((Partial_Sums s) . n) & abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n ) by Th41, ABSVALUE:4; hence (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n by XXREAL_0:2; ::_thesis: verum end; definition let s be Real_Sequence; func Partial_Product s -> Real_Sequence means :Def1: :: SERIES_3:def 1 ( it . 0 = s . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) * (s . (n + 1)) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) ) proof deffunc H1( Nat, Real) -> Element of REAL = \$2 * (s . (\$1 + 1)); consider f being Function of NAT,REAL such that A1: ( f . 0 = s . 0 & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12(); reconsider f = f as Real_Sequence ; take f ; ::_thesis: ( f . 0 = s . 0 & ( for n being Element of NAT holds f . (n + 1) = (f . n) * (s . (n + 1)) ) ) thus ( f . 0 = s . 0 & ( for n being Element of NAT holds f . (n + 1) = (f . n) * (s . (n + 1)) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) holds b1 = b2 proof let s1, s2 be Real_Sequence; ::_thesis: ( s1 . 0 = s . 0 & ( for n being Element of NAT holds s1 . (n + 1) = (s1 . n) * (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Element of NAT holds s2 . (n + 1) = (s2 . n) * (s . (n + 1)) ) implies s1 = s2 ) assume that A2: s1 . 0 = s . 0 and A3: for n being Element of NAT holds s1 . (n + 1) = (s1 . n) * (s . (n + 1)) and A4: s2 . 0 = s . 0 and A5: for n being Element of NAT holds s2 . (n + 1) = (s2 . n) * (s . (n + 1)) ; ::_thesis: s1 = s2 defpred S1[ Element of NAT ] means s1 . \$1 = s2 . \$1; A6: 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 s1 . n = s2 . n ; ::_thesis: S1[n + 1] hence s1 . (n + 1) = (s2 . n) * (s . (n + 1)) by A3 .= s2 . (n + 1) by A5 ; ::_thesis: verum end; A7: S1[ 0 ] by A2, A4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); hence s1 = s2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines Partial_Product SERIES_3:def_1_:_ for s, b2 being Real_Sequence holds ( b2 = Partial_Product s iff ( b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) ) ); theorem Th43: :: SERIES_3:43 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds (Partial_Product s) . n > 0 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds (Partial_Product s) . n > 0 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n > 0 ) implies (Partial_Product s) . n > 0 ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 > 0 ; assume A1: for n being Element of NAT holds s . n > 0 ; ::_thesis: (Partial_Product s) . n > 0 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 A3: (Partial_Product s) . n > 0 ; ::_thesis: S1[n + 1] ( (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) & s . (n + 1) > 0 ) by A1, Def1; hence S1[n + 1] by A3; ::_thesis: verum end; s . 0 > 0 by A1; then A4: S1[ 0 ] by Def1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Product s) . n > 0 ; ::_thesis: verum end; theorem Th44: :: SERIES_3:44 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 0 ) holds (Partial_Product s) . n >= 0 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 0 ) holds (Partial_Product s) . n >= 0 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n >= 0 ) implies (Partial_Product s) . n >= 0 ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 >= 0 ; assume A1: for n being Element of NAT holds s . n >= 0 ; ::_thesis: (Partial_Product s) . n >= 0 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 A3: (Partial_Product s) . n >= 0 ; ::_thesis: S1[n + 1] ( (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) & s . (n + 1) >= 0 ) by A1, Def1; hence S1[n + 1] by A3; ::_thesis: verum end; s . 0 >= 0 by A1; then A4: S1[ 0 ] by Def1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Product s) . n >= 0 ; ::_thesis: verum end; theorem :: SERIES_3:45 for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n < 1 ) ) holds for n being Element of NAT holds ( (Partial_Product s) . n > 0 & (Partial_Product s) . n < 1 ) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s . n < 1 ) ) implies for n being Element of NAT holds ( (Partial_Product s) . n > 0 & (Partial_Product s) . n < 1 ) ) defpred S1[ Element of NAT ] means ( (Partial_Product s) . \$1 > 0 & (Partial_Product s) . \$1 < 1 ); assume A1: for n being Element of NAT holds ( s . n > 0 & s . n < 1 ) ; ::_thesis: for n being Element of NAT holds ( (Partial_Product s) . n > 0 & (Partial_Product s) . 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 A3: ( (Partial_Product s) . n > 0 & (Partial_Product s) . n < 1 ) ; ::_thesis: S1[n + 1] ( (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) & s . (n + 1) > 0 ) by A1, Def1; hence S1[n + 1] by A1, A3, XREAL_1:162; ::_thesis: verum end; (Partial_Product s) . 0 = s . 0 by Def1; then A4: S1[ 0 ] by A1; 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_Product s) . n > 0 & (Partial_Product s) . n < 1 ) ; ::_thesis: verum end; theorem :: SERIES_3:46 for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 1 ) holds for n being Element of NAT holds (Partial_Product s) . n >= 1 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n >= 1 ) implies for n being Element of NAT holds (Partial_Product s) . n >= 1 ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 >= 1; assume A1: for n being Element of NAT holds s . n >= 1 ; ::_thesis: for n being Element of NAT holds (Partial_Product s) . 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: (Partial_Product s) . (n + 1) = ((Partial_Product s) . n) * (s . (n + 1)) by Def1; assume A4: (Partial_Product s) . n >= 1 ; ::_thesis: S1[n + 1] then (Partial_Product s) . n <= ((Partial_Product s) . n) * (s . (n + 1)) by A1, XREAL_1:151; hence S1[n + 1] by A4, A3, XXREAL_0:2; ::_thesis: verum end; (Partial_Product s) . 0 = s . 0 by Def1; then A5: S1[ 0 ] by A1; 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_Product s) . n >= 1 ; ::_thesis: verum end; theorem :: SERIES_3:47 for s1, s2 being Real_Sequence st ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ) holds for n being Element of NAT holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n proof let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ) implies for n being Element of NAT holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n ) set s = s1 + s2; defpred S1[ Element of NAT ] means ((Partial_Product s1) . \$1) + ((Partial_Product s2) . \$1) <= (Partial_Product (s1 + s2)) . \$1; A1: (Partial_Product (s1 + s2)) . 0 = (s1 + s2) . 0 by Def1 .= (s1 . 0) + (s2 . 0) by SEQ_1:7 ; assume A2: for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 ) ; ::_thesis: for n being Element of NAT holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set u = (Partial_Product s1) . n; set v = (Partial_Product s2) . n; set w = (Partial_Product (s1 + s2)) . n; set h = s1 . (n + 1); set j = s2 . (n + 1); A4: ( s1 . (n + 1) >= 0 & s2 . (n + 1) >= 0 ) by A2; ( (Partial_Product s1) . n >= 0 & (Partial_Product s2) . n >= 0 ) by A2, Th44; then A5: (((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1))) <= ((((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1)))) + ((((Partial_Product s1) . n) * (s2 . (n + 1))) + (((Partial_Product s2) . n) * (s1 . (n + 1)))) by A4, XREAL_1:31; A6: (Partial_Product (s1 + s2)) . (n + 1) = ((Partial_Product (s1 + s2)) . n) * ((s1 + s2) . (n + 1)) by Def1 .= ((Partial_Product (s1 + s2)) . n) * ((s1 . (n + 1)) + (s2 . (n + 1))) by SEQ_1:7 ; assume ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n ; ::_thesis: S1[n + 1] then A7: (((Partial_Product s1) . n) + ((Partial_Product s2) . n)) * ((s1 . (n + 1)) + (s2 . (n + 1))) <= ((Partial_Product (s1 + s2)) . n) * ((s1 . (n + 1)) + (s2 . (n + 1))) by A4, XREAL_1:64; ((Partial_Product s1) . (n + 1)) + ((Partial_Product s2) . (n + 1)) = (((Partial_Product s1) . n) * (s1 . (n + 1))) + ((Partial_Product s2) . (n + 1)) by Def1 .= (((Partial_Product s1) . n) * (s1 . (n + 1))) + (((Partial_Product s2) . n) * (s2 . (n + 1))) by Def1 ; hence S1[n + 1] by A7, A6, A5, XXREAL_0:2; ::_thesis: verum end; ((Partial_Product s1) . 0) + ((Partial_Product s2) . 0) = (s1 . 0) + ((Partial_Product s2) . 0) by Def1 .= (s1 . 0) + (s2 . 0) by Def1 ; then A8: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A3); hence for n being Element of NAT holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n ; ::_thesis: verum end; theorem :: SERIES_3:48 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) implies (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) ) defpred S1[ Element of NAT ] means (Partial_Product s) . \$1 <= 1 / (sqrt ((3 * \$1) + 4)); assume A1: for n being Element of NAT holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ; ::_thesis: (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 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_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) ; ::_thesis: S1[n + 1] then ((Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4)) <= (1 / (sqrt ((3 * n) + 4))) * (((2 * n) + 3) / ((2 * n) + 4)) by XREAL_1:64; then A3: ((Partial_Product s) . n) * (((2 * n) + 3) / ((2 * n) + 4)) <= (1 * ((2 * n) + 3)) / ((sqrt ((3 * n) + 4)) * ((2 * n) + 4)) by XCMPLX_1:76; 111 * n <= 112 * n by XREAL_1:64; then (111 * n) + 63 <= (112 * n) + 64 by XREAL_1:7; then ((12 * (n |^ 3)) + (64 * (n ^2))) + ((111 * n) + 63) <= ((12 * (n |^ 3)) + (64 * (n ^2))) + ((112 * n) + 64) by XREAL_1:6; then (((((12 * (n |^ (2 + 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + (48 * (n ^2))) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ; then (((((12 * ((n |^ 2) * (n |^ 1))) + (36 * (n * n))) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + (48 * (n * n))) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:8; then (((((((4 * (n |^ 2)) * 3) * (n |^ 1)) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 ; then (((((((4 * (n |^ 2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:5; then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * (n |^ (2 + 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by Lm1; then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n |^ 2) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:8; then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n ^2) * (n |^ 1))) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by Lm1; then (((((((4 * (n ^2)) * 3) * n) + ((36 * n) * n)) + (27 * n)) + (28 * (n ^2))) + (84 * n)) + 63 <= (((((12 * ((n ^2) * n)) + ((48 * n) * n)) + (48 * n)) + (16 * (n ^2))) + (64 * n)) + 64 by NEWTON:5; then sqrt ((((2 * n) + 3) ^2) * ((3 * n) + 7)) <= sqrt ((((2 * n) + 4) ^2) * ((3 * n) + 4)) by SQUARE_1:26; then (sqrt (((2 * n) + 3) ^2)) * (sqrt ((3 * n) + 7)) <= sqrt ((((2 * n) + 4) ^2) * ((3 * n) + 4)) by SQUARE_1:29; then (sqrt (((2 * n) + 3) ^2)) * (sqrt ((3 * n) + 7)) <= (sqrt (((2 * n) + 4) ^2)) * (sqrt ((3 * n) + 4)) by SQUARE_1:29; then ((2 * n) + 3) * (sqrt ((3 * n) + 7)) <= (sqrt (((2 * n) + 4) ^2)) * (sqrt ((3 * n) + 4)) by SQUARE_1:22; then A4: ((2 * n) + 3) * (sqrt ((3 * n) + 7)) <= (((2 * n) + 4) * (sqrt ((3 * n) + 4))) * 1 by SQUARE_1:22; ( sqrt ((3 * n) + 4) > 0 & sqrt ((3 * n) + 7) > 0 ) by SQUARE_1:25; then (1 * ((2 * n) + 3)) / (((2 * n) + 4) * (sqrt ((3 * n) + 4))) <= 1 / (sqrt ((3 * n) + 7)) by A4, XREAL_1:102; then ((Partial_Product s) . n) * (((2 * (n + 1)) + 1) / ((2 * (n + 1)) + 2)) <= 1 / (sqrt ((3 * (n + 1)) + 4)) by A3, XXREAL_0:2; then ((Partial_Product s) . n) * (s . (n + 1)) <= 1 / (sqrt ((3 * (n + 1)) + 4)) by A1; hence S1[n + 1] by Def1; ::_thesis: verum end; (Partial_Product s) . 0 = s . 0 by Def1 .= ((2 * 0) + 1) / ((2 * 0) + 2) by A1 .= 1 / (sqrt ((3 * 0) + 4)) by SQUARE_1:20 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); hence (Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4)) ; ::_thesis: verum end; Lm9: for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > - 1 & s . n < 0 ) ) holds for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > - 1 & s . n < 0 ) ) implies for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ) defpred S1[ Element of NAT ] means ((Partial_Sums s) . \$1) * (s . (\$1 + 1)) >= 0 ; A1: ((Partial_Sums s) . 0) * (s . 1) = (s . 0) * (s . 1) by SERIES_1:def_1; assume A2: for n being Element of NAT holds ( s . n > - 1 & s . n < 0 ) ; ::_thesis: for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; ::_thesis: S1[n + 1] s . (n + 1) < 0 by A2; then A5: ((Partial_Sums s) . n) * 1 <= 0 by A4; A6: ((Partial_Sums s) . (n + 1)) * (s . (n + 2)) = (((Partial_Sums s) . n) + (s . (n + 1))) * (s . (n + 2)) by SERIES_1:def_1 .= (((Partial_Sums s) . n) * (s . (n + 2))) + ((s . (n + 1)) * (s . (n + 2))) ; ( s . (n + 2) <= 0 & s . (n + 1) <= 0 ) by A2; hence S1[n + 1] by A5, A6; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ( s . 0 < 0 & s . 1 < 0 ) by A2; then A7: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A3); hence ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; ::_thesis: verum end; theorem :: SERIES_3:49 for s1, s being Real_Sequence st ( for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ) holds for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n proof let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ) implies for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ) defpred S1[ Element of NAT ] means 1 + ((Partial_Sums s) . \$1) <= (Partial_Product s1) . \$1; assume A1: for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ; ::_thesis: for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: ((Partial_Product s1) . n) * (1 + (s . (n + 1))) = ((Partial_Product s1) . n) * (s1 . (n + 1)) by A1; s . (n + 1) > - 1 by A1; then A4: (s . (n + 1)) + 1 > (- 1) + 1 by XREAL_1:8; assume 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ; ::_thesis: S1[n + 1] then (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= ((Partial_Product s1) . n) * (1 + (s . (n + 1))) by A4, XREAL_1:64; then A5: (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= (Partial_Product s1) . (n + 1) by A3, Def1; ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 by A1, Lm9; then A6: (((Partial_Sums s) . n) * (s . (n + 1))) + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) >= 0 + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) by XREAL_1:6; 1 + ((Partial_Sums s) . (n + 1)) = 1 + (((Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def_1; hence S1[n + 1] by A5, A6, XXREAL_0:2; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ( (Partial_Sums s) . 0 = s . 0 & (Partial_Product s1) . 0 = s1 . 0 ) by Def1, SERIES_1:def_1; then A7: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); hence 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ; ::_thesis: verum end; Lm10: for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 0 ) holds for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n >= 0 ) implies for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ) assume A1: for n being Element of NAT holds s . n >= 0 ; ::_thesis: for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 let n be Element of NAT ; ::_thesis: ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ( (Partial_Sums s) . n >= 0 & s . (n + 1) >= 0 ) by A1, Th34; hence ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 ; ::_thesis: verum end; theorem :: SERIES_3:50 for s1, s being Real_Sequence st ( for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n >= 0 ) ) holds for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n proof let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n >= 0 ) ) implies for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ) defpred S1[ Element of NAT ] means 1 + ((Partial_Sums s) . \$1) <= (Partial_Product s1) . \$1; assume A1: for n being Element of NAT holds ( s1 . n = 1 + (s . n) & s . n >= 0 ) ; ::_thesis: for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: ((Partial_Product s1) . n) * (1 + (s . (n + 1))) = ((Partial_Product s1) . n) * (s1 . (n + 1)) by A1; s . (n + 1) > - 1 by A1; then A4: (s . (n + 1)) + 1 > (- 1) + 1 by XREAL_1:8; assume 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ; ::_thesis: S1[n + 1] then (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= ((Partial_Product s1) . n) * (1 + (s . (n + 1))) by A4, XREAL_1:64; then A5: (1 + ((Partial_Sums s) . n)) * (1 + (s . (n + 1))) <= (Partial_Product s1) . (n + 1) by A3, Def1; ((Partial_Sums s) . n) * (s . (n + 1)) >= 0 by A1, Lm10; then A6: (((Partial_Sums s) . n) * (s . (n + 1))) + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) >= 0 + ((1 + (s . (n + 1))) + ((Partial_Sums s) . n)) by XREAL_1:6; 1 + ((Partial_Sums s) . (n + 1)) = 1 + (((Partial_Sums s) . n) + (s . (n + 1))) by SERIES_1:def_1; hence S1[n + 1] by A5, A6, XXREAL_0:2; ::_thesis: verum end; ( (Partial_Sums s) . 0 = s . 0 & (Partial_Product s1) . 0 = s1 . 0 ) by Def1, SERIES_1:def_1; then A7: S1[ 0 ] by A1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); hence for n being Element of NAT holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n ; ::_thesis: verum end; theorem :: SERIES_3:51 for s3, s1, s2, s4, s5 being Real_Sequence st s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 holds for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) proof let s3, s1, s2, s4, s5 be Real_Sequence; ::_thesis: ( s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 implies for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ) assume that A1: s3 = s1 (#) s2 and A2: s4 = s1 (#) s1 and A3: s5 = s2 (#) s2 ; ::_thesis: for n being Element of NAT holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) let n be Element of NAT ; ::_thesis: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) A4: (Partial_Sums s3) . 0 = s3 . 0 by SERIES_1:def_1 .= (s1 . 0) * (s2 . 0) by A1, SEQ_1:8 ; defpred S1[ Element of NAT ] means ((Partial_Sums s3) . \$1) ^2 <= ((Partial_Sums s4) . \$1) * ((Partial_Sums s5) . \$1); A5: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set u = (Partial_Sums s3) . n; set v = (Partial_Sums s4) . n; set w = (Partial_Sums s5) . n; set h = s1 . (n + 1); set j = s2 . (n + 1); assume A6: ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; ::_thesis: S1[n + 1] then abs ((Partial_Sums s3) . n) <= sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) by Lm8; then A7: (2 * ((abs (s2 . (n + 1))) * (abs (s1 . (n + 1))))) * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) >= (2 * ((abs (s2 . (n + 1))) * (abs (s1 . (n + 1))))) * (abs ((Partial_Sums s3) . n)) by XREAL_1:64; A8: (Partial_Sums s5) . n >= 0 by A3, Th36; then A9: (Partial_Sums s5) . n = (sqrt ((Partial_Sums s5) . n)) ^2 by SQUARE_1:def_2; (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * (abs ((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))))) * (abs ((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1)))) by Th8; then (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((abs (sqrt ((Partial_Sums s4) . n))) * (abs (s2 . (n + 1))))) * (abs ((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1)))) by COMPLEX1:65; then A10: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((abs (sqrt ((Partial_Sums s4) . n))) * (abs (s2 . (n + 1))))) * ((abs (sqrt ((Partial_Sums s5) . n))) * (abs (s1 . (n + 1)))) by COMPLEX1:65; A11: (Partial_Sums s4) . n >= 0 by A2, Th36; then sqrt ((Partial_Sums s4) . n) >= 0 by SQUARE_1:def_2; then A12: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((sqrt ((Partial_Sums s4) . n)) * (abs (s2 . (n + 1))))) * ((abs (sqrt ((Partial_Sums s5) . n))) * (abs (s1 . (n + 1)))) by A10, ABSVALUE:def_1; sqrt ((Partial_Sums s5) . n) >= 0 by A8, SQUARE_1:def_2; then (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= (2 * ((sqrt ((Partial_Sums s4) . n)) * (abs (s2 . (n + 1))))) * ((sqrt ((Partial_Sums s5) . n)) * (abs (s1 . (n + 1)))) by A12, ABSVALUE:def_1; then A13: (((sqrt ((Partial_Sums s4) . n)) * (s2 . (n + 1))) ^2) + (((sqrt ((Partial_Sums s5) . n)) * (s1 . (n + 1))) ^2) >= ((2 * ((sqrt ((Partial_Sums s4) . n)) * (sqrt ((Partial_Sums s5) . n)))) * (abs (s2 . (n + 1)))) * (abs (s1 . (n + 1))) ; (Partial_Sums s4) . n = (sqrt ((Partial_Sums s4) . n)) ^2 by A11, SQUARE_1:def_2; then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= ((2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)))) * (abs (s2 . (n + 1)))) * (abs (s1 . (n + 1))) by A11, A8, A9, A13, SQUARE_1:29; then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= (2 * ((abs ((Partial_Sums s3) . n)) * (abs (s2 . (n + 1))))) * (abs (s1 . (n + 1))) by A7, XXREAL_0:2; then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= (2 * (abs (((Partial_Sums s3) . n) * (s2 . (n + 1))))) * (abs (s1 . (n + 1))) by COMPLEX1:65; then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= 2 * ((abs (((Partial_Sums s3) . n) * (s2 . (n + 1)))) * (abs (s1 . (n + 1)))) ; then A14: (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= 2 * (abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)))) by COMPLEX1:65; 2 * (abs ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1)))) >= 2 * ((((Partial_Sums s3) . n) * (s2 . (n + 1))) * (s1 . (n + 1))) by ABSVALUE:4, XREAL_1:64; then (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2)) >= ((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1)) by A14, XXREAL_0:2; then A15: ((((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1))) >= 0 by XREAL_1:48; (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2) >= 0 by A6, XREAL_1:48; then A16: ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2)) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s2 . (n + 1))) * (s1 . (n + 1)))) >= 0 by A15; (Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + (s3 . (n + 1)) by SERIES_1:def_1; then (Partial_Sums s3) . (n + 1) = ((Partial_Sums s3) . n) + ((s1 . (n + 1)) * (s2 . (n + 1))) by A1, SEQ_1:8; then A17: ((Partial_Sums s3) . (n + 1)) ^2 = ((((Partial_Sums s3) . n) ^2) + ((2 * ((Partial_Sums s3) . n)) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) ; ((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1)) = (((Partial_Sums s4) . n) + (s4 . (n + 1))) * ((Partial_Sums s5) . (n + 1)) by SERIES_1:def_1; then ((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1)) = (((Partial_Sums s4) . n) + (s4 . (n + 1))) * (((Partial_Sums s5) . n) + (s5 . (n + 1))) by SERIES_1:def_1 .= (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1)))) * (((Partial_Sums s5) . n) + (s5 . (n + 1))) by A2, SEQ_1:8 .= (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1)))) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) * (s2 . (n + 1)))) by A3, SEQ_1:8 .= (((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) ; then (((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1))) - (((Partial_Sums s3) . (n + 1)) ^2) = ((((((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) - ((2 * ((Partial_Sums s3) . n)) * ((s1 . (n + 1)) * (s2 . (n + 1))))) - (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) by A17 .= ((((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) - (((Partial_Sums s3) . n) ^2)) + (((Partial_Sums s4) . n) * ((s2 . (n + 1)) ^2))) + (((Partial_Sums s5) . n) * ((s1 . (n + 1)) ^2))) - (((2 * ((Partial_Sums s3) . n)) * (s1 . (n + 1))) * (s2 . (n + 1))) ; then ((((Partial_Sums s4) . (n + 1)) * ((Partial_Sums s5) . (n + 1))) - (((Partial_Sums s3) . (n + 1)) ^2)) + (((Partial_Sums s3) . (n + 1)) ^2) >= 0 + (((Partial_Sums s3) . (n + 1)) ^2) by A16, XREAL_1:6; hence S1[n + 1] ; ::_thesis: verum end; ((Partial_Sums s4) . 0) * ((Partial_Sums s5) . 0) = (s4 . 0) * ((Partial_Sums s5) . 0) by SERIES_1:def_1 .= (s4 . 0) * (s5 . 0) by SERIES_1:def_1 .= ((s1 . 0) * (s1 . 0)) * (s5 . 0) by A2, SEQ_1:8 .= ((s1 . 0) ^2) * ((s2 . 0) ^2) by A3, SEQ_1:8 ; then A18: S1[ 0 ] by A4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A5); hence ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n) ; ::_thesis: verum end; Lm11: for n being Element of NAT for s, s1, s2 being Real_Sequence st ( for n being Element of NAT holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds (Partial_Sums s) . n >= 0 proof let n be Element of NAT ; ::_thesis: for s, s1, s2 being Real_Sequence st ( for n being Element of NAT holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds (Partial_Sums s) . n >= 0 let s, s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ((s1 . n) + (s2 . n)) ^2 ) implies (Partial_Sums s) . n >= 0 ) assume A1: for n being Element of NAT holds s . n = ((s1 . n) + (s2 . n)) ^2 ; ::_thesis: (Partial_Sums s) . n >= 0 now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_>=_0 let n be Element of NAT ; ::_thesis: s . n >= 0 s . n = ((s1 . n) + (s2 . n)) ^2 by A1; hence s . n >= 0 by XREAL_1:63; ::_thesis: verum end; hence (Partial_Sums s) . n >= 0 by Th34; ::_thesis: verum end; theorem :: SERIES_3:52 for s4, s1, s5, s2, s3 being Real_Sequence st s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) holds for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) proof let s4, s1, s5, s2, s3 be Real_Sequence; ::_thesis: ( s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) implies for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ) assume that A1: s4 = s1 (#) s1 and A2: s5 = s2 (#) s2 and A3: for n being Element of NAT holds ( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ; ::_thesis: for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) A4: s1 . 0 >= 0 by A3; defpred S1[ Element of NAT ] means sqrt ((Partial_Sums s3) . \$1) <= (sqrt ((Partial_Sums s4) . \$1)) + (sqrt ((Partial_Sums s5) . \$1)); A5: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A6: sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; ::_thesis: S1[n + 1] set j = s2 . (n + 1); set h = s1 . (n + 1); set w = (Partial_Sums s5) . n; set v = (Partial_Sums s4) . n; set u = (Partial_Sums s3) . n; A7: (Partial_Sums s5) . n >= 0 by A2, Th36; A8: (s2 . (n + 1)) ^2 >= 0 by XREAL_1:63; then A9: sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= 0 by A7, SQUARE_1:def_2; A10: (Partial_Sums s4) . n >= 0 by A1, Th36; then A11: sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) >= 0 by A7, SQUARE_1:def_2; A12: (Partial_Sums s3) . n >= 0 by A3, Lm11; then sqrt ((Partial_Sums s3) . n) >= 0 by SQUARE_1:def_2; then (sqrt ((Partial_Sums s3) . n)) ^2 <= ((sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))) ^2 by A6, SQUARE_1:15; then (Partial_Sums s3) . n <= (((sqrt ((Partial_Sums s4) . n)) ^2) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2) by A12, SQUARE_1:def_2; then (Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2) by A10, SQUARE_1:def_2; then (Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((Partial_Sums s5) . n) by A7, SQUARE_1:def_2; then ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * ((sqrt ((Partial_Sums s4) . n)) * (sqrt ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) by XREAL_1:6; then A13: ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) by A10, A7, SQUARE_1:29; A14: s1 . (n + 1) >= 0 by A3; A15: s2 . (n + 1) >= 0 by A3; A16: (s1 . (n + 1)) ^2 >= 0 by XREAL_1:63; then A17: sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) >= 0 by A10, SQUARE_1:def_2; (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * (sqrt ((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) * (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)))) by A10, A7, A16, A8, SIN_COS2:1; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * (sqrt ((((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) ; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2 * ((sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) by A10, A7, A16, A8, SQUARE_1:29; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * (sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) ; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * ((sqrt ((s1 . (n + 1)) ^2)) * (sqrt ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A16, A8, SQUARE_1:29; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (sqrt ((s1 . (n + 1)) ^2))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) ; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A14, SQUARE_1:22; then (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))) by A15, SQUARE_1:22; then ((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) >= (((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) by XREAL_1:6; then (((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) >= ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) ; then ( ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2 >= 0 & (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) ^2) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) ) by A10, A7, SQUARE_1:def_2, XREAL_1:63; then sqrt (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by SQUARE_1:26; then (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by A14, A15, A11, SQUARE_1:22; then 2 * ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) <= 2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))) by XREAL_1:64; then (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))))) by XREAL_1:6; then ((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))))) by A13, XXREAL_0:2; then (((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2)) by XREAL_1:6; then ((Partial_Sums s3) . n) + ((((s1 . (n + 1)) ^2) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) ; then ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) by A10, A16, SQUARE_1:def_2; then ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2) by A7, A8, SQUARE_1:def_2; then ( ((s1 . (n + 1)) + (s2 . (n + 1))) ^2 >= 0 & ((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * ((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2) ) by A10, A7, A16, A8, SQUARE_1:29, XREAL_1:63; then A18: sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2)) <= sqrt (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))) ^2) by A12, SQUARE_1:26; A19: sqrt ((Partial_Sums s3) . (n + 1)) = sqrt (((Partial_Sums s3) . n) + (s3 . (n + 1))) by SERIES_1:def_1 .= sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2)) by A3 ; (sqrt ((Partial_Sums s4) . (n + 1))) + (sqrt ((Partial_Sums s5) . (n + 1))) = (sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt ((Partial_Sums s5) . (n + 1))) by SERIES_1:def_1 .= (sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1)))) by SERIES_1:def_1 .= (sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1))))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1)))) by A1, SEQ_1:8 .= (sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) by A2, SEQ_1:8 ; hence S1[n + 1] by A19, A17, A9, A18, SQUARE_1:22; ::_thesis: verum end; A20: s2 . 0 >= 0 by A3; (sqrt ((Partial_Sums s4) . 0)) + (sqrt ((Partial_Sums s5) . 0)) = (sqrt (s4 . 0)) + (sqrt ((Partial_Sums s5) . 0)) by SERIES_1:def_1 .= (sqrt (s4 . 0)) + (sqrt (s5 . 0)) by SERIES_1:def_1 .= (sqrt ((s1 . 0) * (s1 . 0))) + (sqrt (s5 . 0)) by A1, SEQ_1:8 .= (sqrt ((s1 . 0) ^2)) + (sqrt ((s2 . 0) * (s2 . 0))) by A2, SEQ_1:8 .= (s1 . 0) + (sqrt ((s2 . 0) ^2)) by A4, SQUARE_1:22 .= (s1 . 0) + (s2 . 0) by A20, SQUARE_1:22 .= sqrt (((s1 . 0) + (s2 . 0)) ^2) by A4, A20, SQUARE_1:22 .= sqrt (s3 . 0) by A3 .= sqrt ((Partial_Sums s3) . 0) by SERIES_1:def_1 ; then A21: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A5); hence for n being Element of NAT holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) ; ::_thesis: verum end; Lm12: for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds (n + 1) -root ((Partial_Product s) . n) > 0 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds (n + 1) -root ((Partial_Product s) . n) > 0 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n > 0 ) implies (n + 1) -root ((Partial_Product s) . n) > 0 ) assume for n being Element of NAT holds s . n > 0 ; ::_thesis: (n + 1) -root ((Partial_Product s) . n) > 0 then A1: (Partial_Product s) . n > 0 by Th43; A2: n + 1 >= 0 + 1 by XREAL_1:6; then (n + 1) -root ((Partial_Product s) . n) = (n + 1) -Root ((Partial_Product s) . n) by A1, POWER:def_1; hence (n + 1) -root ((Partial_Product s) . n) > 0 by A1, A2, PREPOWER:def_2; ::_thesis: verum end; Lm13: for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) implies ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 ) assume for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ; ::_thesis: ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 then ((n + 1) * (s . (n + 1))) / (n + 1) >= ((Partial_Sums s) . n) / (n + 1) by Th38, XREAL_1:72; then s . (n + 1) >= ((Partial_Sums s) . n) / (n + 1) by XCMPLX_1:89; then (s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1)) >= 0 by XREAL_1:48; hence ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 ; ::_thesis: verum end; theorem :: SERIES_3:53 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) holds (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ) implies (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . \$1 >= (\$1 + 1) * ((\$1 + 1) -root ((Partial_Product s) . \$1)); A1: (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1; assume A2: for n being Element of NAT holds ( s . n > 0 & s . n >= s . (n - 1) ) ; ::_thesis: (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) set u = (Partial_Sums s) . n; set v = s . (n + 1); set w = ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2); set h = (n + 1) -root ((Partial_Product s) . n); set j = ((Partial_Sums s) . n) / (n + 1); A4: s . (n + 1) > 0 by A2; A5: n + 1 >= 0 + 1 by XREAL_1:6; then (n + 1) + 1 >= 1 + 1 by XREAL_1:6; then A6: n + 2 >= 1 by XXREAL_0:2; assume (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) ; ::_thesis: S1[n + 1] then ((Partial_Sums s) . n) / (n + 1) >= ((n + 1) * ((n + 1) -root ((Partial_Product s) . n))) / (n + 1) by XREAL_1:72; then (n + 1) -root ((Partial_Product s) . n) <= ((Partial_Sums s) . n) / (n + 1) by XCMPLX_1:89; then A7: ((n + 1) -root ((Partial_Product s) . n)) |^ (n + 1) <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1) by A2, Lm12, PREPOWER:9; A8: (Partial_Product s) . n > 0 by A2, Th43; then (n + 1) -root ((Partial_Product s) . n) = (n + 1) -Root ((Partial_Product s) . n) by A5, POWER:def_1; then (Partial_Product s) . n <= (((Partial_Sums s) . n) / (n + 1)) |^ (n + 1) by A7, A8, A5, PREPOWER:19; then ((Partial_Product s) . n) * (s . (n + 1)) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1)) by A4, XREAL_1:64; then A9: (Partial_Product s) . (n + 1) <= ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (s . (n + 1)) by Def1; A10: (Partial_Product s) . (n + 1) >= 0 by A2, Th43; ( (Partial_Sums s) . n > 0 & ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 ) by A2, Lm13, Th33; then ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= ((((Partial_Sums s) . n) / (n + 1)) |^ ((n + 1) + 1)) + (((n + 2) * ((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1))) * (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) by Th31; then ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (((Partial_Sums s) . n) / (n + 1))) + (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * ((((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) * (n + 2))) by NEWTON:6; then A11: ((((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2))) |^ (n + 2) >= (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * (((Partial_Sums s) . n) / (n + 1))) + (((((Partial_Sums s) . n) / (n + 1)) |^ (n + 1)) * ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1)))) by XCMPLX_1:87; A12: (Partial_Sums s) . (n + 1) > 0 by A2, Th33; ((Partial_Sums s) . (n + 1)) / (n + 2) = ((1 * ((Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2) by SERIES_1:def_1 .= ((((n + 1) / (n + 1)) * ((Partial_Sums s) . n)) + (s . (n + 1))) / (n + 2) by XCMPLX_1:60 .= (((((n + 2) - 1) * ((Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2) ; then ((Partial_Sums s) . (n + 1)) / (n + 2) = (((((n + 2) * ((Partial_Sums s) . n)) - ((Partial_Sums s) . n)) / (n + 1)) + (s . (n + 1))) / (n + 2) .= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) + (s . (n + 1))) / (n + 2) .= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) + ((s . (n + 1)) / (n + 2)) .= (((((n + 2) * ((Partial_Sums s) . n)) / (n + 1)) / (n + 2)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2)) .= ((((n + 2) * ((Partial_Sums s) . n)) / ((n + 1) * (n + 2))) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2)) by XCMPLX_1:78 .= ((((Partial_Sums s) . n) / (n + 1)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) + ((s . (n + 1)) / (n + 2)) by XCMPLX_1:91 .= (((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) / (n + 2)) - ((((Partial_Sums s) . n) / (n + 1)) / (n + 2))) .= (((Partial_Sums s) . n) / (n + 1)) + (((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2)) ; then (((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2) >= (Partial_Product s) . (n + 1) by A11, A9, XXREAL_0:2; then (n + 2) -Root ((((Partial_Sums s) . (n + 1)) / (n + 2)) |^ (n + 2)) >= (n + 2) -Root ((Partial_Product s) . (n + 1)) by A6, A10, PREPOWER:27; then ((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -Root ((Partial_Product s) . (n + 1)) by A6, A12, PREPOWER:19; then ((Partial_Sums s) . (n + 1)) / (n + 2) >= (n + 2) -root ((Partial_Product s) . (n + 1)) by A6, A10, POWER:def_1; then (((Partial_Sums s) . (n + 1)) / (n + 2)) * (n + 2) >= (n + 2) * ((n + 2) -root ((Partial_Product s) . (n + 1))) by XREAL_1:64; hence S1[n + 1] by XCMPLX_1:87; ::_thesis: verum end; (0 + 1) * ((0 + 1) -root ((Partial_Product s) . 0)) = (0 + 1) -root (s . 0) by Def1 .= (Partial_Sums s) . 0 by A1, POWER:9 ; then A13: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A3); hence (Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n)) ; ::_thesis: verum end;