:: 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 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)))

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)))

a / b < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))

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)

((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 :: 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))

(((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2))

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:38

for a, b, c being positive Real st (a + b) + c = 1 holds

(((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8

(((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

((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64

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))

((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))

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)

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: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)))

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))

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))

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

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

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

( 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

( 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

( 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)

( 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)

( 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))

( 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

( 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;