:: SERIES_5 semantic presentation

Lm2: for x, y being real number holds (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2 ) + (x * y)) + (y ^2 ))

proof end;

Lm3: for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b)

proof end;

Lm4: for x, y, z being real number holds ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z)

proof end;

Lm5: for a, c being real positive number
for b being real number holds (a / c) to_power (- b) = (c / a) to_power b

proof end;

Lm6: 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 end;

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

Lm13: for x being real number st abs x < 1 holds
x ^2 < 1

proof end;

Lm15: for x being real number st x ^2 < 1 holds
abs x < 1

proof end;

Lm21: 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 end;

Lm22: 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 end;

Lm23: for a, b being real positive number holds sqrt (((a ^2 ) + (a * b)) + (b ^2 )) >= ((1 / 2) * (sqrt 3)) * (a + b)

proof end;

Lm24: for a, b being real positive number holds sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3) <= sqrt (((a ^2 ) + (b ^2 )) / 2)

proof end;

Lm26: for b, c, a being real positive number holds (((b * c) / a) ^2 ) + (((c * a) / b) ^2 ) >= 2 * (c ^2 )

proof end;

Lm27: for b, c, a being real positive number holds ((b * c) / a) * ((c * a) / b) = c ^2

proof end;

Lm28: 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 end;

Lm29: 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 end;

Lm30: for a, b, c being real positive number st (a + b) + c = 1 holds
(1 / a) - 1 = (b + c) / a

proof end;

Lm31: 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 end;

Lm32: for a, b, c being real positive number st (a + b) + c = 1 holds
1 + (1 / a) = 2 + ((b + c) / a)

proof end;

Lm33: 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 end;

Lm34: 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 end;

Lm35: 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 end;

Lm36: 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 end;

theorem :: SERIES_5:1

for a, b being real positive number holds (a + b) * ((1 / a) + (1 / b)) >= 4

proof end;

theorem :: SERIES_5:2

for a, b being real positive number holds (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3))

proof end;

theorem Th1: :: SERIES_5:3

for a, b, c being real positive number st a < b holds
1 < (b + c) / (a + c)

proof end;

theorem Th2: :: SERIES_5:4

for a, b being real positive number st a < b holds
a / b < sqrt (a / b)

proof end;

theorem Th3: :: 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 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 end;

theorem Th5: :: SERIES_5:7

for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) <= sqrt (a * b)

proof end;

theorem Th6: :: SERIES_5:8

for a, b being real positive number holds (a + b) / 2 <= sqrt (((a ^2 ) + (b ^2 )) / 2)

proof end;

theorem :: SERIES_5:9

for x, y being real number holds x + y <= sqrt (2 * ((x ^2 ) + (y ^2 )))

proof end;

theorem Th7: :: SERIES_5:10

for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) <= (a + b) / 2

proof end;

theorem :: SERIES_5:11

for a, b being real positive number holds sqrt (a * b) <= sqrt (((a ^2 ) + (b ^2 )) / 2)

proof 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 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 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 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 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 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 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 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 end;

theorem Th12: :: SERIES_5:20

for a, b, c being real positive number holds ((a / b) + (b / c)) + (c / a) >= 3

proof 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 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 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 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 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 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 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 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 end;

theorem Th15: :: 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 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 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 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 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 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 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 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 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 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 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 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 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 end;

theorem :: SERIES_5:42

for a, b, c being real positive number st (a * b) * c = 1 holds
((sqrt a) + (sqrt b)) + (sqrt c) <= ((1 / a) + (1 / b)) + (1 / c)

proof end;

theorem :: SERIES_5:43

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

theorem :: SERIES_5:44

for a, b being real positive number
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:45

for a, b, c being real positive number
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 n being Nat st n >= 1 holds
(1 + (1 / (n + 1))) |^ n < (1 + (1 / n)) |^ (n + 1)

proof end;

theorem :: SERIES_5:47

for a, b being real positive number
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:48

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 Th4: :: SERIES_5:49

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

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 Th9: :: SERIES_5:51

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

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 Th11: :: 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 s1) . n > 0

proof end;

theorem :: SERIES_5:54

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: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 < ((1 / 6) * ((4 * n) + 3)) * (sqrt n)

proof end;

theorem :: SERIES_5:56

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

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

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;