:: On the Partial Product and Partial Sum of Series and Related Basic Inequalities
:: by Fuguo Ge and Xiquan Liang
::
:: Received November 23, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


Lm1: for x, y being Real holds (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2) + (x * y)) + (y ^2))
proof end;

Lm2: for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b)
proof end;

Lm3: for x, y, z being Real holds ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z)
proof end;

Lm4: for a, c being positive Real
for b being Real holds (a / c) to_power (- b) = (c / a) to_power b
proof end;

Lm5: for a, b, c, d being positive Real holds (((sqrt (a * b)) ^2) + ((sqrt (c * d)) ^2)) * (((sqrt (a * c)) ^2) + ((sqrt (b * d)) ^2)) >= (b * c) * ((a + d) ^2)
proof end;

Lm6: for x, y, z being Real 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 st |.x.| < 1 holds
x ^2 < 1
proof end;

Lm8: for x being Real st x ^2 < 1 holds
|.x.| < 1
proof end;

Lm9: for a, b, c being positive Real 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 end;

Lm10: for a, b being positive Real holds sqrt (((a ^2) + (a * b)) + (b ^2)) = (1 / 2) * (sqrt ((4 * ((a ^2) + (b ^2))) + ((4 * a) * b)))
proof end;

Lm11: for a, b being positive Real holds sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b)
proof end;

Lm12: for a, b being positive Real holds sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2)
proof end;

Lm13: for a, b, c being positive Real holds (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2)
proof end;

Lm14: for a, b, c being positive Real holds ((b * c) / a) * ((c * a) / b) = c ^2
proof end;

Lm15: for a, b, c being positive Real 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 end;

Lm16: for a, b, c being positive Real 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 end;

Lm17: for a, b, c being positive Real st (a + b) + c = 1 holds
(1 / a) - 1 = (b + c) / a
proof end;

Lm18: for a, b, c being positive Real holds (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = 8
proof end;

Lm19: for a, b, c being positive Real st (a + b) + c = 1 holds
1 + (1 / a) = 2 + ((b + c) / a)
proof end;

Lm20: for a, b, c being positive Real holds (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c)))
proof end;

Lm21: for a, b, c being positive Real holds (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (b / (sqrt (a * c))) + 1
proof end;

Lm22: for a, b, c being positive Real 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 end;

Lm23: for a, b, c being positive Real 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 end;

theorem :: SERIES_5:1
for a, b being positive Real holds (a + b) * ((1 / a) + (1 / b)) >= 4
proof end;

theorem :: SERIES_5:2
for a, b being positive Real holds (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3))
proof end;

theorem Th3: :: SERIES_5:3
for a, b, c being positive Real st a < b holds
1 < (b + c) / (a + c)
proof end;

theorem Th4: :: SERIES_5:4
for a, b being positive Real st a < b holds
a / b < sqrt (a / b)
proof end;

theorem Th5: :: SERIES_5:5
for a, b being positive Real st a < b holds
sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))
proof end;

theorem :: SERIES_5:6
for a, b being positive Real st a < b holds
a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))
proof end;

theorem Th7: :: SERIES_5:7
for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) <= sqrt (a * b)
proof end;

theorem Th8: :: SERIES_5:8
for a, b being positive Real holds (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2)
proof end;

theorem :: SERIES_5:9
for x, y being Real holds x + y <= sqrt (2 * ((x ^2) + (y ^2)))
proof end;

theorem Th10: :: SERIES_5:10
for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) <= (a + b) / 2
proof end;

theorem :: SERIES_5:11
for a, b being positive Real holds sqrt (a * b) <= sqrt (((a ^2) + (b ^2)) / 2)
proof end;

theorem :: SERIES_5:12
for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) <= sqrt (((a ^2) + (b ^2)) / 2)
proof end;

theorem :: SERIES_5:13
for x, y being Real st |.x.| < 1 & |.y.| < 1 holds
|.((x + y) / (1 + (x * y))).| <= 1
proof end;

theorem :: SERIES_5:14
for x, y being Real holds |.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))
proof end;

theorem :: SERIES_5:15
for a, b, c, d being positive Real holds (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) > 1
proof end;

theorem :: SERIES_5:16
for a, b, c, d being positive Real holds (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2
proof end;

theorem :: SERIES_5:17
for a, b, c being positive Real 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 end;

theorem :: SERIES_5:18
for a, b, c, d being positive Real holds sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d))
proof end;

theorem :: SERIES_5:19
for a, b, c, d being positive Real holds ((a * b) + (c * d)) * ((a * c) + (b * d)) >= (((4 * a) * b) * c) * d
proof end;

theorem Th20: :: SERIES_5:20
for a, b, c being positive Real holds ((a / b) + (b / c)) + (c / a) >= 3
proof end;

theorem :: SERIES_5:21
for a, b, c being positive Real st ((a * b) + (b * c)) + (c * a) = 1 holds
(a + b) + c >= sqrt 3
proof end;

theorem :: SERIES_5:22
for a, b, c being positive Real holds ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3
proof end;

theorem :: SERIES_5:23
for a, b being positive Real holds (a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2
proof end;

theorem :: SERIES_5:24
for a, b, c being positive Real holds (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c
proof end;

theorem :: SERIES_5:25
for x, y, z being Real 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 end;

theorem :: SERIES_5:26
for a, b, c being positive Real st a > b & b > c holds
b / (a - b) > c / (a - c)
proof end;

theorem :: SERIES_5:27
for a, b, c, d being positive Real st b > a & c > d holds
c / (c + a) > d / (d + b)
proof end;

theorem :: SERIES_5:28
for m, x, y, z being Real holds (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2)))
proof end;

theorem Th29: :: SERIES_5:29
for m, u, w, x, y, z being Real holds (((m * x) + (u * y)) + (w * z)) ^2 <= (((m ^2) + (u ^2)) + (w ^2)) * (((x ^2) + (y ^2)) + (z ^2))
proof end;

theorem :: SERIES_5:30
for a, b, c being positive Real holds (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c
proof end;

theorem :: SERIES_5:31
for a, b, c being positive Real 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 end;

theorem :: SERIES_5:32
for a, b, c being positive Real 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 end;

theorem :: SERIES_5:33
for a, b, c being positive Real 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 end;

theorem :: SERIES_5:34
for a, b, c being positive Real holds sqrt (3 * (((a ^2) + (b ^2)) + (c ^2))) <= (((b * c) / a) + ((c * a) / b)) + ((a * b) / c)
proof end;

theorem :: SERIES_5:35
for a, b being positive Real st a + b = 1 holds
((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9
proof end;

theorem :: SERIES_5:36
for a, b being positive Real st a + b = 1 holds
(a * b) + (1 / (a * b)) >= 17 / 4
proof end;

theorem :: SERIES_5:37
for a, b, c being positive Real st (a + b) + c = 1 holds
((1 / a) + (1 / b)) + (1 / c) >= 9
proof end;

theorem :: SERIES_5:38
for a, b, c being positive Real st (a + b) + c = 1 holds
(((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8
proof end;

theorem :: SERIES_5:39
for a, b, c being positive Real st (a + b) + c = 1 holds
((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64
proof end;

theorem :: SERIES_5:40
for x, y, z being Real st (x + y) + z = 1 holds
((x ^2) + (y ^2)) + (z ^2) >= 1 / 3
proof end;

theorem :: SERIES_5:41
for x, y, z being Real st (x + y) + z = 1 holds
((x * y) + (y * z)) + (z * x) <= 1 / 3
proof end;

theorem :: SERIES_5:42
for a, b, c being positive Real 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 end;

theorem :: SERIES_5:43
for a, b being positive Real
for n being Nat st n >= 1 holds
(a |^ (n + 1)) + (b |^ (n + 1)) >= ((a |^ n) * b) + (a * (b |^ n))
proof end;

theorem :: SERIES_5:44
for a, b, c being positive Real
for n being Nat st (a ^2) + (b ^2) = c ^2 & n >= 3 holds
(a |^ (n + 2)) + (b |^ (n + 2)) < c |^ (n + 2)
proof end;

theorem :: SERIES_5:45
for n being Nat st n >= 1 holds
(1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1)
proof end;

theorem :: SERIES_5:46
for a, b being positive Real
for n, k being Nat st n >= 1 & k >= 1 holds
((a |^ k) + (b |^ k)) * ((a |^ n) + (b |^ n)) <= 2 * ((a |^ (k + n)) + (b |^ (k + n)))
proof end;

theorem :: SERIES_5:47
for s being Real_Sequence st ( for n being Nat holds s . n = 1 / (sqrt (n + 1)) ) holds
for n being Nat holds (Partial_Sums s) . n < 2 * (sqrt (n + 1))
proof end;

theorem Th48: :: SERIES_5:48
for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) holds
for n being Nat holds (Partial_Sums s) . n <= 2 - (1 / (n + 1))
proof end;

theorem :: SERIES_5:49
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) holds
(Partial_Sums s) . n < 2
proof end;

theorem Th50: :: SERIES_5:50
for s being Real_Sequence st ( for n being Nat holds s . n < 1 ) holds
for n being Nat holds (Partial_Sums s) . n < n + 1
proof end;

theorem :: SERIES_5:51
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n < 1 ) ) holds
for n being Nat holds (Partial_Product s) . n >= ((Partial_Sums s) . n) - n
proof end;

theorem Th52: :: SERIES_5:52
for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s1 . n = 1 / (s . n) ) ) holds
for n being Nat holds (Partial_Sums s1) . n > 0
proof end;

theorem :: SERIES_5:53
for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s1 . n = 1 / (s . n) ) ) holds
for n being Nat holds ((Partial_Sums s) . n) * ((Partial_Sums s1) . n) >= (n + 1) ^2
proof end;

theorem :: SERIES_5:54
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n)
proof end;

theorem :: SERIES_5:55
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n > ((2 / 3) * n) * (sqrt n)
proof end;

theorem :: SERIES_5:56
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3))
proof end;

theorem :: SERIES_5:57
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = sqrt (n * (n + 1)) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n > (n * (n + 1)) / 2
proof end;