:: SERIES_5 semantic presentation begin Lm1: 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 - y) * (((x ^2) + (x * y)) + (y ^2)) = (((x * (x ^2)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2))) .= (((x * (x |^ 2)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2))) by NEWTON:81 .= (((x |^ (2 + 1)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2))) by NEWTON:6 .= (((x |^ 3) + (x * (y * y))) - ((y * x) * y)) - (y * (y ^2)) .= (x |^ 3) - ((y |^ 2) * y) by NEWTON:81 .= (x |^ 3) - (y |^ (2 + 1)) by NEWTON:6 ; hence (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2) + (x * y)) + (y ^2)) ; ::_thesis: verum end; Lm2: for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b) proof let a, b be real positive number ; ::_thesis: 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b) 1 / ((1 / a) + (1 / b)) = 1 / (((1 * b) + (1 * a)) / (a * b)) by XCMPLX_1:116 .= ((a * b) * 1) / (b + a) by XCMPLX_1:77 .= (a * b) / (b + a) ; then (2 * 1) / ((1 / a) + (1 / b)) = 2 * ((a * b) / (b + a)) by XCMPLX_1:74; hence 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b) by XCMPLX_1:74; ::_thesis: verum end; Lm3: for x, y, z being real number holds ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z) proof let x, y, z be real number ; ::_thesis: ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z) ((1 / x) * (1 / y)) * (1 / z) = (1 / (x * y)) * (1 / z) by XCMPLX_1:102 .= 1 / ((x * y) * z) by XCMPLX_1:102 ; hence ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z) ; ::_thesis: verum end; Lm4: for a, c being real positive number for b being real number holds (a / c) to_power (- b) = (c / a) to_power b proof let a, c be real positive number ; ::_thesis: for b being real number holds (a / c) to_power (- b) = (c / a) to_power b let b be real number ; ::_thesis: (a / c) to_power (- b) = (c / a) to_power b (a / c) to_power (- b) = (1 / (a / c)) to_power b by POWER:32 .= ((c / a) * 1) to_power b by XCMPLX_1:80 .= (c / a) to_power b ; hence (a / c) to_power (- b) = (c / a) to_power b ; ::_thesis: verum end; Lm5: for a, b, c, d being real positive number holds (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2) proof let a, b, c, d be real positive number ; ::_thesis: (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2) ((a * (b ^2)) * d) + (((c ^2) * d) * a) >= 2 * (sqrt (((a * (b ^2)) * d) * (((c ^2) * d) * a))) by SIN_COS2:1; then (((a * (b ^2)) * d) + (((c ^2) * d) * a)) + ((((a ^2) * b) * c) + ((b * c) * (d ^2))) >= (2 * (sqrt ((((a ^2) * (b ^2)) * (c ^2)) * (d ^2)))) + ((((a ^2) * b) * c) + ((b * c) * (d ^2))) by XREAL_1:7; then ((((a * (b ^2)) * d) + (((c ^2) * d) * a)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) >= ((2 * (sqrt (((a * b) * (c * d)) ^2))) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) ; then A1: ((((a * (b ^2)) * d) + (((c ^2) * d) * a)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) >= ((2 * (((a * b) * c) * d)) + (((a ^2) * b) * c)) + ((b * c) * (d ^2)) by SQUARE_1:22; (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) = ((a * b) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) by SQUARE_1:def_2 .= ((a * b) + (c * d)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) by SQUARE_1:def_2 .= ((a * b) + (c * d)) * ((a * c) + ((sqrt (b * d)) ^2)) by SQUARE_1:def_2 .= ((a * b) + (c * d)) * ((a * c) + (b * d)) by SQUARE_1:def_2 .= (((((a ^2) * b) * c) + ((a * (b ^2)) * d)) + (((c ^2) * d) * a)) + ((b * c) * (d ^2)) ; hence (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2) by A1; ::_thesis: verum end; Lm6: for x, y, z being real number holds ((x + y) + z) ^2 = (((((x ^2) + (y ^2)) + (z ^2)) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x) ; Lm7: for x being real number st abs x < 1 holds x ^2 < 1 proof let x be real number ; ::_thesis: ( abs x < 1 implies x ^2 < 1 ) assume abs x < 1 ; ::_thesis: x ^2 < 1 then (abs x) ^2 < 1 ^2 by SQUARE_1:16; hence x ^2 < 1 by COMPLEX1:75; ::_thesis: verum end; Lm8: for x being real number st x ^2 < 1 holds abs x < 1 proof let x be real number ; ::_thesis: ( x ^2 < 1 implies abs x < 1 ) assume x ^2 < 1 ; ::_thesis: abs x < 1 then sqrt (x ^2) < 1 by SQUARE_1:18, SQUARE_1:27, XREAL_1:63; hence abs x < 1 by COMPLEX1:72; ::_thesis: verum end; Lm9: for a, b, c being real positive number holds (((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3 proof let a, b, c be real positive number ; ::_thesis: (((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3 (((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((((((2 ^2) * 2) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b)) .= (((((((2 |^ 2) * 2) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b)) by NEWTON:81 .= ((((((2 |^ (2 + 1)) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (b * c))) * (sqrt (a * c))) * (sqrt (a * b)) by NEWTON:6 .= (((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((sqrt (b * c)) * (sqrt (a * c)))) * (sqrt (a * b)) .= (((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt ((b * c) * (a * c)))) * (sqrt (a * b)) by SQUARE_1:29 .= ((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((sqrt (((b * c) * a) * c)) * (sqrt (a * b))) .= ((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt ((((b * c) * a) * c) * (a * b))) by SQUARE_1:29 .= ((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * (sqrt (((a * b) * c) ^2)) .= ((((2 |^ 3) * (a ^2)) * (b ^2)) * (c ^2)) * ((a * b) * c) by SQUARE_1:22 .= (((2 |^ 3) * ((a ^2) * a)) * ((b ^2) * b)) * ((c ^2) * c) .= (((2 |^ 3) * ((a |^ 2) * a)) * ((b ^2) * b)) * ((c ^2) * c) by NEWTON:81 .= (((2 |^ 3) * ((a |^ 2) * a)) * ((b |^ 2) * b)) * ((c ^2) * c) by NEWTON:81 .= (((2 |^ 3) * ((a |^ 2) * a)) * ((b |^ 2) * b)) * ((c |^ 2) * c) by NEWTON:81 .= (((2 |^ 3) * (a |^ (2 + 1))) * ((b |^ 2) * b)) * ((c |^ 2) * c) by NEWTON:6 .= (((2 |^ 3) * (a |^ 3)) * (b |^ 3)) * ((c |^ 2) * c) by NEWTON:6 .= (((2 |^ 3) * (a |^ 3)) * (b |^ 3)) * (c |^ (2 + 1)) by NEWTON:6 .= (((2 * a) |^ 3) * (b |^ 3)) * (c |^ 3) by NEWTON:7 .= (((2 * a) * b) |^ 3) * (c |^ 3) by NEWTON:7 .= (((2 * a) * b) * c) |^ 3 by NEWTON:7 ; hence (((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3 ; ::_thesis: verum end; Lm10: for a, b being real positive number holds sqrt (((a ^2) + (a * b)) + (b ^2)) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) proof let a, b be real positive number ; ::_thesis: sqrt (((a ^2) + (a * b)) + (b ^2)) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) A1: ((1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)))) ^2 = ((1 / 2) * (1 / 2)) * ((sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) ^2) .= (1 / 4) * ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)) by SQUARE_1:def_2 .= (sqrt (((a ^2) + (a * b)) + (b ^2))) ^2 by SQUARE_1:def_2 ; A2: sqrt (((a ^2) + (a * b)) + (b ^2)) > 0 by SQUARE_1:25; sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)) > 0 by SQUARE_1:25; then sqrt ((sqrt (((a ^2) + (a * b)) + (b ^2))) ^2) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) by A1, SQUARE_1:22; hence sqrt (((a ^2) + (a * b)) + (b ^2)) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) by A2, SQUARE_1:22; ::_thesis: verum end; Lm11: for a, b being real positive number holds sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b) proof let a, b be real positive number ; ::_thesis: sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b) (a ^2) + (b ^2) >= (2 * a) * b by SERIES_3:6; then ((a ^2) + (b ^2)) + ((3 * ((a ^2) + (b ^2))) + ((4 * a) * b)) >= ((2 * a) * b) + ((3 * ((a ^2) + (b ^2))) + ((4 * a) * b)) by XREAL_1:6; then sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)) >= sqrt ((3 * ((a ^2) + (b ^2))) + ((6 * a) * b)) by SQUARE_1:26; then A1: (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b))) >= (1 / 2) * (sqrt ((3 * ((a ^2) + (b ^2))) + ((6 * a) * b))) by XREAL_1:64; sqrt ((3 * ((a ^2) + (b ^2))) + ((6 * a) * b)) = sqrt (3 * ((a + b) ^2)) ; then sqrt ((3 * ((a ^2) + (b ^2))) + ((6 * a) * b)) = (sqrt 3) * (sqrt ((a + b) ^2)) by SQUARE_1:29 .= (sqrt 3) * (a + b) by SQUARE_1:22 ; hence sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b) by A1, Lm10; ::_thesis: verum end; Lm12: for a, b being real positive number holds sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) proof let a, b be real positive number ; ::_thesis: sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) ((a ^2) + (b ^2)) / 2 >= a * b by SERIES_3:7; then (((a ^2) + (b ^2)) / 2) + ((a ^2) + (b ^2)) >= (a * b) + ((a ^2) + (b ^2)) by XREAL_1:6; then (((a ^2) + (b ^2)) + (((a ^2) + (b ^2)) / 2)) / 3 >= (((a ^2) + (a * b)) + (b ^2)) / 3 by XREAL_1:72; hence sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) by SQUARE_1:26; ::_thesis: verum end; Lm13: for b, c, a being real positive number holds (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2) proof let b, c, a be real positive number ; ::_thesis: (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2) (((b * c) / a) ^2) + (((c * a) / b) ^2) >= (2 * ((b * c) / a)) * ((c * a) / b) by SERIES_3:6; then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * c) / a) * ((c * a) / b)) ; then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * c) * (c * a)) / (a * b)) by XCMPLX_1:76; then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * a) * (c * c)) / ((a * b) * 1)) ; then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * ((c * c) / 1) by XCMPLX_1:91; hence (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2) ; ::_thesis: verum end; Lm14: for b, c, a being real positive number holds ((b * c) / a) * ((c * a) / b) = c ^2 proof let b, c, a be real positive number ; ::_thesis: ((b * c) / a) * ((c * a) / b) = c ^2 ((b * c) / a) * ((c * a) / b) = ((b * c) * (c * a)) / (a * b) by XCMPLX_1:76 .= ((c * c) * (a * b)) / (a * b) .= (c * c) * ((a * b) / (a * b)) by XCMPLX_1:74 .= (c * c) * 1 by XCMPLX_1:60 ; hence ((b * c) / a) * ((c * a) / b) = c ^2 ; ::_thesis: verum end; Lm15: for b, c, a being real positive number holds (((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) = 2 * (((a ^2) + (b ^2)) + (c ^2)) proof let b, c, a be real positive number ; ::_thesis: (((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) = 2 * (((a ^2) + (b ^2)) + (c ^2)) (((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) = ((2 * (((b * c) / a) * ((c * a) / b))) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) .= ((2 * (c ^2)) + (2 * (((b * c) / a) * ((a * b) / c)))) + ((2 * ((c * a) / b)) * ((a * b) / c)) by Lm14 .= ((2 * (c ^2)) + (2 * (b ^2))) + (2 * (((c * a) / b) * ((a * b) / c))) by Lm14 .= ((2 * (c ^2)) + (2 * (b ^2))) + (2 * (a ^2)) by Lm14 .= 2 * (((c ^2) + (b ^2)) + (a ^2)) ; hence (((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) = 2 * (((a ^2) + (b ^2)) + (c ^2)) ; ::_thesis: verum end; Lm16: for b, c, a being real positive number holds ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) proof let b, c, a be real positive number ; ::_thesis: ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((b * c) / a) ^2) + (((c * a) / b) ^2)) + (((a * b) / c) ^2)) + ((((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c))) .= (((((b * c) / a) ^2) + (((c * a) / b) ^2)) + (((a * b) / c) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) by Lm15 ; hence ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) ; ::_thesis: verum end; Lm17: for a, b, c being real positive number st (a + b) + c = 1 holds (1 / a) - 1 = (b + c) / a proof let a, b, c be real positive number ; ::_thesis: ( (a + b) + c = 1 implies (1 / a) - 1 = (b + c) / a ) assume (a + b) + c = 1 ; ::_thesis: (1 / a) - 1 = (b + c) / a then (1 / a) - 1 = ((a + (b + c)) / a) - 1 .= ((a / a) + ((b + c) / a)) - 1 by XCMPLX_1:62 .= (1 + ((b + c) / a)) - 1 by XCMPLX_1:60 ; hence (1 / a) - 1 = (b + c) / a ; ::_thesis: verum end; Lm18: for b, c, a being real positive number holds (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = 8 proof let b, c, a be real positive number ; ::_thesis: (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = 8 (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = (((2 * (sqrt (b * c))) * (2 * (sqrt (a * c)))) / (a * b)) * ((2 * (sqrt (a * b))) / c) by XCMPLX_1:76 .= ((4 * ((sqrt (b * c)) * (sqrt (a * c)))) / (a * b)) * ((2 * (sqrt (a * b))) / c) .= ((4 * (sqrt ((b * c) * (a * c)))) / (a * b)) * ((2 * (sqrt (a * b))) / c) by SQUARE_1:29 .= ((4 * (sqrt ((b * a) * (c ^2)))) * (2 * (sqrt (a * b)))) / ((a * b) * c) by XCMPLX_1:76 .= (8 * ((sqrt ((b * a) * (c ^2))) * (sqrt (a * b)))) / ((a * b) * c) .= (8 * (sqrt (((b * a) * (c ^2)) * (a * b)))) / ((a * b) * c) by SQUARE_1:29 .= (8 * (sqrt (((a * b) * c) ^2))) / ((a * b) * c) .= (8 * ((a * b) * c)) / ((a * b) * c) by SQUARE_1:22 .= 8 * (((a * b) * c) / ((a * b) * c)) by XCMPLX_1:74 .= 8 * 1 by XCMPLX_1:60 ; hence (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = 8 ; ::_thesis: verum end; Lm19: for a, b, c being real positive number st (a + b) + c = 1 holds 1 + (1 / a) = 2 + ((b + c) / a) proof let a, b, c be real positive number ; ::_thesis: ( (a + b) + c = 1 implies 1 + (1 / a) = 2 + ((b + c) / a) ) assume (a + b) + c = 1 ; ::_thesis: 1 + (1 / a) = 2 + ((b + c) / a) then 1 + (1 / a) = 1 + ((a + (b + c)) / a) .= 1 + ((a / a) + ((b + c) / a)) by XCMPLX_1:62 .= (1 + (a / a)) + ((b + c) / a) .= (1 + 1) + ((b + c) / a) by XCMPLX_1:60 ; hence 1 + (1 / a) = 2 + ((b + c) / a) ; ::_thesis: verum end; Lm20: for a, c, b being real positive number holds (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c))) proof let a, c, b be real positive number ; ::_thesis: (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c))) A1: sqrt (b * c) > 0 by SQUARE_1:25; (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = (1 * ((sqrt (a * b)) / c)) + (((sqrt (a * c)) / b) * ((sqrt (a * b)) / c)) .= ((sqrt (a * b)) / c) + (((sqrt (a * c)) * (sqrt (a * b))) / (b * c)) by XCMPLX_1:76 .= ((sqrt (a * b)) / c) + ((sqrt ((a * c) * (a * b))) / (b * c)) by SQUARE_1:29 .= ((sqrt (a * b)) / c) + ((sqrt ((a ^2) * (c * b))) / (b * c)) .= ((sqrt (a * b)) / c) + (((sqrt (a ^2)) * (sqrt (c * b))) / (b * c)) by SQUARE_1:29 .= ((sqrt (a * b)) / c) + (((sqrt (a ^2)) * (sqrt (c * b))) / ((sqrt (b * c)) ^2)) by SQUARE_1:def_2 .= ((sqrt (a * b)) / c) + (((sqrt (a ^2)) / (sqrt (b * c))) * ((sqrt (c * b)) / (sqrt (b * c)))) by XCMPLX_1:76 .= ((sqrt (a * b)) / c) + (((sqrt (a ^2)) / (sqrt (b * c))) * 1) by A1, XCMPLX_1:60 .= ((sqrt (a * b)) / c) + (a / (sqrt (b * c))) by SQUARE_1:22 ; hence (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c))) ; ::_thesis: verum end; Lm21: for b, c, a being real positive number holds (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (b / (sqrt (a * c))) + 1 proof let b, c, a be real positive number ; ::_thesis: (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (b / (sqrt (a * c))) + 1 A1: sqrt (a * c) > 0 by SQUARE_1:25; A2: sqrt (a * b) > 0 by SQUARE_1:25; (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (((sqrt (b * c)) / a) * ((sqrt (a * b)) / c)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) .= (((sqrt (b * c)) * (sqrt (a * b))) / (a * c)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by XCMPLX_1:76 .= ((sqrt ((b * c) * (a * b))) / (a * c)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by SQUARE_1:29 .= ((sqrt ((a * c) * (b ^2))) / (a * c)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) .= (((sqrt (a * c)) * (sqrt (b ^2))) / (a * c)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by SQUARE_1:29 .= (((sqrt (b ^2)) * (sqrt (a * c))) / ((sqrt (a * c)) ^2)) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by SQUARE_1:def_2 .= (((sqrt (b ^2)) / (sqrt (a * c))) * ((sqrt (a * c)) / (sqrt (a * c)))) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by XCMPLX_1:76 .= (((sqrt (b ^2)) / (sqrt (a * c))) * 1) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by A1, XCMPLX_1:60 .= (b / (sqrt (a * c))) + ((c / (sqrt (b * a))) * ((sqrt (a * b)) / c)) by SQUARE_1:22 .= (b / (sqrt (a * c))) + ((c / c) * ((sqrt (a * b)) / (sqrt (b * a)))) by XCMPLX_1:85 .= (b / (sqrt (a * c))) + (1 * ((sqrt (a * b)) / (sqrt (b * a)))) by XCMPLX_1:60 .= (b / (sqrt (a * c))) + 1 by A2, XCMPLX_1:60 ; hence (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (b / (sqrt (a * c))) + 1 ; ::_thesis: verum end; Lm22: for b, c, a being real positive number holds ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) proof let b, c, a be real positive number ; ::_thesis: ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) A1: sqrt (b * a) > 0 by SQUARE_1:25; ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = ((((1 * 1) + (1 * ((sqrt (a * c)) / b))) + (((sqrt (b * c)) / a) * 1)) + (((sqrt (b * c)) / a) * ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * c)) * (sqrt (a * c))) / (a * b))) * (1 + ((sqrt (a * b)) / c)) by XCMPLX_1:76 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + ((sqrt ((b * c) * (a * c))) / (a * b))) * (1 + ((sqrt (a * b)) / c)) by SQUARE_1:29 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + ((sqrt ((b * a) * (c ^2))) / (a * b))) * (1 + ((sqrt (a * b)) / c)) .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * (sqrt (c ^2))) / (a * b))) * (1 + ((sqrt (a * b)) / c)) by SQUARE_1:29 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * c) / (a * b))) * (1 + ((sqrt (a * b)) / c)) by SQUARE_1:22 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) * c) / ((sqrt (a * b)) ^2))) * (1 + ((sqrt (a * b)) / c)) by SQUARE_1:def_2 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (((sqrt (b * a)) / (sqrt (b * a))) * (c / (sqrt (b * a))))) * (1 + ((sqrt (a * b)) / c)) by XCMPLX_1:76 .= (((1 + ((sqrt (a * c)) / b)) + ((sqrt (b * c)) / a)) + (1 * (c / (sqrt (b * a))))) * (1 + ((sqrt (a * b)) / c)) by A1, XCMPLX_1:60 .= ((((1 + ((sqrt (a * c)) / b)) + ((1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c)) .= ((((1 + ((sqrt (a * c)) / b)) + (((sqrt (a * b)) / c) + (a / (sqrt (b * c))))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c)) by Lm20 .= (((((1 + ((sqrt (a * c)) / b)) + ((sqrt (a * b)) / c)) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) + (c / (sqrt (b * a)))) + ((b / (sqrt (a * c))) + 1) by Lm21 .= (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) ; hence ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) ; ::_thesis: verum end; Lm23: for a, c, b being real positive number holds ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6 proof let a, c, b be real positive number ; ::_thesis: ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6 sqrt (a * c) > 0 by SQUARE_1:25; then A1: ((sqrt (a * c)) / b) + (b / (sqrt (a * c))) >= 2 by SERIES_3:3; sqrt (b * c) > 0 by SQUARE_1:25; then A2: (a / (sqrt (b * c))) + ((sqrt (b * c)) / a) >= 2 by SERIES_3:3; sqrt (b * a) > 0 by SQUARE_1:25; then ((sqrt (a * b)) / c) + (c / (sqrt (b * a))) >= 2 by SERIES_3:3; then (((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + (((sqrt (a * b)) / c) + (c / (sqrt (b * a)))) >= 2 + 2 by A1, XREAL_1:7; then (((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + ((a / (sqrt (b * c))) + ((sqrt (b * c)) / a)) >= 4 + 2 by A2, XREAL_1:7; hence ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6 ; ::_thesis: verum end; theorem :: SERIES_5:1 for a, b being real positive number holds (a + b) * ((1 / a) + (1 / b)) >= 4 proof let a, b be real positive number ; ::_thesis: (a + b) * ((1 / a) + (1 / b)) >= 4 (a / b) + (b / a) >= 2 * (sqrt ((a / b) * (b / a))) by SIN_COS2:1; then (a / b) + (b / a) >= 2 * (sqrt ((a * b) / (b * a))) by XCMPLX_1:76; then (a / b) + (b / a) >= 2 * (sqrt (((a / b) * b) / a)) by XCMPLX_1:83; then (a / b) + (b / a) >= 2 * (sqrt (a / a)) by XCMPLX_1:87; then (a / b) + (b / a) >= 2 * 1 by SQUARE_1:18, XCMPLX_1:60; then ((a / b) + (b / a)) + 2 >= 2 + 2 by XREAL_1:7; then (((a / b) + (b / a)) + 1) + 1 >= 4 ; then (((a * (1 / b)) + (b / a)) + 1) + 1 >= 4 by XCMPLX_1:99; then (((a * (1 / b)) + (b * (1 / a))) + 1) + 1 >= 4 by XCMPLX_1:99; then (((a * (1 / b)) + (b * (1 / a))) + (a * (1 / a))) + 1 >= 4 by XCMPLX_1:106; then (((a * (1 / b)) + (b * (1 / a))) + (a * (1 / a))) + (b * (1 / b)) >= 4 by XCMPLX_1:106; hence (a + b) * ((1 / a) + (1 / b)) >= 4 ; ::_thesis: verum end; theorem :: SERIES_5:2 for a, b being real positive number holds (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3)) proof let a, b be real positive number ; ::_thesis: (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3)) (a - b) ^2 >= 0 by XREAL_1:63; then ((a - b) * (a - b)) * (((a ^2) + (a * b)) + (b ^2)) >= 0 ; then (a - b) * ((a - b) * (((a ^2) + (a * b)) + (b ^2))) >= 0 ; then (a - b) * ((a |^ 3) - (b |^ 3)) >= 0 by Lm1; then (((a |^ 3) * a) - ((a |^ 3) * b)) - ((b |^ 3) * (a - b)) >= 0 ; then ((a |^ (3 + 1)) - ((a |^ 3) * b)) - ((b |^ 3) * (a - b)) >= 0 by NEWTON:6; then ((a |^ 4) - ((a |^ 3) * b)) - (((b |^ 3) * a) - ((b |^ 3) * b)) >= 0 ; then ((a |^ 4) - ((a |^ 3) * b)) - (((b |^ 3) * a) - (b |^ (3 + 1))) >= 0 by NEWTON:6; then ((((a |^ 4) + (b |^ 4)) - ((a |^ 3) * b)) - ((b |^ 3) * a)) + (((a |^ 3) * b) + ((b |^ 3) * a)) >= 0 + (((a |^ 3) * b) + ((b |^ 3) * a)) by XREAL_1:7; hence (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3)) ; ::_thesis: verum end; theorem Th3: :: SERIES_5:3 for a, b, c being real positive number st a < b holds 1 < (b + c) / (a + c) proof let a, b, c be real positive number ; ::_thesis: ( a < b implies 1 < (b + c) / (a + c) ) assume a < b ; ::_thesis: 1 < (b + c) / (a + c) then a + c < b + c by XREAL_1:8; hence 1 < (b + c) / (a + c) by XREAL_1:187; ::_thesis: verum end; theorem Th4: :: SERIES_5:4 for a, b being real positive number st a < b holds a / b < sqrt (a / b) proof let a, b be real positive number ; ::_thesis: ( a < b implies a / b < sqrt (a / b) ) b ^2 > 0 ; then b |^ 2 > 0 by NEWTON:81; then (b |^ 2) * b > 0 ; then A1: b |^ (2 + 1) > 0 by NEWTON:6; assume a < b ; ::_thesis: a / b < sqrt (a / b) then a - b < 0 by XREAL_1:49; then (a * b) * (a - b) < 0 ; then (((a ^2) * b) - (a * (b ^2))) + (a * (b ^2)) < 0 + (a * (b ^2)) by XREAL_1:8; then ((a ^2) * b) / (b |^ (2 + 1)) < (a * (b ^2)) / (b |^ (2 + 1)) by A1, XREAL_1:74; then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / (b |^ (2 + 1)) by NEWTON:6; then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:6; then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:81; then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b ^2) * b) by NEWTON:81; then (a ^2) / (b ^2) < (a * (b ^2)) / (b * (b ^2)) by XCMPLX_1:91; then (a ^2) / (b ^2) < a / b by XCMPLX_1:91; then (a / b) ^2 < a / b by XCMPLX_1:76; then sqrt ((a / b) ^2) < sqrt (a / b) by SQUARE_1:27; hence a / b < sqrt (a / b) by SQUARE_1:22; ::_thesis: verum end; theorem Th5: :: SERIES_5:5 for a, b being real positive number st a < b holds sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) proof let a, b be real positive number ; ::_thesis: ( a < b implies sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) ) assume A1: a < b ; ::_thesis: sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) then a / b < 1 by XREAL_1:189; then A2: sqrt (a / b) < 1 by SQUARE_1:18, SQUARE_1:27; sqrt (((a ^2) + (b ^2)) / 2) > 0 by SQUARE_1:25; then 1 < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A1, Th3; hence sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A2, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:6 for a, b being real positive number st a < b holds a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) proof let a, b be real positive number ; ::_thesis: ( a < b implies a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) ) assume A1: a < b ; ::_thesis: a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) then A2: sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by Th5; a / b < sqrt (a / b) by A1, Th4; hence a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A2, XXREAL_0:2; ::_thesis: verum end; theorem Th7: :: SERIES_5:7 for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) <= sqrt (a * b) proof let a, b be real positive number ; ::_thesis: 2 / ((1 / a) + (1 / b)) <= sqrt (a * b) A1: sqrt (a * b) > 0 by SQUARE_1:25; then (2 * (sqrt (a * b))) / (a + b) <= 1 by SIN_COS2:1, XREAL_1:183; then ((2 * (sqrt (a * b))) / (a + b)) * (sqrt (a * b)) <= 1 * (sqrt (a * b)) by A1, XREAL_1:64; then (2 * (sqrt (a * b))) / ((a + b) / (sqrt (a * b))) <= sqrt (a * b) by XCMPLX_1:82; then ((2 * (sqrt (a * b))) * (sqrt (a * b))) / (a + b) <= sqrt (a * b) by XCMPLX_1:77; then (2 * ((sqrt (a * b)) ^2)) / (a + b) <= sqrt (a * b) ; then (2 * (a * b)) / (a + b) <= sqrt (a * b) by SQUARE_1:def_2; hence 2 / ((1 / a) + (1 / b)) <= sqrt (a * b) by Lm2; ::_thesis: verum end; theorem Th8: :: SERIES_5:8 for a, b being real positive number holds (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) proof let a, b be real positive number ; ::_thesis: (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) (a ^2) + (b ^2) >= (2 * a) * b by SERIES_3:6; then ((a ^2) + (b ^2)) + ((a ^2) + (b ^2)) >= ((2 * a) * b) + ((a ^2) + (b ^2)) by XREAL_1:7; then sqrt (2 * ((a ^2) + (b ^2))) >= sqrt ((a + b) ^2) by SQUARE_1:26; then sqrt (2 * ((a ^2) + (b ^2))) >= a + b by SQUARE_1:22; then (sqrt (2 * ((a ^2) + (b ^2)))) / (sqrt (2 * 2)) >= (a + b) / 2 by SQUARE_1:20, XREAL_1:72; then (sqrt (2 * ((a ^2) + (b ^2)))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:29; then ((sqrt 2) * (sqrt ((a ^2) + (b ^2)))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:29; then A1: (((sqrt 2) / (sqrt 2)) * (sqrt ((a ^2) + (b ^2)))) / (sqrt 2) >= (a + b) / 2 by XCMPLX_1:83; sqrt 2 > 0 by SQUARE_1:25; then (1 * (sqrt ((a ^2) + (b ^2)))) / (sqrt 2) >= (a + b) / 2 by A1, XCMPLX_1:60; hence (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) by SQUARE_1:30; ::_thesis: verum end; theorem :: SERIES_5:9 for x, y being real number holds x + y <= sqrt (2 * ((x ^2) + (y ^2))) proof let x, y be real number ; ::_thesis: x + y <= sqrt (2 * ((x ^2) + (y ^2))) (x ^2) + (y ^2) >= (2 * x) * y by SERIES_3:6; then A1: ((x ^2) + (y ^2)) + ((x ^2) + (y ^2)) >= ((2 * x) * y) + ((x ^2) + (y ^2)) by XREAL_1:6; then A2: 2 * ((x ^2) + (y ^2)) >= (x + y) ^2 ; A3: (x + y) ^2 >= 0 by XREAL_1:63; then A4: sqrt (2 * ((x ^2) + (y ^2))) >= sqrt ((x + y) ^2) by A1, SQUARE_1:26; percases ( x + y > 0 or x + y = 0 or x + y < 0 ) ; suppose x + y > 0 ; ::_thesis: x + y <= sqrt (2 * ((x ^2) + (y ^2))) hence x + y <= sqrt (2 * ((x ^2) + (y ^2))) by A4, SQUARE_1:22; ::_thesis: verum end; suppose x + y = 0 ; ::_thesis: x + y <= sqrt (2 * ((x ^2) + (y ^2))) hence x + y <= sqrt (2 * ((x ^2) + (y ^2))) by A2, SQUARE_1:17, SQUARE_1:26; ::_thesis: verum end; suppose x + y < 0 ; ::_thesis: x + y <= sqrt (2 * ((x ^2) + (y ^2))) hence x + y <= sqrt (2 * ((x ^2) + (y ^2))) by A1, A3, SQUARE_1:def_2; ::_thesis: verum end; end; end; theorem Th10: :: SERIES_5:10 for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 proof let a, b be real positive number ; ::_thesis: 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 A1: (a + b) / 2 >= sqrt (a * b) by SERIES_3:2; 2 / ((1 / a) + (1 / b)) <= sqrt (a * b) by Th7; hence 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:11 for a, b being real positive number holds sqrt (a * b) <= sqrt (((a ^2) + (b ^2)) / 2) proof let a, b be real positive number ; ::_thesis: sqrt (a * b) <= sqrt (((a ^2) + (b ^2)) / 2) A1: (a + b) / 2 >= sqrt (a * b) by SERIES_3:2; (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) by Th8; hence sqrt (a * b) <= sqrt (((a ^2) + (b ^2)) / 2) by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:12 for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2) proof let a, b be real positive number ; ::_thesis: 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2) A1: 2 / ((1 / a) + (1 / b)) <= (a + b) / 2 by Th10; (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) by Th8; hence 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2) by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:13 for x, y being real number st abs x < 1 & abs y < 1 holds abs ((x + y) / (1 + (x * y))) <= 1 proof let x, y be real number ; ::_thesis: ( abs x < 1 & abs y < 1 implies abs ((x + y) / (1 + (x * y))) <= 1 ) assume that A1: abs x < 1 and A2: abs y < 1 ; ::_thesis: abs ((x + y) / (1 + (x * y))) <= 1 percases ( 1 + (x * y) <> 0 or 1 + (x * y) = 0 ) ; supposeA3: 1 + (x * y) <> 0 ; ::_thesis: abs ((x + y) / (1 + (x * y))) <= 1 y ^2 < 1 by A2, Lm7; then A4: (y ^2) - (y ^2) < 1 - (y ^2) by XREAL_1:14; x ^2 < 1 by A1, Lm7; then (x ^2) - (x ^2) < 1 - (x ^2) by XREAL_1:14; then 0 < (1 - (x ^2)) * (1 - (y ^2)) by A4; then 0 + ((x ^2) + (y ^2)) < (((1 - (y ^2)) - (x ^2)) + ((x ^2) * (y ^2))) + ((x ^2) + (y ^2)) by XREAL_1:8; then A5: ((x ^2) + (y ^2)) + ((2 * x) * y) < (1 + ((x ^2) * (y ^2))) + ((2 * x) * y) by XREAL_1:8; (1 + (x * y)) ^2 > 0 by A3, SQUARE_1:12; then ((x + y) ^2) / ((1 + (x * y)) ^2) < (((x * y) + 1) ^2) / ((1 + (x * y)) ^2) by A5, XREAL_1:74; then ((x + y) ^2) / ((1 + (x * y)) ^2) < 1 by A3, XCMPLX_1:60; then ((x + y) / (1 + (x * y))) ^2 < 1 by XCMPLX_1:76; hence abs ((x + y) / (1 + (x * y))) <= 1 by Lm8; ::_thesis: verum end; suppose 1 + (x * y) = 0 ; ::_thesis: abs ((x + y) / (1 + (x * y))) <= 1 then abs ((x + y) / (1 + (x * y))) = abs 0 by XCMPLX_1:49 .= 0 by ABSVALUE:2 ; hence abs ((x + y) / (1 + (x * y))) <= 1 ; ::_thesis: verum end; end; end; theorem :: SERIES_5:14 for x, y being real number holds (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) proof let x, y be real number ; ::_thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) percases ( abs (x + y) = 0 or abs (x + y) > 0 ) ; suppose abs (x + y) = 0 ; ::_thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) hence (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) ; ::_thesis: verum end; supposeA1: abs (x + y) > 0 ; ::_thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) 1 + (abs y) >= 1 by XREAL_1:31; then (1 + (abs y)) + (abs x) >= 1 + (abs x) by XREAL_1:6; then A2: (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) by XREAL_1:118; 1 + (abs x) >= 1 by XREAL_1:31; then (1 + (abs x)) + (abs y) >= 1 + (abs y) by XREAL_1:6; then (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) by XREAL_1:118; then A3: ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A2, XREAL_1:7; 1 / ((abs x) + (abs y)) <= 1 / (abs (x + y)) by A1, COMPLEX1:56, XREAL_1:118; then (1 / ((abs x) + (abs y))) + 1 <= (1 / (abs (x + y))) + 1 by XREAL_1:7; then A4: 1 / ((1 / (abs (x + y))) + 1) <= 1 / ((1 / ((abs x) + (abs y))) + 1) by XREAL_1:118; A5: 0 < (abs x) + (abs y) by A1, COMPLEX1:56; then A6: 1 / ((1 / ((abs x) + (abs y))) + 1) = (1 * ((abs x) + (abs y))) / (((1 / ((abs x) + (abs y))) + 1) * ((abs x) + (abs y))) by XCMPLX_1:91 .= ((abs x) + (abs y)) / (((1 / ((abs x) + (abs y))) * ((abs x) + (abs y))) + ((abs x) + (abs y))) .= ((abs x) + (abs y)) / (1 + ((abs x) + (abs y))) by A5, XCMPLX_1:87 .= ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) by XCMPLX_1:62 ; (abs (x + y)) / (1 + (abs (x + y))) = ((abs (x + y)) / (abs (x + y))) / ((1 + (abs (x + y))) / (abs (x + y))) by A1, XCMPLX_1:55 .= 1 / ((1 + (abs (x + y))) / (abs (x + y))) by A1, XCMPLX_1:60 .= 1 / ((1 / (abs (x + y))) + ((abs (x + y)) / (abs (x + y)))) by XCMPLX_1:62 .= 1 / ((1 / (abs (x + y))) + 1) by A1, XCMPLX_1:60 ; hence (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A4, A6, A3, XXREAL_0:2; ::_thesis: verum end; end; end; theorem :: SERIES_5:15 for a, b, d, c being real positive number holds (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) > 1 proof let a, b, d, c be real positive number ; ::_thesis: (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) > 1 d + ((a + b) + c) > 0 + ((a + b) + c) by XREAL_1:8; then A1: b / (((a + b) + c) + d) < b / ((a + b) + c) by XREAL_1:76; ((b + c) + d) + a > 0 + ((b + c) + d) by XREAL_1:8; then A2: c / ((b + c) + d) > c / (((a + b) + c) + d) by XREAL_1:76; c + ((a + b) + d) > 0 + ((a + b) + d) by XREAL_1:8; then a / (((a + b) + c) + d) < a / ((a + b) + d) by XREAL_1:76; then (a / (((a + b) + c) + d)) + (b / (((a + b) + c) + d)) < (a / ((a + b) + d)) + (b / ((a + b) + c)) by A1, XREAL_1:8; then (a + b) / (((a + b) + c) + d) < (a / ((a + b) + d)) + (b / ((a + b) + c)) by XCMPLX_1:62; then ((a + b) / (((a + b) + c) + d)) + (c / (((a + b) + c) + d)) < ((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d)) by A2, XREAL_1:8; then A3: ((a + b) + c) / (((a + b) + c) + d) < ((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d)) by XCMPLX_1:62; b + ((a + c) + d) > 0 + ((a + c) + d) by XREAL_1:8; then d / ((a + c) + d) > d / (((a + b) + c) + d) by XREAL_1:76; then (((a + b) + c) / (((a + b) + c) + d)) + (d / (((a + b) + c) + d)) < (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) by A3, XREAL_1:8; then (((a + b) + c) + d) / (((a + b) + c) + d) < (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) by XCMPLX_1:62; hence (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) > 1 by XCMPLX_1:60; ::_thesis: verum end; theorem :: SERIES_5:16 for a, b, d, c being real positive number holds (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2 proof let a, b, d, c be real positive number ; ::_thesis: (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2 A1: b / (a + b) > b / ((a + b) + c) by XREAL_1:29, XREAL_1:76; a / (a + b) > a / ((a + b) + d) by XREAL_1:29, XREAL_1:76; then (a / (a + b)) + (b / (a + b)) > (a / ((a + b) + d)) + (b / ((a + b) + c)) by A1, XREAL_1:8; then (a + b) / (a + b) > (a / ((a + b) + d)) + (b / ((a + b) + c)) by XCMPLX_1:62; then A2: 1 > (a / ((a + b) + d)) + (b / ((a + b) + c)) by XCMPLX_1:60; a + (c + d) > c + d by XREAL_1:29; then A3: d / (c + d) > d / ((a + c) + d) by XREAL_1:76; b + (c + d) > c + d by XREAL_1:29; then c / (c + d) > c / ((b + c) + d) by XREAL_1:76; then 1 + (c / (c + d)) > ((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d)) by A2, XREAL_1:8; then (1 + (c / (c + d))) + (d / (c + d)) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) by A3, XREAL_1:8; then 1 + ((c / (c + d)) + (d / (c + d))) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) ; then 1 + ((c + d) / (c + d)) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) by XCMPLX_1:62; then 1 + 1 > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) by XCMPLX_1:60; hence (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2 ; ::_thesis: verum end; theorem :: SERIES_5:17 for a, b, c being real positive number st a + b > c & b + c > a & a + c > b holds ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) proof let a, b, c be real positive number ; ::_thesis: ( a + b > c & b + c > a & a + c > b implies ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) ) assume that A1: a + b > c and A2: b + c > a and A3: a + c > b ; ::_thesis: ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) A4: (a + c) - b > 0 by A3, XREAL_1:50; set f = (c + a) - b; set e = (b + c) - a; set d = (a + b) - c; A5: (b + c) - a > 0 by A2, XREAL_1:50; A6: (a + b) - c > 0 by A1, XREAL_1:50; then A7: (((a + b) - c) + ((b + c) - a)) + ((c + a) - b) >= 3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) by A5, A4, SERIES_3:15; ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 3 * (3 -root (((1 / ((a + b) - c)) * (1 / ((b + c) - a))) * (1 / ((c + a) - b)))) by A6, A5, A4, SERIES_3:15; then A8: ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 3 * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))) by Lm3; A9: 3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) >= 0 by A6, A5, A4, POWER:7; 3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) >= 0 by A6, A5, A4, POWER:7; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= (3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))) * (3 * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) by A7, A9, A8, XREAL_1:66; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * ((3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) ; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) * (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) by A6, A5, A4, POWER:11; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) / (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) / 1))) by XCMPLX_1:79; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root 1) by A6, A5, A4, XCMPLX_1:60; then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * 1 by POWER:6; hence ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) by XREAL_1:79; ::_thesis: verum end; theorem :: SERIES_5:18 for a, b, c, d being real positive number holds sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d)) proof let a, b, c, d be real positive number ; ::_thesis: sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d)) A1: sqrt ((a + b) * (c + d)) > 0 by SQUARE_1:25; A2: sqrt (b * d) > 0 by SQUARE_1:25; (a * d) + (b * c) >= 2 * (sqrt ((a * d) * (b * c))) by SIN_COS2:1; then ((a * d) + (b * c)) + ((a * c) + (b * d)) >= (2 * (sqrt ((a * d) * (b * c)))) + ((a * c) + (b * d)) by XREAL_1:7; then (a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + (a * c)) + (b * d) ; then (a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + ((sqrt (a * c)) ^2)) + (b * d) by SQUARE_1:def_2; then (a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + ((sqrt (a * c)) ^2)) + ((sqrt (b * d)) ^2) by SQUARE_1:def_2; then (sqrt ((a + b) * (c + d))) ^2 >= ((2 * (sqrt ((a * c) * (b * d)))) + ((sqrt (a * c)) ^2)) + ((sqrt (b * d)) ^2) by SQUARE_1:def_2; then A3: (sqrt ((a + b) * (c + d))) ^2 >= (((sqrt (a * c)) ^2) + (2 * ((sqrt (a * c)) * (sqrt (b * d))))) + ((sqrt (b * d)) ^2) by SQUARE_1:29; ((sqrt (a * c)) + (sqrt (b * d))) ^2 >= 0 by XREAL_1:63; then A4: sqrt ((sqrt ((a + b) * (c + d))) ^2) >= sqrt (((sqrt (a * c)) + (sqrt (b * d))) ^2) by A3, SQUARE_1:26; sqrt (a * c) > 0 by SQUARE_1:25; then sqrt ((sqrt ((a + b) * (c + d))) ^2) >= (sqrt (a * c)) + (sqrt (b * d)) by A4, A2, SQUARE_1:22; hence sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d)) by A1, SQUARE_1:22; ::_thesis: verum end; theorem :: SERIES_5:19 for a, b, c, d being real positive number holds ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d proof let a, b, c, d be real positive number ; ::_thesis: ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d sqrt (a * d) > 0 by SQUARE_1:25; then (a + d) ^2 >= (2 * (sqrt (a * d))) ^2 by SIN_COS2:1, SQUARE_1:15; then (a + d) ^2 >= (2 ^2) * ((sqrt (a * d)) ^2) ; then (a + d) ^2 >= (2 * 2) * (a * d) by SQUARE_1:def_2; then A1: ((a + d) ^2) * (b * c) >= ((4 * a) * d) * (b * c) by XREAL_1:64; ((a * b) + (c * d)) * ((a * c) + (b * d)) = (((sqrt (a * b)) ^2) + (c * d)) * ((a * c) + (b * d)) by SQUARE_1:def_2 .= (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * ((a * c) + (b * d)) by SQUARE_1:def_2 .= (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + (b * d)) by SQUARE_1:def_2 .= (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) by SQUARE_1:def_2 ; then ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (b * c) * ((a + d) ^2) by Lm5; hence ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th20: :: SERIES_5:20 for a, b, c being real positive number holds ((a / b) + (b / c)) + (c / a) >= 3 proof let a, b, c be real positive number ; ::_thesis: ((a / b) + (b / c)) + (c / a) >= 3 ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root (((a / b) * (b / c)) * (c / a))) by SERIES_3:15; then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root (((a * b) / (b * c)) * (c / a))) by XCMPLX_1:76; then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root ((a / c) * (c / a))) by XCMPLX_1:91; then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root ((a * c) / (c * a))) by XCMPLX_1:76; then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root 1) by XCMPLX_1:60; then ((a / b) + (b / c)) + (c / a) >= 3 * 1 by POWER:6; hence ((a / b) + (b / c)) + (c / a) >= 3 ; ::_thesis: verum end; theorem :: SERIES_5:21 for a, b, c being real positive number st ((a * b) + (b * c)) + (c * a) = 1 holds (a + b) + c >= sqrt 3 proof let a, b, c be real positive number ; ::_thesis: ( ((a * b) + (b * c)) + (c * a) = 1 implies (a + b) + c >= sqrt 3 ) assume A1: ((a * b) + (b * c)) + (c * a) = 1 ; ::_thesis: (a + b) + c >= sqrt 3 then ((a ^2) + (b ^2)) + (c ^2) >= 1 by SERIES_3:10; then (((a ^2) + (b ^2)) + (c ^2)) + 2 >= 1 + 2 by XREAL_1:6; then sqrt (((a + b) + c) ^2) >= sqrt 3 by A1, SQUARE_1:26; hence (a + b) + c >= sqrt 3 by SQUARE_1:22; ::_thesis: verum end; theorem :: SERIES_5:22 for b, c, a being real positive number holds ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3 proof let b, c, a be real positive number ; ::_thesis: ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3 A1: ((b / a) + (c / b)) + (a / c) >= 3 by Th20; ((a / b) + (b / c)) + (c / a) >= 3 by Th20; then (((a / b) + (b / c)) + (c / a)) + (((b / a) + (c / b)) + (a / c)) >= 3 + 3 by A1, XREAL_1:7; then A2: ((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3 >= 6 - 3 by XREAL_1:9; ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) = ((((b + c) / a) - (a / a)) + (((c + a) - b) / b)) + (((a + b) - c) / c) by XCMPLX_1:120 .= ((((b + c) / a) - 1) + (((c + a) - b) / b)) + (((a + b) - c) / c) by XCMPLX_1:60 .= ((((b + c) / a) - 1) + (((c + a) / b) - (b / b))) + (((a + b) - c) / c) by XCMPLX_1:120 .= ((((b + c) / a) - 1) + (((c + a) / b) - 1)) + (((a + b) - c) / c) by XCMPLX_1:60 .= (((((b + c) / a) - 1) + ((c + a) / b)) - 1) + (((a + b) / c) - (c / c)) by XCMPLX_1:120 .= (((((b + c) / a) - 1) + ((c + a) / b)) - 1) + (((a + b) / c) - 1) by XCMPLX_1:60 .= ((((b + c) / a) + ((c + a) / b)) + ((a + b) / c)) - 3 .= ((((b / a) + (c / a)) + ((c + a) / b)) + ((a + b) / c)) - 3 by XCMPLX_1:62 .= ((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a + b) / c)) - 3 by XCMPLX_1:62 .= ((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a / c) + (b / c))) - 3 by XCMPLX_1:62 .= ((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3 ; hence ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3 by A2; ::_thesis: verum end; theorem :: SERIES_5:23 for a, b being real positive number holds (a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2 proof let a, b be real positive number ; ::_thesis: (a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2 A1: sqrt (a * b) > 0 by SQUARE_1:25; A2: (a + (1 / a)) * (b + (1 / b)) = (((a * b) + (a * (1 / b))) + ((1 / a) * b)) + ((1 / a) * (1 / b)) .= (((a * b) + ((a * 1) / b)) + ((1 / a) * b)) + ((1 / a) * (1 / b)) by XCMPLX_1:74 .= (((a * b) + ((a * 1) / b)) + ((b * 1) / a)) + ((1 / a) * (1 / b)) by XCMPLX_1:74 .= (((a * b) + ((a * 1) / b)) + ((b * 1) / a)) + ((1 * 1) / (a * b)) by XCMPLX_1:76 .= (((a * b) + (a / b)) + (b / a)) + (1 / (a * b)) ; (a / b) + (b / a) >= 2 * (sqrt ((a / b) * (b / a))) by SIN_COS2:1; then (a / b) + (b / a) >= 2 * (sqrt ((a * b) / (b * a))) by XCMPLX_1:76; then (a / b) + (b / a) >= 2 * 1 by SQUARE_1:18, XCMPLX_1:60; then A3: ((a / b) + (b / a)) + ((a * b) + (1 / (a * b))) >= 2 + ((a * b) + (1 / (a * b))) by XREAL_1:6; ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2 = (((sqrt (a * b)) ^2) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 / (sqrt (a * b))) ^2) .= ((a * b) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 / (sqrt (a * b))) ^2) by SQUARE_1:def_2 .= ((a * b) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 ^2) / ((sqrt (a * b)) ^2)) by XCMPLX_1:76 .= ((a * b) + (2 * ((sqrt (a * b)) * (1 / (sqrt (a * b)))))) + (1 / (a * b)) by SQUARE_1:def_2 .= ((a * b) + (2 * (((sqrt (a * b)) * 1) / (sqrt (a * b))))) + (1 / (a * b)) by XCMPLX_1:74 .= ((a * b) + (2 * 1)) + (1 / (a * b)) by A1, XCMPLX_1:60 .= ((a * b) + 2) + (1 / (a * b)) ; hence (a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2 by A2, A3; ::_thesis: verum end; theorem :: SERIES_5:24 for b, c, a being real positive number holds (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c proof let b, c, a be real positive number ; ::_thesis: (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c A1: ((a * c) / b) + ((a * b) / c) = (a * (c / b)) + ((a * b) / c) by XCMPLX_1:74 .= (a * (c / b)) + (a * (b / c)) by XCMPLX_1:74 .= a * ((c / b) + (b / c)) ; A2: ((a * b) / c) + ((b * c) / a) = (b * (a / c)) + ((b * c) / a) by XCMPLX_1:74 .= (b * (a / c)) + (b * (c / a)) by XCMPLX_1:74 .= b * ((a / c) + (c / a)) ; A3: b * ((a / c) + (c / a)) >= b * 2 by SERIES_3:3, XREAL_1:64; A4: c * ((b / a) + (a / b)) >= c * 2 by SERIES_3:3, XREAL_1:64; a * ((c / b) + (b / c)) >= a * 2 by SERIES_3:3, XREAL_1:64; then (a * ((c / b) + (b / c))) + (b * ((a / c) + (c / a))) >= (a * 2) + (b * 2) by A3, XREAL_1:7; then A5: ((a * ((c / b) + (b / c))) + (b * ((a / c) + (c / a)))) + (c * ((b / a) + (a / b))) >= ((a * 2) + (b * 2)) + (c * 2) by A4, XREAL_1:7; ((b * c) / a) + ((a * c) / b) = (c * (b / a)) + ((a * c) / b) by XCMPLX_1:74 .= (c * (b / a)) + (c * (a / b)) by XCMPLX_1:74 .= c * ((b / a) + (a / b)) ; then (2 * ((((b * c) / a) + ((a * c) / b)) + ((a * b) / c))) / 2 >= (2 * ((a + b) + c)) / 2 by A1, A2, A5, XREAL_1:72; hence (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c ; ::_thesis: verum end; theorem :: SERIES_5:25 for x, y, z being real number st x > y & y > z holds (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2)) proof let x, y, z be real number ; ::_thesis: ( x > y & y > z implies (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2)) ) assume that A1: x > y and A2: y > z ; ::_thesis: (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2)) A3: y - z > 0 by A2, XREAL_1:50; x > z by A1, A2, XXREAL_0:2; then A4: x - z > 0 by XREAL_1:50; x - y > 0 by A1, XREAL_1:50; then ((x - y) * (y - z)) * (x - z) > 0 by A3, A4; then ((((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x)) - (((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2))) > 0 ; hence (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2)) by XREAL_1:47; ::_thesis: verum end; theorem :: SERIES_5:26 for a, b, c being real positive number st a > b & b > c holds b / (a - b) > c / (a - c) proof let a, b, c be real positive number ; ::_thesis: ( a > b & b > c implies b / (a - b) > c / (a - c) ) assume that A1: a > b and A2: b > c ; ::_thesis: b / (a - b) > c / (a - c) A3: a - b > 0 by A1, XREAL_1:50; b * (- 1) < c * (- 1) by A2, XREAL_1:69; then (- b) + a < (- c) + a by XREAL_1:8; then A4: c / (a - b) > c / (a - c) by A3, XREAL_1:76; b / (a - b) > c / (a - b) by A2, A3, XREAL_1:74; hence b / (a - b) > c / (a - c) by A4, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:27 for b, a, c, d being real positive number st b > a & c > d holds c / (c + a) > d / (d + b) proof let b, a, c, d be real positive number ; ::_thesis: ( b > a & c > d implies c / (c + a) > d / (d + b) ) assume that A1: b > a and A2: c > d ; ::_thesis: c / (c + a) > d / (d + b) b * c > a * d by A1, A2, XREAL_1:96; then (b * c) + (c * d) > (a * d) + (c * d) by XREAL_1:8; then c * (b + d) > d * (a + c) ; hence c / (c + a) > d / (d + b) by XREAL_1:106; ::_thesis: verum end; theorem :: SERIES_5:28 for m, x, z, y being real number holds (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) proof let m, x, z, y be real number ; ::_thesis: (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) A1: z ^2 >= 0 by XREAL_1:63; A2: m ^2 >= 0 by XREAL_1:63; then A3: sqrt ((m ^2) + (z ^2)) >= 0 by A1, SQUARE_1:def_2; A4: ((m * x) + (z * y)) ^2 >= 0 by XREAL_1:63; ((m * y) ^2) + ((z * x) ^2) >= (2 * (m * y)) * (z * x) by SERIES_3:6; then A5: (((m * y) ^2) + ((z * x) ^2)) + (((m ^2) * (x ^2)) + ((z ^2) * (y ^2))) >= ((((2 * m) * x) * y) * z) + (((m ^2) * (x ^2)) + ((z ^2) * (y ^2))) by XREAL_1:6; A6: y ^2 >= 0 by XREAL_1:63; A7: x ^2 >= 0 by XREAL_1:63; then A8: sqrt ((x ^2) + (y ^2)) >= 0 by A6, SQUARE_1:def_2; ((sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2)))) ^2 = ((sqrt ((m ^2) + (z ^2))) ^2) * ((sqrt ((x ^2) + (y ^2))) ^2) .= ((m ^2) + (z ^2)) * ((sqrt ((x ^2) + (y ^2))) ^2) by A2, A1, SQUARE_1:def_2 .= ((m ^2) + (z ^2)) * ((x ^2) + (y ^2)) by A7, A6, SQUARE_1:def_2 .= ((((m ^2) * (x ^2)) + ((m * y) ^2)) + ((z * x) ^2)) + ((z ^2) * (y ^2)) ; then sqrt (((sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2)))) ^2) >= sqrt (((m * x) + (z * y)) ^2) by A5, A4, SQUARE_1:26; then A9: (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) >= sqrt (((m * x) + (z * y)) ^2) by A3, A8, SQUARE_1:22; percases ( (m * x) + (z * y) > 0 or (m * x) + (z * y) = 0 or (m * x) + (z * y) < 0 ) ; suppose (m * x) + (z * y) > 0 ; ::_thesis: (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) hence (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) by A9, SQUARE_1:22; ::_thesis: verum end; suppose (m * x) + (z * y) = 0 ; ::_thesis: (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) hence (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) by A3, A8; ::_thesis: verum end; suppose (m * x) + (z * y) < 0 ; ::_thesis: (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) hence (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) by A3, A8; ::_thesis: verum end; end; end; theorem Th29: :: SERIES_5:29 for m, x, u, y, w, z being real number holds (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2) + (u ^2)) + (w ^2)) * (((x ^2) + (y ^2)) + (z ^2)) proof let m, x, u, y, w, z be real number ; ::_thesis: (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2) + (u ^2)) + (w ^2)) * (((x ^2) + (y ^2)) + (z ^2)) ((m ^2) * (z ^2)) + ((w ^2) * (x ^2)) = ((m * z) ^2) + ((w * x) ^2) ; then A1: ((m ^2) * (z ^2)) + ((w ^2) * (x ^2)) >= (2 * (m * z)) * (w * x) by SERIES_3:6; ((u ^2) * (z ^2)) + ((w ^2) * (y ^2)) = ((u * z) ^2) + ((w * y) ^2) ; then A2: ((u ^2) * (z ^2)) + ((w ^2) * (y ^2)) >= (2 * (u * z)) * (w * y) by SERIES_3:6; ((m * y) ^2) + ((u * x) ^2) >= (2 * (m * y)) * (u * x) by SERIES_3:6; then (((m ^2) * (y ^2)) + ((u ^2) * (x ^2))) + (((m ^2) * (z ^2)) + ((w ^2) * (x ^2))) >= ((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x) by A1, XREAL_1:7; then (((((m ^2) * (y ^2)) + ((u ^2) * (x ^2))) + ((m ^2) * (z ^2))) + ((w ^2) * (x ^2))) + (((u ^2) * (z ^2)) + ((w ^2) * (y ^2))) >= (((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x)) + ((((2 * u) * z) * w) * y) by A2, XREAL_1:7; then (((((((m ^2) * (y ^2)) + ((u ^2) * (x ^2))) + ((m ^2) * (z ^2))) + ((w ^2) * (x ^2))) + ((u ^2) * (z ^2))) + ((w ^2) * (y ^2))) + ((((m * x) ^2) + ((u * y) ^2)) + ((w * z) ^2)) >= ((((((2 * m) * y) * u) * x) + ((((2 * m) * z) * w) * x)) + ((((2 * u) * z) * w) * y)) + ((((m * x) ^2) + ((u * y) ^2)) + ((w * z) ^2)) by XREAL_1:6; hence (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2) + (u ^2)) + (w ^2)) * (((x ^2) + (y ^2)) + (z ^2)) ; ::_thesis: verum end; theorem :: SERIES_5:30 for a, b, c being real positive number holds (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c proof let a, b, c be real positive number ; ::_thesis: (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c A1: (b ^2) * (a + c) >= (b ^2) * (2 * (sqrt (a * c))) by SIN_COS2:1, XREAL_1:64; A2: (c ^2) * (a + b) >= (c ^2) * (2 * (sqrt (a * b))) by SIN_COS2:1, XREAL_1:64; A3: sqrt (a * b) > 0 by SQUARE_1:25; A4: sqrt (a * c) > 0 by SQUARE_1:25; sqrt (b * c) > 0 by SQUARE_1:25; then (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((2 * (a ^2)) * (sqrt (b * c))) * ((2 * (b ^2)) * (sqrt (a * c)))) * ((2 * (c ^2)) * (sqrt (a * b))))) by A4, A3, SERIES_3:15; then (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b)))) ; then (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((2 * a) * b) * c) |^ 3)) by Lm9; then A5: (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (((2 * a) * b) * c) by POWER:4; A6: ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c by SERIES_3:12; (a ^2) * (b + c) >= (a ^2) * (2 * (sqrt (b * c))) by SIN_COS2:1, XREAL_1:64; then ((a ^2) * (b + c)) + ((b ^2) * (a + c)) >= ((a ^2) * (2 * (sqrt (b * c)))) + ((b ^2) * (2 * (sqrt (a * c)))) by A1, XREAL_1:7; then (((a ^2) * (b + c)) + ((b ^2) * (a + c))) + ((c ^2) * (a + b)) >= (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) by A2, XREAL_1:7; then (((((a * (b ^2)) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2)) >= ((6 * a) * b) * c by A5, XXREAL_0:2; then A7: (((a |^ 3) + (b |^ 3)) + (c |^ 3)) + ((((((a * (b ^2)) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) >= (((3 * a) * b) * c) + (((6 * a) * b) * c) by A6, XREAL_1:7; (((a ^2) + (b ^2)) + (c ^2)) * ((a + b) + c) = ((((((((a * (a ^2)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2)) .= ((((((((a * (a |^ 2)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2)) by NEWTON:81 .= ((((((((a |^ (2 + 1)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2)) by NEWTON:6 .= ((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b |^ 2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2)) by NEWTON:81 .= ((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ (2 + 1))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2)) by NEWTON:6 .= ((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ 3)) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c |^ 2)) by NEWTON:81 .= ((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ 3)) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c |^ (2 + 1)) by NEWTON:6 .= ((((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2)) ; then (((a + b) + c) * (((a ^2) + (b ^2)) + (c ^2))) / (((a ^2) + (b ^2)) + (c ^2)) >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) by A7, XREAL_1:72; then ((a + b) + c) / ((((a ^2) + (b ^2)) + (c ^2)) / (((a ^2) + (b ^2)) + (c ^2))) >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) by XCMPLX_1:77; then ((a + b) + c) / 1 >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) by XCMPLX_1:60; hence (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c ; ::_thesis: verum end; theorem :: SERIES_5:31 for a, b, c being real positive number holds (a + b) + c <= ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) proof let a, b, c be real positive number ; ::_thesis: (a + b) + c <= ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) A1: sqrt 3 > 0 by SQUARE_1:25; A2: sqrt (((c ^2) + (c * a)) + (a ^2)) >= ((1 / 2) * (sqrt 3)) * (c + a) by Lm11; A3: sqrt (((b ^2) + (b * c)) + (c ^2)) >= ((1 / 2) * (sqrt 3)) * (b + c) by Lm11; sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b) by Lm11; then (sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2))) >= (((1 / 2) * (sqrt 3)) * (a + b)) + (((1 / 2) * (sqrt 3)) * (b + c)) by A3, XREAL_1:7; then ((sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2)))) + (sqrt (((c ^2) + (c * a)) + (a ^2))) >= ((((1 / 2) * (sqrt 3)) * (a + b)) + (((1 / 2) * (sqrt 3)) * (b + c))) + (((1 / 2) * (sqrt 3)) * (c + a)) by A2, XREAL_1:7; then (((sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2)))) + (sqrt (((c ^2) + (c * a)) + (a ^2)))) / (sqrt 3) >= (((a + b) + c) * (sqrt 3)) / (sqrt 3) by A1, XREAL_1:72; then (((sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2)))) + (sqrt (((c ^2) + (c * a)) + (a ^2)))) / (sqrt 3) >= ((a + b) + c) * ((sqrt 3) / (sqrt 3)) by XCMPLX_1:74; then (((sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2)))) + (sqrt (((c ^2) + (c * a)) + (a ^2)))) / (sqrt 3) >= ((a + b) + c) * 1 by A1, XCMPLX_1:60; then (((sqrt (((a ^2) + (a * b)) + (b ^2))) + (sqrt (((b ^2) + (b * c)) + (c ^2)))) / (sqrt 3)) + ((sqrt (((c ^2) + (c * a)) + (a ^2))) / (sqrt 3)) >= (a + b) + c by XCMPLX_1:62; then (((sqrt (((a ^2) + (a * b)) + (b ^2))) / (sqrt 3)) + ((sqrt (((b ^2) + (b * c)) + (c ^2))) / (sqrt 3))) + ((sqrt (((c ^2) + (c * a)) + (a ^2))) / (sqrt 3)) >= (a + b) + c by XCMPLX_1:62; then ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + ((sqrt (((b ^2) + (b * c)) + (c ^2))) / (sqrt 3))) + ((sqrt (((c ^2) + (c * a)) + (a ^2))) / (sqrt 3)) >= (a + b) + c by SQUARE_1:30; then ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + ((sqrt (((c ^2) + (c * a)) + (a ^2))) / (sqrt 3)) >= (a + b) + c by SQUARE_1:30; hence (a + b) + c <= ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) by SQUARE_1:30; ::_thesis: verum end; theorem :: SERIES_5:32 for a, b, c being real positive number holds ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) <= ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) proof let a, b, c be real positive number ; ::_thesis: ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) <= ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) A1: sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3) <= sqrt (((b ^2) + (c ^2)) / 2) by Lm12; A2: sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3) <= sqrt (((c ^2) + (a ^2)) / 2) by Lm12; sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) by Lm12; then (sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3)) <= (sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2)) by A1, XREAL_1:7; hence ((sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3)) + (sqrt ((((b ^2) + (b * c)) + (c ^2)) / 3))) + (sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3)) <= ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) by A2, XREAL_1:7; ::_thesis: verum end; theorem :: SERIES_5:33 for a, b, c being real positive number holds ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) <= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) proof let a, b, c be real positive number ; ::_thesis: ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) <= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) A1: (sqrt (((a ^2) + (b ^2)) / 2)) ^2 = ((a ^2) + (b ^2)) / 2 by SQUARE_1:def_2; A2: (sqrt (((b ^2) + (c ^2)) / 2)) ^2 = ((b ^2) + (c ^2)) / 2 by SQUARE_1:def_2; A3: sqrt (((c ^2) + (a ^2)) / 2) > 0 by SQUARE_1:25; A4: sqrt (((b ^2) + (c ^2)) / 2) > 0 by SQUARE_1:25; A5: (((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2))) ^2 >= 0 by XREAL_1:63; A6: sqrt (((a ^2) + (b ^2)) / 2) > 0 by SQUARE_1:25; A7: (sqrt (((c ^2) + (a ^2)) / 2)) ^2 = ((c ^2) + (a ^2)) / 2 by SQUARE_1:def_2; (((1 * (sqrt (((a ^2) + (b ^2)) / 2))) + (1 * (sqrt (((b ^2) + (c ^2)) / 2)))) + (1 * (sqrt (((c ^2) + (a ^2)) / 2)))) ^2 <= (((1 ^2) + (1 ^2)) + (1 ^2)) * ((((sqrt (((a ^2) + (b ^2)) / 2)) ^2) + ((sqrt (((b ^2) + (c ^2)) / 2)) ^2)) + ((sqrt (((c ^2) + (a ^2)) / 2)) ^2)) by Th29; then sqrt ((((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2))) ^2) <= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) by A1, A2, A7, A5, SQUARE_1:26; hence ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) <= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) by A6, A4, A3, SQUARE_1:22; ::_thesis: verum end; theorem :: SERIES_5:34 for a, b, c being real positive number holds sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c) proof let a, b, c be real positive number ; ::_thesis: sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c) A1: (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2) by Lm13; A2: (((c * a) / b) ^2) + (((a * b) / c) ^2) >= 2 * (a ^2) by Lm13; (((b * c) / a) ^2) + (((a * b) / c) ^2) >= 2 * (b ^2) by Lm13; then ((((c * a) / b) ^2) + (((a * b) / c) ^2)) + ((((b * c) / a) ^2) + (((a * b) / c) ^2)) >= (2 * (a ^2)) + (2 * (b ^2)) by A2, XREAL_1:7; then ((((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (((a * b) / c) ^2)) + ((((b * c) / a) ^2) + (((c * a) / b) ^2)) >= ((2 * (a ^2)) + (2 * (b ^2))) + (2 * (c ^2)) by A1, XREAL_1:7; then ((((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) * 2) / 2 >= ((((a ^2) + (b ^2)) + (c ^2)) * 2) / 2 by XREAL_1:72; then (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) >= (((a ^2) + (b ^2)) + (c ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2))) by XREAL_1:6; then ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 >= 3 * (((a ^2) + (b ^2)) + (c ^2)) by Lm16; then sqrt (((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2) >= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) by SQUARE_1:26; hence sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c) by SQUARE_1:22; ::_thesis: verum end; theorem :: SERIES_5:35 for a, b being real positive number st a + b = 1 holds ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 proof let a, b be real positive number ; ::_thesis: ( a + b = 1 implies ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 ) assume A1: a + b = 1 ; ::_thesis: ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 sqrt (a * b) > 0 by SQUARE_1:25; then 1 ^2 >= (2 * (sqrt (a * b))) ^2 by A1, SIN_COS2:1, SQUARE_1:15; then 1 >= (2 * 2) * ((sqrt (a * b)) ^2) ; then 1 >= 4 * (a * b) by SQUARE_1:def_2; then 8 / 1 <= 8 / ((4 * a) * b) by XREAL_1:118; then 8 <= 8 / (4 * (a * b)) ; then 8 <= (8 / 4) / (a * b) by XCMPLX_1:78; then A2: 8 + 1 <= (2 / (a * b)) + 1 by XREAL_1:7; ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) = ((1 - (1 * (a ^2))) / (a ^2)) * ((1 / (b ^2)) - 1) by XCMPLX_1:126 .= ((1 - (1 * (a ^2))) / (a ^2)) * ((1 - (1 * (b ^2))) / (b ^2)) by XCMPLX_1:126 .= (((1 - a) * (1 + a)) * ((1 - b) * (1 + b))) / ((a ^2) * (b ^2)) by XCMPLX_1:76 ; then ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) = ((a * b) * ((1 + a) * (1 + b))) / ((a * b) * (a * b)) by A1 .= ((a * b) / (a * b)) * (((1 + a) * (1 + b)) / (a * b)) by XCMPLX_1:76 .= 1 * (((1 + a) * (1 + b)) / (a * b)) by XCMPLX_1:60 .= ((1 + (a + b)) + (a * b)) / (a * b) .= (2 / (a * b)) + ((a * b) / (a * b)) by A1, XCMPLX_1:62 .= (2 / (a * b)) + 1 by XCMPLX_1:60 ; hence ((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9 by A2; ::_thesis: verum end; theorem :: SERIES_5:36 for a, b being real positive number st a + b = 1 holds (a * b) + (1 / (a * b)) >= 17 / 4 proof let a, b be real positive number ; ::_thesis: ( a + b = 1 implies (a * b) + (1 / (a * b)) >= 17 / 4 ) A1: sqrt (a * b) > 0 by SQUARE_1:25; assume a + b = 1 ; ::_thesis: (a * b) + (1 / (a * b)) >= 17 / 4 then 1 ^2 >= (2 * (sqrt (a * b))) ^2 by A1, SIN_COS2:1, SQUARE_1:15; then 1 >= (2 * 2) * ((sqrt (a * b)) ^2) ; then 1 >= 4 * (a * b) by SQUARE_1:def_2; then A2: 1 / 4 >= ((a * b) * 4) / 4 by XREAL_1:72; then (1 / 4) * (- 1) <= (a * b) * (- 1) by XREAL_1:65; then (- (1 / 4)) + 1 <= (- (a * b)) + 1 by XREAL_1:7; then (3 / 4) ^2 <= (1 - (a * b)) ^2 by SQUARE_1:15; then (9 / (4 ^2)) / (1 / 4) <= ((1 - (a * b)) ^2) / (1 / 4) by XREAL_1:72; then A3: (9 / 4) + (8 / 4) <= (((1 - (a * b)) ^2) * 4) + 2 by XREAL_1:7; (1 - (a * b)) ^2 >= 0 by XREAL_1:63; then ((1 - (a * b)) ^2) / (1 / 4) <= ((1 - (a * b)) ^2) / (a * b) by A2, XREAL_1:118; then A4: (((1 - (a * b)) ^2) * 4) + 2 <= (((1 - (a * b)) ^2) / (a * b)) + 2 by XREAL_1:7; (1 / (a * b)) + (a * b) = (1 + ((a * b) * (a * b))) / (a * b) by XCMPLX_1:113 .= ((((1 ^2) - ((2 * 1) * (a * b))) + ((a * b) ^2)) + (2 * (a * b))) / (a * b) .= (((1 - (a * b)) ^2) / (a * b)) + ((2 * (a * b)) / (a * b)) by XCMPLX_1:62 .= (((1 - (a * b)) ^2) / (a * b)) + (2 * ((a * b) / (a * b))) by XCMPLX_1:74 .= (((1 - (a * b)) ^2) / (a * b)) + (2 * 1) by XCMPLX_1:60 .= (((1 - (a * b)) ^2) / (a * b)) + 2 ; hence (a * b) + (1 / (a * b)) >= 17 / 4 by A4, A3, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:37 for a, b, c being real positive number st (a + b) + c = 1 holds ((1 / a) + (1 / b)) + (1 / c) >= 9 proof let a, b, c be real positive number ; ::_thesis: ( (a + b) + c = 1 implies ((1 / a) + (1 / b)) + (1 / c) >= 9 ) assume A1: (a + b) + c = 1 ; ::_thesis: ((1 / a) + (1 / b)) + (1 / c) >= 9 A2: 3 -root ((a * b) * c) >= 0 by POWER:7; ((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (((1 / a) * (1 / b)) * (1 / c))) by SERIES_3:15; then A3: ((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (1 / ((a * b) * c))) by Lm3; A4: 3 -root (1 / ((a * b) * c)) >= 0 by POWER:7; (a + b) + c >= 3 * (3 -root ((a * b) * c)) by SERIES_3:15; then ((a + b) + c) * (((1 / a) + (1 / b)) + (1 / c)) >= (3 * (3 -root ((a * b) * c))) * (3 * (3 -root (1 / ((a * b) * c)))) by A2, A3, A4, XREAL_1:66; then ((1 / a) + (1 / b)) + (1 / c) >= 9 * ((3 -root ((a * b) * c)) * (3 -root (1 / ((a * b) * c)))) by A1; then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root (((a * b) * c) * (1 / ((a * b) * c)))) by POWER:11; then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root (((a * b) * c) / (((a * b) * c) / 1))) by XCMPLX_1:79; then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root 1) by XCMPLX_1:60; then ((1 / a) + (1 / b)) + (1 / c) >= 9 * 1 by POWER:6; hence ((1 / a) + (1 / b)) + (1 / c) >= 9 ; ::_thesis: verum end; theorem :: SERIES_5:38 for a, b, c being real positive number st (a + b) + c = 1 holds (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 proof let a, b, c be real positive number ; ::_thesis: ( (a + b) + c = 1 implies (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 ) A1: (a + c) / b >= (2 * (sqrt (a * c))) / b by SIN_COS2:1, XREAL_1:72; A2: (a + b) / c >= (2 * (sqrt (a * b))) / c by SIN_COS2:1, XREAL_1:72; A3: sqrt (a * b) > 0 by SQUARE_1:25; A4: sqrt (a * c) > 0 by SQUARE_1:25; assume A5: (a + b) + c = 1 ; ::_thesis: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 then A6: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) = (((b + c) / a) * ((1 / b) - 1)) * ((1 / c) - 1) by Lm17 .= (((b + c) / a) * ((a + c) / b)) * ((1 / c) - 1) by A5, Lm17 .= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + (c / c)) - 1) by A5, XCMPLX_1:62 .= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + 1) - 1) by XCMPLX_1:60 .= (((b + c) / a) * ((a + c) / b)) * ((a + b) / c) ; A7: sqrt (b * c) > 0 by SQUARE_1:25; (b + c) / a >= (2 * (sqrt (b * c))) / a by SIN_COS2:1, XREAL_1:72; then ((b + c) / a) * ((a + c) / b) >= ((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b) by A1, A7, A4, XREAL_1:66; then (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) by A6, A2, A7, A4, A3, XREAL_1:66; hence (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 by Lm18; ::_thesis: verum end; theorem :: SERIES_5:39 for a, b, c being real positive number st (a + b) + c = 1 holds ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 proof let a, b, c be real positive number ; ::_thesis: ( (a + b) + c = 1 implies ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 ) A1: sqrt (b * c) > 0 by SQUARE_1:25; (a + b) / c >= (2 * (sqrt (a * b))) / c by SIN_COS2:1, XREAL_1:72; then 2 + ((a + b) / c) >= 2 + ((2 * (sqrt (a * b))) / c) by XREAL_1:6; then A2: 2 + ((a + b) / c) >= 2 + (2 * ((sqrt (a * b)) / c)) by XCMPLX_1:74; A3: sqrt (a * b) > 0 by SQUARE_1:25; (a + c) / b >= (2 * (sqrt (a * c))) / b by SIN_COS2:1, XREAL_1:72; then 2 + ((a + c) / b) >= 2 + ((2 * (sqrt (a * c))) / b) by XREAL_1:6; then A4: 2 + ((a + c) / b) >= 2 + (2 * ((sqrt (a * c)) / b)) by XCMPLX_1:74; A5: sqrt (a * c) > 0 by SQUARE_1:25; (b + c) / a >= (2 * (sqrt (b * c))) / a by SIN_COS2:1, XREAL_1:72; then 2 + ((b + c) / a) >= 2 + ((2 * (sqrt (b * c))) / a) by XREAL_1:6; then 2 + ((b + c) / a) >= 2 + (2 * ((sqrt (b * c)) / a)) by XCMPLX_1:74; then (2 + ((b + c) / a)) * (2 + ((a + c) / b)) >= (2 * (1 + ((sqrt (b * c)) / a))) * (2 * (1 + ((sqrt (a * c)) / b))) by A4, A1, A5, XREAL_1:66; then A6: ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (2 + ((a + b) / c)) >= ((2 * (1 + ((sqrt (b * c)) / a))) * (2 * (1 + ((sqrt (a * c)) / b)))) * (2 * (1 + ((sqrt (a * b)) / c))) by A2, A1, A5, A3, XREAL_1:66; ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6 by Lm23; then 2 + (((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) >= 6 + 2 by XREAL_1:6; then A7: 8 * ((((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) >= 8 * 8 by XREAL_1:64; assume A8: (a + b) + c = 1 ; ::_thesis: ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 then ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) = ((2 + ((b + c) / a)) * (1 + (1 / b))) * (1 + (1 / c)) by Lm19 .= ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (1 + (1 / c)) by A8, Lm19 .= ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (1 + (((a + b) / c) + (c / c))) by A8, XCMPLX_1:62 .= ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * ((1 + ((a + b) / c)) + 1) by XCMPLX_1:60 .= ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (2 + ((a + b) / c)) ; then ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 8 * (((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c))) by A6; then ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 8 * ((((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) by Lm22; hence ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 by A7, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:40 for x, y, z being real number st (x + y) + z = 1 holds ((x ^2) + (y ^2)) + (z ^2) >= 1 / 3 proof let x, y, z be real number ; ::_thesis: ( (x + y) + z = 1 implies ((x ^2) + (y ^2)) + (z ^2) >= 1 / 3 ) A1: ((y ^2) + (z ^2)) / 2 >= y * z by SERIES_3:7; A2: ((x ^2) + (z ^2)) / 2 >= x * z by SERIES_3:7; ((x ^2) + (y ^2)) / 2 >= x * y by SERIES_3:7; then (((x ^2) + (y ^2)) / 2) + (((y ^2) + (z ^2)) / 2) >= (y * z) + (x * y) by A1, XREAL_1:7; then ((((x ^2) + (y ^2)) / 2) + (((y ^2) + (z ^2)) / 2)) + (((x ^2) + (z ^2)) / 2) >= ((y * z) + (x * y)) + (x * z) by A2, XREAL_1:7; then - (((((x ^2) + (y ^2)) / 2) + (((y ^2) + (z ^2)) / 2)) + (((x ^2) + (z ^2)) / 2)) <= - (((y * z) + (x * y)) + (x * z)) by XREAL_1:24; then (- (((((x ^2) + (y ^2)) / 2) + (((y ^2) + (z ^2)) / 2)) + (((x ^2) + (z ^2)) / 2))) * 2 <= (- (((y * z) + (x * y)) + (x * z))) * 2 by XREAL_1:64; then (- ((((((x ^2) + (y ^2)) / 2) + (((y ^2) + (z ^2)) / 2)) + (((x ^2) + (z ^2)) / 2)) * 2)) + 1 <= (- ((((y * z) + (x * y)) + (x * z)) * 2)) + 1 by XREAL_1:6; then A3: 1 - ((((x ^2) + (y ^2)) + (z ^2)) * 2) <= 1 - ((((y * z) + (x * y)) + (x * z)) * 2) ; assume (x + y) + z = 1 ; ::_thesis: ((x ^2) + (y ^2)) + (z ^2) >= 1 / 3 then (((((x ^2) + (y ^2)) + (z ^2)) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x) = 1 ^2 by Lm6; then 1 <= (((x ^2) + (y ^2)) + (z ^2)) + ((((x ^2) + (y ^2)) + (z ^2)) * 2) by A3, XREAL_1:20; then 1 / 3 <= ((((x ^2) + (y ^2)) + (z ^2)) * 3) / 3 by XREAL_1:72; hence ((x ^2) + (y ^2)) + (z ^2) >= 1 / 3 ; ::_thesis: verum end; theorem :: SERIES_5:41 for x, y, z being real number st (x + y) + z = 1 holds ((x * y) + (y * z)) + (z * x) <= 1 / 3 proof let x, y, z be real number ; ::_thesis: ( (x + y) + z = 1 implies ((x * y) + (y * z)) + (z * x) <= 1 / 3 ) ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) by SERIES_3:10; then A1: (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * y) + (y * z)) + (z * x))) >= (((x * y) + (y * z)) + (x * z)) + (2 * (((x * y) + (y * z)) + (z * x))) by XREAL_1:7; assume (x + y) + z = 1 ; ::_thesis: ((x * y) + (y * z)) + (z * x) <= 1 / 3 then 1 ^2 = (((((x ^2) + (y ^2)) + (z ^2)) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x) by Lm6; then 1 / 3 >= (3 * (((x * y) + (y * z)) + (z * x))) / 3 by A1, XREAL_1:72; hence ((x * y) + (y * z)) + (z * x) <= 1 / 3 ; ::_thesis: verum end; theorem :: SERIES_5:42 for a, b, c being real positive number st a > b & b > c holds ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) proof let a, b, c be real positive number ; ::_thesis: ( a > b & b > c implies ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) ) assume that A1: a > b and A2: b > c ; ::_thesis: ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) A3: b / c > 1 by A2, XREAL_1:187; set e = ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)); A4: b to_power (c + a) > 0 by POWER:34; b - c > 0 by A2, XREAL_1:50; then A5: (b / c) to_power (b - c) > 1 by A3, POWER:35; A6: a / b > 1 by A1, XREAL_1:187; a - b > 0 by A1, XREAL_1:50; then (a / b) to_power (a - b) > 1 by A6, POWER:35; then A7: ((a / b) to_power (a - b)) * ((b / c) to_power (b - c)) > 1 by A5, XREAL_1:161; A8: c to_power (a + b) > 0 by POWER:34; A9: a > c by A1, A2, XXREAL_0:2; then A10: a / c > 1 by XREAL_1:187; set d = ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)); A11: a to_power (b + c) > 0 by POWER:34; a - c > 0 by A9, XREAL_1:50; then (a / c) to_power (a - c) > 1 by A10, POWER:35; then (((a / b) to_power (a - b)) * ((b / c) to_power (b - c))) * ((a / c) to_power (- (c - a))) > 1 by A7, XREAL_1:161; then (((a / b) to_power (a - b)) * ((b / c) to_power (b - c))) * ((c / a) to_power (c - a)) > 1 by Lm4; then (((a to_power (a - b)) / (b to_power (a - b))) * ((b / c) to_power (b - c))) * ((c / a) to_power (c - a)) > 1 by POWER:31; then (((a to_power (a - b)) / (b to_power (a - b))) * ((b to_power (b - c)) / (c to_power (b - c)))) * ((c / a) to_power (c - a)) > 1 by POWER:31; then (((a to_power (a - b)) / (b to_power (a - b))) * ((b to_power (b - c)) / (c to_power (b - c)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by POWER:31; then (((a to_power (a - b)) * (b to_power (b - c))) / ((c to_power (b - c)) * (b to_power (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by XCMPLX_1:76; then (((a to_power (a - b)) / (c to_power (b - c))) * ((b to_power (b - c)) / (b to_power (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by XCMPLX_1:76; then (((a to_power (a - b)) / (c to_power (b - c))) * (b to_power ((b - c) - (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by POWER:29; then (((a to_power (a - b)) / (c to_power (b - c))) * ((c to_power (c - a)) / (a to_power (c - a)))) * (b to_power (((2 * b) - a) - c)) > 1 ; then (((a to_power (a - b)) / (a to_power (c - a))) * ((c to_power (c - a)) / (c to_power (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by XCMPLX_1:85; then ((a to_power ((a - b) - (c - a))) * ((c to_power (c - a)) / (c to_power (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by POWER:29; then ((a to_power (((2 * a) - b) - c)) * (c to_power ((c - a) - (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by POWER:29; then ((a to_power ((2 * a) - (b + c))) * (c to_power ((2 * c) - (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 ; then (((a to_power (2 * a)) / (a to_power (b + c))) * (c to_power ((2 * c) - (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by POWER:29; then (((a to_power (2 * a)) / (a to_power (b + c))) * ((c to_power (2 * c)) / (c to_power (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by POWER:29; then (((a to_power (2 * a)) * (c to_power (2 * c))) / ((a to_power (b + c)) * (c to_power (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by XCMPLX_1:76; then (((a to_power (2 * a)) * (c to_power (2 * c))) / ((a to_power (b + c)) * (c to_power (a + b)))) * ((b to_power (2 * b)) / (b to_power (a + c))) > 1 by POWER:29; then (((a to_power (2 * a)) * (c to_power (2 * c))) * (b to_power (2 * b))) / (((a to_power (b + c)) * (c to_power (a + b))) * (b to_power (a + c))) > 1 by XCMPLX_1:76; then ((((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c))) / (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)))) * (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b))) > 1 * (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b))) by A11, A4, A8, XREAL_1:68; hence ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) by A11, A4, A8, XCMPLX_1:87; ::_thesis: verum end; theorem :: SERIES_5:43 for a, b being real positive number for n being Element of NAT st n >= 1 holds (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) proof let a, b be real positive number ; ::_thesis: for n being Element of NAT st n >= 1 holds (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) let n be Element of NAT ; ::_thesis: ( n >= 1 implies (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) ) assume A1: n >= 1 ; ::_thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) percases ( a - b > 0 or a - b = 0 or a - b < 0 ) ; supposeA2: a - b > 0 ; ::_thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) then (a - b) + b > 0 + b by XREAL_1:8; then a |^ n > b |^ n by A1, PREPOWER:10; then (a |^ n) - (b |^ n) > 0 by XREAL_1:50; then (a - b) * ((a |^ n) - (b |^ n)) > 0 by A2; then (((a * (a |^ n)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 ; then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 by NEWTON:6; then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b |^ (n + 1)) > 0 by NEWTON:6; then ((((a |^ (n + 1)) + (b |^ (n + 1))) - (a * (b |^ n))) - (b * (a |^ n))) + ((a * (b |^ n)) + (b * (a |^ n))) > 0 + ((a * (b |^ n)) + (b * (a |^ n))) by XREAL_1:8; hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) ; ::_thesis: verum end; supposeA3: a - b = 0 ; ::_thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) then ((a |^ n) * b) + (a * (b |^ n)) = (a |^ (n + 1)) + ((a |^ n) * a) by NEWTON:6 .= (a |^ (n + 1)) + (a |^ (n + 1)) by NEWTON:6 .= 2 * (a |^ (n + 1)) ; hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) by A3; ::_thesis: verum end; supposeA4: a - b < 0 ; ::_thesis: (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) then (a - b) + b < 0 + b by XREAL_1:8; then a |^ n < b |^ n by A1, PREPOWER:10; then (a |^ n) - (b |^ n) < 0 by XREAL_1:49; then (a - b) * ((a |^ n) - (b |^ n)) > 0 by A4; then (((a * (a |^ n)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 ; then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b * (b |^ n)) > 0 by NEWTON:6; then (((a |^ (n + 1)) - (a * (b |^ n))) - (b * (a |^ n))) + (b |^ (n + 1)) > 0 by NEWTON:6; then ((((a |^ (n + 1)) + (b |^ (n + 1))) - (a * (b |^ n))) - (b * (a |^ n))) + ((a * (b |^ n)) + (b * (a |^ n))) > 0 + ((a * (b |^ n)) + (b * (a |^ n))) by XREAL_1:8; hence (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n)) ; ::_thesis: verum end; end; end; theorem :: SERIES_5:44 for a, b, c being real positive number for n being Element of NAT st (a ^2) + (b ^2) = c ^2 & n >= 3 holds (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) proof let a, b, c be real positive number ; ::_thesis: for n being Element of NAT st (a ^2) + (b ^2) = c ^2 & n >= 3 holds (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) let n be Element of NAT ; ::_thesis: ( (a ^2) + (b ^2) = c ^2 & n >= 3 implies (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) ) assume that A1: (a ^2) + (b ^2) = c ^2 and A2: n >= 3 ; ::_thesis: (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) A3: n >= 1 by A2, XXREAL_0:2; b ^2 > 0 ; then A4: b |^ 2 > 0 by NEWTON:81; ((c ^2) - (b ^2)) + (b ^2) > 0 + (b ^2) by A1, XREAL_1:8; then sqrt (c ^2) > sqrt (b ^2) by SQUARE_1:27; then c > sqrt (b ^2) by SQUARE_1:22; then c > b by SQUARE_1:22; then c |^ n > b |^ n by A3, PREPOWER:10; then (c |^ n) * (b |^ 2) > (b |^ n) * (b |^ 2) by A4, XREAL_1:68; then A5: (c |^ n) * (b |^ 2) > b |^ (n + 2) by NEWTON:8; a ^2 > 0 ; then A6: a |^ 2 > 0 by NEWTON:81; ((c ^2) - (a ^2)) + (a ^2) > 0 + (a ^2) by A1, XREAL_1:8; then sqrt (c ^2) > sqrt (a ^2) by SQUARE_1:27; then c > sqrt (a ^2) by SQUARE_1:22; then c > a by SQUARE_1:22; then c |^ n > a |^ n by A3, PREPOWER:10; then (c |^ n) * (a |^ 2) > (a |^ n) * (a |^ 2) by A6, XREAL_1:68; then (c |^ n) * (a |^ 2) > a |^ (n + 2) by NEWTON:8; then ((c |^ n) * (a |^ 2)) + ((c |^ n) * (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) by A5, XREAL_1:8; then (c |^ n) * ((a |^ 2) + (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) ; then (c |^ n) * ((a ^2) + (b |^ 2)) > (a |^ (n + 2)) + (b |^ (n + 2)) by NEWTON:81; then (c |^ n) * (c ^2) > (a |^ (n + 2)) + (b |^ (n + 2)) by A1, NEWTON:81; then (c |^ n) * (c |^ 2) > (a |^ (n + 2)) + (b |^ (n + 2)) by NEWTON:81; hence (a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2) by NEWTON:8; ::_thesis: verum end; theorem :: SERIES_5:45 for n being Element of NAT st n >= 1 holds (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) ) assume A1: n >= 1 ; ::_thesis: (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) n + 1 > n + 0 by XREAL_1:8; then 1 / (n + 1) < 1 / n by A1, XREAL_1:76; then (1 / (n + 1)) + 1 < (1 / n) + 1 by XREAL_1:8; then A2: (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ n by A1, PREPOWER:10; A3: (1 + (1 / n)) |^ n > 0 by PREPOWER:6; ((1 + (1 / n)) |^ (n + 1)) - ((1 + (1 / n)) |^ n) = (((1 + (1 / n)) |^ n) * (1 + (1 / n))) - ((1 + (1 / n)) |^ n) by NEWTON:6 .= ((1 + (1 / n)) |^ n) * (1 / n) ; then (((1 + (1 / n)) |^ (n + 1)) - ((1 + (1 / n)) |^ n)) + ((1 + (1 / n)) |^ n) > 0 + ((1 + (1 / n)) |^ n) by A1, A3, XREAL_1:8; hence (1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1) by A2, XXREAL_0:2; ::_thesis: verum end; theorem :: SERIES_5:46 for a, b being real positive number for n, k being Element of NAT st n >= 1 & k >= 1 holds ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) proof let a, b be real positive number ; ::_thesis: for n, k being Element of NAT st n >= 1 & k >= 1 holds ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) let n, k be Element of NAT ; ::_thesis: ( n >= 1 & k >= 1 implies ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) ) assume that A1: n >= 1 and A2: k >= 1 ; ::_thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) A3: (((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n))) - (2 * ((a |^ (k + n)) + (b |^ (k + n)))) = ((((((a |^ k) * (a |^ n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + ((b |^ k) * (b |^ n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) .= (((((a |^ (k + n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + ((b |^ k) * (b |^ n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) by NEWTON:8 .= (((((a |^ (k + n)) + ((a |^ k) * (b |^ n))) + ((b |^ k) * (a |^ n))) + (b |^ (k + n))) - (2 * (a |^ (k + n)))) - (2 * (b |^ (k + n))) by NEWTON:8 .= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - (a |^ (k + n))) - (b |^ (k + n)) .= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - ((a |^ k) * (a |^ n))) - (b |^ (k + n)) by NEWTON:8 .= ((((a |^ k) * (b |^ n)) + ((b |^ k) * (a |^ n))) - ((a |^ k) * (a |^ n))) - ((b |^ k) * (b |^ n)) by NEWTON:8 .= ((a |^ n) - (b |^ n)) * ((b |^ k) - (a |^ k)) ; percases ( a - b > 0 or a - b = 0 or a - b < 0 ) ; suppose a - b > 0 ; ::_thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) then A4: (a - b) + b > 0 + b by XREAL_1:8; then a |^ k > b |^ k by A2, PREPOWER:10; then A5: (b |^ k) - (a |^ k) < 0 by XREAL_1:49; a |^ n > b |^ n by A1, A4, PREPOWER:10; then (a |^ n) - (b |^ n) > 0 by XREAL_1:50; hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3, A5, XREAL_1:48; ::_thesis: verum end; suppose a - b = 0 ; ::_thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) then a |^ n = b |^ n ; hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3; ::_thesis: verum end; suppose a - b < 0 ; ::_thesis: ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) then A6: (a - b) + b < 0 + b by XREAL_1:8; then a |^ k < b |^ k by A2, PREPOWER:10; then A7: (b |^ k) - (a |^ k) > 0 by XREAL_1:50; a |^ n < b |^ n by A1, A6, PREPOWER:10; then (a |^ n) - (b |^ n) < 0 by XREAL_1:49; hence ((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n))) by A3, A7, XREAL_1:48; ::_thesis: verum end; end; end; theorem :: SERIES_5:47 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / (sqrt (n + 1)) ) holds for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / (sqrt (n + 1)) ) implies for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 < 2 * (sqrt ($1 + 1)); assume A1: for n being Element of NAT holds s . n = 1 / (sqrt (n + 1)) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (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: sqrt (n + 2) > 0 by SQUARE_1:25; ((4 * (n ^2)) + (12 * n)) + 8 < ((4 * (n ^2)) + (12 * n)) + 9 by XREAL_1:8; then sqrt (4 * ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2) by SQUARE_1:27; then 2 * (sqrt ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2) by SQUARE_1:20, SQUARE_1:29; then 2 * (sqrt ((n + 2) * (n + 1))) < (2 * n) + 3 by SQUARE_1:22; then (2 * (sqrt ((n + 2) * (n + 1)))) + 1 < ((2 * n) + 3) + 1 by XREAL_1:8; then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (n + 2) by SQUARE_1:29; then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (sqrt ((n + 2) ^2)) by SQUARE_1:22; then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < (2 * (sqrt ((n + 2) * (n + 2)))) / (sqrt (n + 2)) by A3, XREAL_1:74; then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < (2 * ((sqrt (n + 2)) * (sqrt (n + 2)))) / (sqrt (n + 2)) by SQUARE_1:29; then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < ((2 * (sqrt (n + 2))) * (sqrt (n + 2))) / (sqrt (n + 2)) ; then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < 2 * (sqrt (n + 2)) by A3, XCMPLX_1:89; then (((2 * (sqrt (n + 1))) * (sqrt (n + 2))) / (sqrt (n + 2))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by XCMPLX_1:62; then A4: (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by A3, XCMPLX_1:89; assume (Partial_Sums s) . n < 2 * (sqrt (n + 1)) ; ::_thesis: S1[n + 1] then ((Partial_Sums s) . n) + (1 / (sqrt (n + 2))) < (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) by XREAL_1:8; then ((Partial_Sums s) . n) + (1 / (sqrt ((n + 1) + 1))) < 2 * (sqrt (n + 2)) by A4, XXREAL_0:2; then ((Partial_Sums s) . n) + (s . (n + 1)) < 2 * (sqrt (n + 2)) by A1; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / (sqrt (0 + 1)) by A1 .= 1 by SQUARE_1:18 ; then A5: S1[ 0 ] by SQUARE_1:18; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); hence for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) ; ::_thesis: verum end; theorem Th48: :: SERIES_5:48 for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ) holds for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ) implies for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ) defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 <= 2 - (1 / ($1 + 1)); assume A1: for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; ::_thesis: S1[n + 1] then A3: ((Partial_Sums s) . n) + (1 / ((n + 2) ^2)) <= (2 - (1 / (n + 1))) + (1 / ((n + 2) ^2)) by XREAL_1:7; ((n ^2) + (3 * n)) + 3 > ((n ^2) + (3 * n)) + 2 by XREAL_1:8; then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > ((n + 2) * (n + 1)) / (((n + 2) ^2) * (n + 1)) by XREAL_1:74; then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > (n + 2) / ((n + 2) * (n + 2)) by XCMPLX_1:91; then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > ((n + 2) / (n + 2)) / (n + 2) by XCMPLX_1:78; then (((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)) > 1 / (n + 2) by XCMPLX_1:60; then (- 1) * ((((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2))) < (- 1) * (1 / (n + 2)) by XREAL_1:69; then A4: (- ((((n ^2) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2)))) + 2 < (- (1 / (n + 2))) + 2 by XREAL_1:8; (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1 .= ((Partial_Sums s) . n) + (1 / (((n + 1) + 1) ^2)) by A1 ; then (Partial_Sums s) . (n + 1) <= 2 - ((1 / (n + 1)) - (1 / ((n + 2) ^2))) by A3; then (Partial_Sums s) . (n + 1) <= 2 - (((1 * ((n + 2) ^2)) - (1 * (n + 1))) / ((n + 1) * ((n + 2) ^2))) by XCMPLX_1:130; hence S1[n + 1] by A4, XXREAL_0:2; ::_thesis: verum end; (Partial_Sums s) . 0 = s . 0 by SERIES_1:def_1 .= 1 / ((0 + 1) ^2) by A1 .= 1 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); hence for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; ::_thesis: verum end; theorem :: SERIES_5:49 for n being Element of NAT for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ) holds (Partial_Sums s) . n < 2 proof let n be Element of NAT ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ) holds (Partial_Sums s) . n < 2 let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ) implies (Partial_Sums s) . n < 2 ) assume for n being Element of NAT holds s . n = 1 / ((n + 1) ^2) ; ::_thesis: (Partial_Sums s) . n < 2 then A1: (Partial_Sums s) . n <= 2 - (1 / (n + 1)) by Th48; (- (1 / (n + 1))) + 2 < 0 + 2 by XREAL_1:8; hence (Partial_Sums s) . n < 2 by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th50: :: SERIES_5:50 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_Sums s) . n < 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_Sums s) . n < n + 1 ) defpred S1[ Element of NAT ] means (Partial_Sums s) . $1 < $1 + 1; assume A1: for n being Element of NAT holds s . n < 1 ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n < n + 1 A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def_1; assume (Partial_Sums s) . n < n + 1 ; ::_thesis: S1[n + 1] hence S1[n + 1] by A1, A3, XREAL_1:8; ::_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 < n + 1 ; ::_thesis: verum end; theorem :: SERIES_5:51 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 >= ((Partial_Sums s) . n) - n 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 >= ((Partial_Sums s) . n) - n ) defpred S1[ Element of NAT ] means (Partial_Product s) . $1 >= ((Partial_Sums 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 >= ((Partial_Sums s) . n) - 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 A3: (Partial_Product s) . n >= ((Partial_Sums s) . n) - n ; ::_thesis: S1[n + 1] A4: s . (n + 1) < 1 by A1; ((Partial_Sums s) . n) - (n + 1) < 0 by A1, Th50, XREAL_1:49; then (s . (n + 1)) * ((((Partial_Sums s) . n) - n) - 1) > 1 * ((((Partial_Sums s) . n) - n) - 1) by A4, XREAL_1:69; then A5: ((((s . (n + 1)) * ((Partial_Sums s) . n)) - ((s . (n + 1)) * n)) - (s . (n + 1))) + (s . (n + 1)) > ((((Partial_Sums s) . n) - n) - 1) + (s . (n + 1)) by XREAL_1:8; s . (n + 1) > 0 by A1; then ((Partial_Product s) . n) * (s . (n + 1)) >= (((Partial_Sums s) . n) - n) * (s . (n + 1)) by A3, XREAL_1:64; then ((Partial_Product s) . n) * (s . (n + 1)) > (((Partial_Sums s) . n) + (s . (n + 1))) - (n + 1) by A5, XXREAL_0:2; then (Partial_Product s) . (n + 1) > (((Partial_Sums s) . n) + (s . (n + 1))) - (n + 1) by SERIES_3:def_1; hence S1[n + 1] by SERIES_1:def_1; ::_thesis: verum end; ((Partial_Sums s) . 0) - 0 = s . 0 by SERIES_1:def_1; then A6: S1[ 0 ] by SERIES_3:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); hence for n being Element of NAT holds (Partial_Product s) . n >= ((Partial_Sums s) . n) - n ; ::_thesis: verum end; theorem Th52: :: SERIES_5:52 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ) holds for n being Element of NAT holds (Partial_Sums s1) . n > 0 proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ) implies for n being Element of NAT holds (Partial_Sums s1) . n > 0 ) defpred S1[ Element of NAT ] means (Partial_Sums s1) . $1 > 0 ; assume A1: for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s1) . n > 0 then A2: s1 . 0 = 1 / (s . 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 s1) . n > 0 ; ::_thesis: S1[n + 1] A5: (Partial_Sums s1) . (n + 1) = ((Partial_Sums s1) . n) + (s1 . (n + 1)) by SERIES_1:def_1; A6: s . (n + 1) > 0 by A1; s1 . (n + 1) = 1 / (s . (n + 1)) by A1; hence S1[n + 1] by A4, A5, A6; ::_thesis: verum end; s . 0 > 0 by A1; then A7: S1[ 0 ] by A2, SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A3); hence for n being Element of NAT holds (Partial_Sums s1) . n > 0 ; ::_thesis: verum end; theorem :: SERIES_5:53 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ) holds for n being Element of NAT holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ) implies for n being Element of NAT holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 ) defpred S1[ Element of NAT ] means ((Partial_Sums s) . $1) * ((Partial_Sums s1) . $1) >= ($1 + 1) ^2 ; assume A1: for n being Element of NAT holds ( s . n > 0 & s1 . n = 1 / (s . n) ) ; ::_thesis: for n being Element of NAT holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 then A2: s . 0 > 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] ) set x = (Partial_Sums s) . n; set y = (Partial_Sums s1) . n; assume A4: ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 ; ::_thesis: S1[n + 1] then A5: (((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + 1) >= ((n + 1) ^2) + (((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + 1) by XREAL_1:7; sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) >= sqrt ((n + 1) ^2) by A4, SQUARE_1:26; then sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) >= n + 1 by SQUARE_1:22; then A6: 2 * (sqrt (((Partial_Sums s) . n) * ((Partial_Sums s1) . n))) >= 2 * (n + 1) by XREAL_1:64; A7: s . (n + 1) > 0 by A1; A8: (Partial_Sums s) . n > 0 by A1, SERIES_3:33; (Partial_Sums s1) . n > 0 by A1, Th52; then (((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2 * (sqrt ((((Partial_Sums s1) . n) * (s . (n + 1))) * (((Partial_Sums s) . n) / (s . (n + 1))))) by A7, A8, SIN_COS2:1; then (((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2 * (sqrt (((Partial_Sums s) . n) / ((1 * (s . (n + 1))) / (((Partial_Sums s1) . n) * (s . (n + 1)))))) by XCMPLX_1:81; then (((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2 * (sqrt (((Partial_Sums s) . n) / (1 / ((Partial_Sums s1) . n)))) by A7, XCMPLX_1:91; then (((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= 2 * (sqrt (((Partial_Sums s1) . n) * (((Partial_Sums s) . n) / 1))) by XCMPLX_1:81; then (((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1))) >= (2 * n) + 2 by A6, XXREAL_0:2; then A9: ((((Partial_Sums s) . n) / (s . (n + 1))) + (((Partial_Sums s1) . n) * (s . (n + 1)))) + (((n ^2) + (2 * n)) + 2) >= ((2 * n) + 2) + (((n ^2) + (2 * n)) + 2) by XREAL_1:7; ((Partial_Sums s) . (n + 1)) * ((Partial_Sums s1) . (n + 1)) = (((Partial_Sums s) . n) + (s . (n + 1))) * ((Partial_Sums s1) . (n + 1)) by SERIES_1:def_1 .= (((Partial_Sums s) . n) + (s . (n + 1))) * (((Partial_Sums s1) . n) + (s1 . (n + 1))) by SERIES_1:def_1 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (s1 . (n + 1)))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (s1 . (n + 1))) .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (s1 . (n + 1))) by A1 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + ((s . (n + 1)) * (1 / (s . (n + 1)))) by A1 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + (((s . (n + 1)) * 1) / (s . (n + 1))) by XCMPLX_1:74 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) * (1 / (s . (n + 1))))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1 by A7, XCMPLX_1:60 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) / ((s . (n + 1)) / 1))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1 by XCMPLX_1:79 .= (((((Partial_Sums s) . n) * ((Partial_Sums s1) . n)) + (((Partial_Sums s) . n) / (s . (n + 1)))) + ((s . (n + 1)) * ((Partial_Sums s1) . n))) + 1 ; hence S1[n + 1] by A9, A5, XXREAL_0:2; ::_thesis: verum end; ((Partial_Sums s) . 0) * ((Partial_Sums s1) . 0) = (s . 0) * ((Partial_Sums s1) . 0) by SERIES_1:def_1 .= (s . 0) * (s1 . 0) by SERIES_1:def_1 .= (s . 0) * (1 / (s . 0)) by A1 .= (s . 0) / ((s . 0) / 1) by XCMPLX_1:79 .= 1 by A2, XCMPLX_1:60 ; then A10: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A3); hence for n being Element of NAT holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2 ; ::_thesis: verum end; theorem :: SERIES_5:54 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) ) defpred S1[ Nat] means (Partial_Sums s) . $1 < ((1 / 6) * ((4 * $1) + 3)) * (sqrt $1); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A3: n >= 1 and A4: (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) ; ::_thesis: S1[n + 1] n + 1 >= 1 + 1 by A3, XREAL_1:7; then n + 1 >= 1 by XXREAL_0:2; then A5: s . (n + 1) = sqrt (n + 1) by A1; 0 + ((16 * (n ^2)) + (8 * n)) < 1 + ((16 * (n ^2)) + (8 * n)) by XREAL_1:8; then ((16 * n) + 8) * n < 1 * (((16 * (n ^2)) + (8 * n)) + 1) ; then ((4 * ((4 * n) + 1)) + 4) / (((4 * n) + 1) ^2) < 1 / n by A3, XREAL_1:106; then ((4 * ((4 * n) + 1)) / (((4 * n) + 1) * ((4 * n) + 1))) + (4 / (((4 * n) + 1) ^2)) < 1 / n by XCMPLX_1:62; then (4 / ((4 * n) + 1)) + (4 / (((4 * n) + 1) ^2)) < 1 / n by XCMPLX_1:91; then 1 + ((4 / ((4 * n) + 1)) + (4 / (((4 * n) + 1) ^2))) < 1 + (1 / n) by XREAL_1:8; then (1 + (4 / ((4 * n) + 1))) + (4 / (((4 * n) + 1) ^2)) < 1 + (1 / n) ; then (1 + ((2 * 2) / ((4 * n) + 1))) + ((2 / ((4 * n) + 1)) ^2) < 1 + (1 / n) by XCMPLX_1:76; then (1 + (2 * (2 / ((4 * n) + 1)))) + ((2 / ((4 * n) + 1)) ^2) < 1 + (1 / n) by XCMPLX_1:74; then ((2 / ((4 * n) + 1)) + 1) ^2 < (1 + (n * 1)) / n by A3, XCMPLX_1:113; then sqrt (((2 / ((4 * n) + 1)) + 1) ^2) < sqrt ((1 + n) / n) by SQUARE_1:27; then (2 / ((4 * n) + 1)) + 1 < sqrt ((1 + n) / n) by SQUARE_1:22; then (2 + (((4 * n) + 1) * 1)) / ((4 * n) + 1) < sqrt ((1 + n) / n) by XCMPLX_1:113; then A6: ((4 * n) + 3) / ((4 * n) + 1) < (sqrt (1 + n)) / (sqrt n) by SQUARE_1:30; sqrt n > 0 by A3, SQUARE_1:25; then (1 / 6) * (((4 * n) + 3) * (sqrt n)) < (1 / 6) * ((sqrt (1 + n)) * ((4 * n) + 1)) by A6, XREAL_1:68, XREAL_1:102; then (Partial_Sums s) . n < (((1 / 6) * (sqrt (1 + n))) * ((4 * n) + 7)) - (sqrt (1 + n)) by A4, XXREAL_0:2; then A7: ((Partial_Sums s) . n) + (sqrt (1 + n)) < ((((1 / 6) * (sqrt (1 + n))) * ((4 * n) + 7)) - (sqrt (1 + n))) + (sqrt (1 + n)) by XREAL_1:8; n in NAT by ORDINAL1:def_12; hence S1[n + 1] by A5, A7, SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= 0 + (s . 1) by A1 .= 1 by A1, SQUARE_1:18 ; then A8: S1[1] by SQUARE_1:18; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A8, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n) ; ::_thesis: verum end; theorem :: SERIES_5:55 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) ) defpred S1[ Nat] means (Partial_Sums s) . $1 > ((2 / 3) * $1) * (sqrt $1); assume A1: for n being Element of NAT st n >= 1 holds ( s . n = sqrt n & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A3: n >= 1 and A4: (Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) ; ::_thesis: S1[n + 1] 2 * n >= 2 * 1 by A3, XREAL_1:64; then 2 * n > 1 by XXREAL_0:2; then A5: (2 * n) - 1 > 0 by XREAL_1:50; 3 * n >= 3 * 1 by A3, XREAL_1:64; then 3 * n > 1 by XXREAL_0:2; then 1 - (3 * n) < 0 by XREAL_1:49; then ((1 + (n - (4 * n))) + ((4 * (n ^2)) - (4 * (n ^2)))) + (4 * (n |^ 3)) < 0 + (4 * (n |^ 3)) by XREAL_1:8; then (((4 * (n |^ (2 + 1))) - (4 * (n ^2))) + n) + (((4 * (n ^2)) - (4 * n)) + 1) < 4 * (n |^ 3) ; then (((4 * ((n |^ 2) * n)) - (4 * (n * n))) + n) + (((4 * (n ^2)) - (4 * n)) + 1) < 4 * (n |^ 3) by NEWTON:6; then ((((4 * (n |^ 2)) - (4 * n)) + 1) * n) + ((((4 * (n ^2)) - (4 * n)) + 1) * 1) < 4 * (n |^ 3) ; then ((((4 * (n ^2)) - (4 * n)) + 1) * n) + ((((4 * (n ^2)) - (4 * n)) + 1) * 1) < 4 * (n |^ 3) by NEWTON:81; then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < 4 * (n |^ (2 + 1)) ; then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < 4 * ((n |^ 2) * n) by NEWTON:6; then (((4 * (n ^2)) - (4 * n)) + 1) * (n + 1) < (4 * (n |^ 2)) * n ; then (((2 * n) - 1) ^2) * (n + 1) < (4 * (n ^2)) * n by NEWTON:81; then (n + 1) / n < ((2 * n) ^2) / (((2 * n) - 1) ^2) by A3, A5, XREAL_1:106; then (n + 1) / n < ((2 * n) / ((2 * n) - 1)) ^2 by XCMPLX_1:76; then sqrt ((n + 1) / n) < sqrt (((2 * n) / ((2 * n) - 1)) ^2) by SQUARE_1:27; then sqrt ((n + 1) / n) < (2 * n) / ((2 * n) - 1) by A5, SQUARE_1:22; then A6: (sqrt (n + 1)) / (sqrt n) < (2 * n) / ((2 * n) - 1) by SQUARE_1:30; sqrt n > 0 by A3, SQUARE_1:25; then (1 / 3) * ((sqrt (n + 1)) * ((2 * n) - 1)) < (1 / 3) * ((2 * n) * (sqrt n)) by A5, A6, XREAL_1:68, XREAL_1:102; then (Partial_Sums s) . n > (((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1)) by A4, XXREAL_0:2; then A7: ((Partial_Sums s) . n) + (sqrt (n + 1)) > ((((2 / 3) * (n + 1)) * (sqrt (n + 1))) - (sqrt (n + 1))) + (sqrt (n + 1)) by XREAL_1:8; A8: n in NAT by ORDINAL1:def_12; n + 1 >= 1 + 1 by A3, XREAL_1:7; then n + 1 >= 1 by XXREAL_0:2; then ((Partial_Sums s) . n) + (s . (n + 1)) > ((2 / 3) * (n + 1)) * (sqrt (n + 1)) by A1, A7; hence S1[n + 1] by A8, SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums s) . (1 + 0) = ((Partial_Sums s) . 0) + (s . (1 + 0)) by SERIES_1:def_1 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= 0 + (s . 1) by A1 .= 1 by A1, SQUARE_1:18 ; then A9: S1[1] by SQUARE_1:18; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A9, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n) ; ::_thesis: verum end; theorem :: SERIES_5:56 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ) defpred S1[ Nat] means (Partial_Product s) . $1 > (1 / 2) * (sqrt ((2 * $1) + 3)); A1: (1 / 2) * (sqrt ((2 * 1) + 3)) = (sqrt 5) / 2 ; assume A2: for n being Element of NAT st n >= 1 holds ( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) A3: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A4: n >= 1 and A5: (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ; ::_thesis: S1[n + 1] n + 1 >= 1 + 1 by A4, XREAL_1:7; then A6: n + 1 >= 1 by XXREAL_0:2; A7: n in NAT by ORDINAL1:def_12; A8: sqrt ((2 * n) + 3) > 0 by SQUARE_1:25; (1 / ((2 * n) + 3)) + ((2 * n) + 5) > 0 + ((2 * n) + 5) by XREAL_1:8; then ((1 / ((2 * n) + 3)) + 2) + ((2 * n) + 3) > (2 * n) + 5 ; then (((1 ^2) / ((sqrt ((2 * n) + 3)) ^2)) + 2) + ((2 * n) + 3) > (2 * n) + 5 by SQUARE_1:def_2; then (((1 / (sqrt ((2 * n) + 3))) ^2) + 2) + ((2 * n) + 3) > (2 * n) + 5 by XCMPLX_1:76; then (((1 / (sqrt ((2 * n) + 3))) ^2) + (2 * 1)) + ((sqrt ((2 * n) + 3)) ^2) > (2 * n) + 5 by SQUARE_1:def_2; then (((1 / (sqrt ((2 * n) + 3))) ^2) + (2 * ((sqrt ((2 * n) + 3)) * (1 / (sqrt ((2 * n) + 3)))))) + ((sqrt ((2 * n) + 3)) ^2) > (2 * n) + 5 by A8, XCMPLX_1:106; then sqrt (((1 / (sqrt ((2 * n) + 3))) + (sqrt ((2 * n) + 3))) ^2) > sqrt ((2 * n) + 5) by SQUARE_1:27; then (sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3))) > sqrt ((2 * n) + 5) by A8, SQUARE_1:22; then A9: (1 / 2) * ((sqrt ((2 * n) + 3)) + (1 / (sqrt ((2 * n) + 3)))) > (1 / 2) * (sqrt ((2 * n) + 5)) by XREAL_1:68; ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) * (1 + (1 / ((2 * n) + 3))) by A5, XREAL_1:68; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > (((1 / 2) * (sqrt ((2 * n) + 3))) * 1) + (((1 / 2) * (sqrt ((2 * n) + 3))) * (1 / ((2 * n) + 3))) ; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + (((1 / 2) * (sqrt ((2 * n) + 3))) / ((2 * n) + 3)) by XCMPLX_1:74; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * ((sqrt ((2 * n) + 3)) / ((2 * n) + 3))) by XCMPLX_1:74; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * ((sqrt ((2 * n) + 3)) / (sqrt (((2 * n) + 3) ^2)))) by SQUARE_1:22; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (((sqrt ((2 * n) + 3)) * 1) / ((sqrt ((2 * n) + 3)) * (sqrt ((2 * n) + 3))))) by SQUARE_1:29; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (((sqrt ((2 * n) + 3)) / (sqrt ((2 * n) + 3))) * (1 / (sqrt ((2 * n) + 3))))) by XCMPLX_1:76; then ((Partial_Product s) . n) * (1 + (1 / ((2 * n) + 3))) > ((1 / 2) * (sqrt ((2 * n) + 3))) + ((1 / 2) * (1 * (1 / (sqrt ((2 * n) + 3))))) by A8, XCMPLX_1:60; then ((Partial_Product s) . n) * (1 + (1 / ((2 * (n + 1)) + 1))) > (1 / 2) * (sqrt ((2 * n) + 5)) by A9, XXREAL_0:2; then ((Partial_Product s) . n) * (s . (n + 1)) > (1 / 2) * (sqrt ((2 * n) + 5)) by A2, A6; hence S1[n + 1] by A7, SERIES_3:def_1; ::_thesis: verum end; sqrt (16 / 9) > sqrt (5 / 4) by SQUARE_1:27; then (sqrt (4 ^2)) / (sqrt (3 ^2)) > sqrt (5 / 4) by SQUARE_1:30; then 4 / (sqrt (3 ^2)) > sqrt (5 / 4) by SQUARE_1:22; then 4 / 3 > sqrt (5 / 4) by SQUARE_1:22; then A10: 4 / 3 > (sqrt 5) / (sqrt (2 ^2)) by SQUARE_1:30; (Partial_Product s) . (1 + 0) = ((Partial_Product s) . 0) * (s . (1 + 0)) by SERIES_3:def_1 .= (s . 0) * (s . 1) by SERIES_3:def_1 .= 1 * (s . 1) by A2 .= 1 + (1 / ((2 * 1) + 1)) by A2 .= 4 / 3 ; then A11: S1[1] by A1, A10, SQUARE_1:22; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A11, A3); hence for n being Element of NAT st n >= 1 holds (Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3)) ; ::_thesis: verum end; theorem :: SERIES_5:57 for s being Real_Sequence st ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt (n * (n + 1)) & s . 0 = 0 ) ) holds for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > (n * (n + 1)) / 2 proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT st n >= 1 holds ( s . n = sqrt (n * (n + 1)) & s . 0 = 0 ) ) implies for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > (n * (n + 1)) / 2 ) defpred S1[ Nat] means (Partial_Sums s) . $1 > ($1 * ($1 + 1)) / 2; assume A1: for n being Element of NAT st n >= 1 holds ( s . n = sqrt (n * (n + 1)) & s . 0 = 0 ) ; ::_thesis: for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > (n * (n + 1)) / 2 A2: for n being Nat st n >= 1 & S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] ) assume that A3: n >= 1 and A4: (Partial_Sums s) . n > (n * (n + 1)) / 2 ; ::_thesis: S1[n + 1] n + 1 >= 1 + 1 by A3, XREAL_1:7; then n + 1 >= 1 by XXREAL_0:2; then A5: s . (n + 1) = sqrt ((n + 1) * ((n + 1) + 1)) by A1; n + 2 > n + 1 by XREAL_1:8; then (n + 2) * (n + 1) > (n + 1) ^2 by XREAL_1:68; then sqrt ((n + 2) * (n + 1)) > sqrt ((n + 1) ^2) by SQUARE_1:27; then A6: sqrt ((n + 2) * (n + 1)) > n + 1 by SQUARE_1:22; ((Partial_Sums s) . n) + ((sqrt ((n + 1) * (n + 2))) - (((n + 1) * (n + 2)) / 2)) > ((n * (n + 1)) / 2) + ((sqrt ((n + 1) * (n + 2))) - (((n + 1) * (n + 2)) / 2)) by A4, XREAL_1:8; then (((Partial_Sums s) . n) + (sqrt ((n + 1) * (n + 2)))) - (((n + 1) * (n + 2)) / 2) > (sqrt ((n + 1) * (n + 2))) - (n + 1) ; then (((Partial_Sums s) . n) + (sqrt ((n + 1) * (n + 2)))) - (((n + 1) * (n + 2)) / 2) > 0 by A6, XREAL_1:50; then A7: ((((Partial_Sums s) . n) + (sqrt ((n + 1) * (n + 2)))) - (((n + 1) * (n + 2)) / 2)) + (((n + 1) * (n + 2)) / 2) > 0 + (((n + 1) * (n + 2)) / 2) by XREAL_1:8; n in NAT by ORDINAL1:def_12; hence S1[n + 1] by A5, A7, SERIES_1:def_1; ::_thesis: verum end; A8: (Partial_Sums s) . 1 = (Partial_Sums s) . (0 + 1) .= ((Partial_Sums s) . 0) + (s . 1) by SERIES_1:def_1 .= (s . 0) + (s . 1) by SERIES_1:def_1 .= 0 + (s . 1) by A1 .= sqrt (1 * (1 + 1)) by A1 .= sqrt 2 ; then ((Partial_Sums s) . 1) ^2 = 2 by SQUARE_1:def_2; then sqrt (((Partial_Sums s) . 1) ^2) > sqrt (((1 * (1 + 1)) / 2) ^2) by SQUARE_1:27; then A9: sqrt (((Partial_Sums s) . 1) ^2) > (1 * (1 + 1)) / 2 by SQUARE_1:22; (Partial_Sums s) . 1 > 0 by A8, SQUARE_1:25; then A10: S1[1] by A9, SQUARE_1:22; for n being Nat st n >= 1 holds S1[n] from NAT_1:sch_8(A10, A2); hence for n being Element of NAT st n >= 1 holds (Partial_Sums s) . n > (n * (n + 1)) / 2 ; ::_thesis: verum end;