:: SERIES_5 semantic presentation

Lemma1: for b₁, b₂ being real number holds (b₁ |^ 3) - (b₂ |^ 3) = (b₁ - b₂) * (((b₁ ^2 ) + (b₁ * b₂)) + (b₂ ^2 ))

proof end;

Lemma2: for b₁, b₂ being real positive number holds 2 / ((1 / b₁) + (1 / b₂)) = (2 * (b₁ * b₂)) / (b₁ + b₂)

proof end;

Lemma3: for b₁, b₂, b₃ being real number holds ((1 / b₁) * (1 / b₂)) * (1 / b₃) = 1 / ((b₁ * b₂) * b₃)

proof end;

Lemma4: for b₁, b₂ being real positive number
for b₃ being real number holds (b₁ / b₂) to_power (- b₃) = (b₂ / b₁) to_power b₃

proof end;

Lemma5: for b₁, b₂, b₃, b₄ being real positive number holds (((sqrt (b₁ * b₂)) ^2 ) + ((sqrt (b₃ * b₄)) ^2 )) * (((sqrt (b₁ * b₃)) ^2 ) + ((sqrt (b₂ * b₄)) ^2 )) >= (b₂ * b₃) * ((b₁ + b₄) ^2 )

proof end;

Lemma6: for b₁, b₂, b₃ being real number holds ((b₁ + b₂) + b₃) ^2 = (((((b₁ ^2 ) + (b₂ ^2 )) + (b₃ ^2 )) + ((2 * b₁) * b₂)) + ((2 * b₂) * b₃)) + ((2 * b₃) * b₁)
;

Lemma7: for b₁ being real number st abs b₁ < 1 holds
b₁ ^2 < 1

proof end;

Lemma8: for b₁ being real number st b₁ ^2 < 1 holds
abs b₁ < 1

proof end;

Lemma9: for b₁, b₂, b₃ being real positive number holds (((((((2 * (b₁ ^2 )) * (sqrt (b₂ * b₃))) * 2) * (b₂ ^2 )) * (sqrt (b₁ * b₃))) * 2) * (b₃ ^2 )) * (sqrt (b₁ * b₂)) = (((2 * b₁) * b₂) * b₃) |^ 3

proof end;

Lemma10: for b₁, b₂ being real positive number holds sqrt (((b₁ ^2 ) + (b₁ * b₂)) + (b₂ ^2 )) = (1 / 2) * (sqrt ((4 * ((b₁ ^2 ) + (b₂ ^2 ))) + ((4 * b₁) * b₂)))

proof end;

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

proof end;

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

proof end;

Lemma13: for b₁, b₂, b₃ being real positive number holds (((b₁ * b₂) / b₃) ^2 ) + (((b₂ * b₃) / b₁) ^2 ) >= 2 * (b₂ ^2 )

proof end;

Lemma14: for b₁, b₂, b₃ being real positive number holds ((b₁ * b₂) / b₃) * ((b₂ * b₃) / b₁) = b₂ ^2

proof end;

Lemma15: for b₁, b₂, b₃ being real positive number holds (((2 * ((b₁ * b₂) / b₃)) * ((b₂ * b₃) / b₁)) + ((2 * ((b₁ * b₂) / b₃)) * ((b₃ * b₁) / b₂))) + ((2 * ((b₂ * b₃) / b₁)) * ((b₃ * b₁) / b₂)) = 2 * (((b₃ ^2 ) + (b₁ ^2 )) + (b₂ ^2 ))

proof end;

Lemma16: for b₁, b₂, b₃ being real positive number holds ((((b₁ * b₂) / b₃) + ((b₂ * b₃) / b₁)) + ((b₃ * b₁) / b₂)) ^2 = (((((b₂ * b₃) / b₁) ^2 ) + (((b₃ * b₁) / b₂) ^2 )) + (((b₁ * b₂) / b₃) ^2 )) + (2 * (((b₃ ^2 ) + (b₁ ^2 )) + (b₂ ^2 )))

proof end;

Lemma17: for b₁, b₂, b₃ being real positive number st (b₁ + b₂) + b₃ = 1 holds
(1 / b₁) - 1 = (b₂ + b₃) / b₁

proof end;

Lemma18: for b₁, b₂, b₃ being real positive number holds (((2 * (sqrt (b₁ * b₂))) / b₃) * ((2 * (sqrt (b₃ * b₂))) / b₁)) * ((2 * (sqrt (b₃ * b₁))) / b₂) = 8

proof end;

Lemma19: for b₁, b₂, b₃ being real positive number st (b₁ + b₂) + b₃ = 1 holds
1 + (1 / b₁) = 2 + ((b₂ + b₃) / b₁)

proof end;

Lemma20: for b₁, b₂, b₃ being real positive number holds (1 + ((sqrt (b₁ * b₂)) / b₃)) * ((sqrt (b₁ * b₃)) / b₂) = ((sqrt (b₁ * b₃)) / b₂) + (b₁ / (sqrt (b₃ * b₂)))

proof end;

Lemma21: for b₁, b₂, b₃ being real positive number holds (((sqrt (b₁ * b₂)) / b₃) + (b₂ / (sqrt (b₁ * b₃)))) * ((sqrt (b₃ * b₁)) / b₂) = (b₁ / (sqrt (b₃ * b₂))) + 1

proof end;

Lemma22: for b₁, b₂, b₃ being real positive number holds ((1 + ((sqrt (b₁ * b₂)) / b₃)) * (1 + ((sqrt (b₃ * b₂)) / b₁))) * (1 + ((sqrt (b₃ * b₁)) / b₂)) = (((((2 + ((sqrt (b₃ * b₂)) / b₁)) + (b₁ / (sqrt (b₃ * b₂)))) + ((sqrt (b₃ * b₁)) / b₂)) + (b₂ / (sqrt (b₁ * b₃)))) + (b₃ / (sqrt (b₁ * b₂)))) + ((sqrt (b₁ * b₂)) / b₃)

proof end;

Lemma23: for b₁, b₂, b₃ being real positive number holds ((((((sqrt (b₁ * b₂)) / b₃) + (b₃ / (sqrt (b₁ * b₂)))) + ((sqrt (b₁ * b₃)) / b₂)) + (b₂ / (sqrt (b₃ * b₁)))) + (b₁ / (sqrt (b₃ * b₂)))) + ((sqrt (b₃ * b₂)) / b₁) >= 6

proof end;

theorem Th1: :: SERIES_5:1

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

proof end;

theorem Th2: :: SERIES_5:2

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

proof end;

theorem Th3: :: SERIES_5:3

for b₁, b₂, b₃ being real positive number st b₁ < b₂ holds
1 < (b₂ + b₃) / (b₁ + b₃)

proof end;

theorem Th4: :: SERIES_5:4

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

proof end;

theorem Th5: :: SERIES_5:5

for b₁, b₂ being real positive number st b₁ < b₂ holds
sqrt (b₁ / b₂) < (b₂ + (sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2))) / (b₁ + (sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2)))

proof end;

theorem Th6: :: SERIES_5:6

for b₁, b₂ being real positive number st b₁ < b₂ holds
b₁ / b₂ < (b₂ + (sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2))) / (b₁ + (sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2)))

proof end;

theorem Th7: :: SERIES_5:7

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

proof end;

theorem Th8: :: SERIES_5:8

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

proof end;

theorem Th9: :: SERIES_5:9

for b₁, b₂ being real number holds b₁ + b₂ <= sqrt (2 * ((b₁ ^2 ) + (b₂ ^2 )))

proof end;

theorem Th10: :: SERIES_5:10

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

proof end;

theorem Th11: :: SERIES_5:11

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

proof end;

theorem Th12: :: SERIES_5:12

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

proof end;

theorem Th13: :: SERIES_5:13

for b₁, b₂ being real number st abs b₁ < 1 & abs b₂ < 1 holds
abs ((b₁ + b₂) / (1 + (b₁ * b₂))) <= 1

proof end;

theorem Th14: :: SERIES_5:14

for b₁, b₂ being real number holds (abs (b₁ + b₂)) / (1 + (abs (b₁ + b₂))) <= ((abs b₁) / (1 + (abs b₁))) + ((abs b₂) / (1 + (abs b₂)))

proof end;

theorem Th15: :: SERIES_5:15

for b₁, b₂, b₃, b₄ being real positive number holds (((b₁ / ((b₁ + b₂) + b₃)) + (b₂ / ((b₁ + b₂) + b₄))) + (b₄ / ((b₂ + b₄) + b₃))) + (b₃ / ((b₁ + b₄) + b₃)) > 1

proof end;

theorem Th16: :: SERIES_5:16

for b₁, b₂, b₃, b₄ being real positive number holds (((b₁ / ((b₁ + b₂) + b₃)) + (b₂ / ((b₁ + b₂) + b₄))) + (b₄ / ((b₂ + b₄) + b₃))) + (b₃ / ((b₁ + b₄) + b₃)) < 2

proof end;

theorem Th17: :: SERIES_5:17

for b₁, b₂, b₃ being real positive number st b₁ + b₂ > b₃ & b₂ + b₃ > b₁ & b₁ + b₃ > b₂ holds
((1 / ((b₁ + b₂) - b₃)) + (1 / ((b₂ + b₃) - b₁))) + (1 / ((b₃ + b₁) - b₂)) >= 9 / ((b₁ + b₂) + b₃)

proof end;

theorem Th18: :: SERIES_5:18

for b₁, b₂, b₃, b₄ being real positive number holds sqrt ((b₁ + b₂) * (b₃ + b₄)) >= (sqrt (b₁ * b₃)) + (sqrt (b₂ * b₄))

proof end;

theorem Th19: :: SERIES_5:19

for b₁, b₂, b₃, b₄ being real positive number holds ((b₁ * b₂) + (b₃ * b₄)) * ((b₁ * b₃) + (b₂ * b₄)) >= (((4 * b₁) * b₂) * b₃) * b₄

proof end;

theorem Th20: :: SERIES_5:20

for b₁, b₂, b₃ being real positive number holds ((b₁ / b₂) + (b₂ / b₃)) + (b₃ / b₁) >= 3

proof end;

theorem Th21: :: SERIES_5:21

for b₁, b₂, b₃ being real positive number st ((b₁ * b₂) + (b₂ * b₃)) + (b₃ * b₁) = 1 holds
(b₁ + b₂) + b₃ >= sqrt 3

proof end;

theorem Th22: :: SERIES_5:22

for b₁, b₂, b₃ being real positive number holds ((((b₁ + b₂) - b₃) / b₃) + (((b₂ + b₃) - b₁) / b₁)) + (((b₃ + b₁) - b₂) / b₂) >= 3

proof end;

theorem Th23: :: SERIES_5:23

for b₁, b₂ being real positive number holds (b₁ + (1 / b₁)) * (b₂ + (1 / b₂)) >= ((sqrt (b₁ * b₂)) + (1 / (sqrt (b₁ * b₂)))) ^2

proof end;

theorem Th24: :: SERIES_5:24

for b₁, b₂, b₃ being real positive number holds (((b₁ * b₂) / b₃) + ((b₃ * b₂) / b₁)) + ((b₃ * b₁) / b₂) >= (b₃ + b₁) + b₂

proof end;

theorem Th25: :: SERIES_5:25

for b₁, b₂, b₃ being real number st b₁ > b₂ & b₂ > b₃ holds
(((b₁ ^2 ) * b₂) + ((b₂ ^2 ) * b₃)) + ((b₃ ^2 ) * b₁) > ((b₁ * (b₂ ^2 )) + (b₂ * (b₃ ^2 ))) + (b₃ * (b₁ ^2 ))

proof end;

theorem Th26: :: SERIES_5:26

for b₁, b₂, b₃ being real positive number st b₁ > b₂ & b₂ > b₃ holds
b₂ / (b₁ - b₂) > b₃ / (b₁ - b₃)

proof end;

theorem Th27: :: SERIES_5:27

for b₁, b₂, b₃, b₄ being real positive number st b₁ > b₂ & b₃ > b₄ holds
b₃ / (b₃ + b₂) > b₄ / (b₄ + b₁)

proof end;

theorem Th28: :: SERIES_5:28

for b₁, b₂, b₃, b₄ being real number holds (b₁ * b₂) + (b₃ * b₄) <= (sqrt ((b₁ ^2 ) + (b₃ ^2 ))) * (sqrt ((b₂ ^2 ) + (b₄ ^2 )))

proof end;

theorem Th29: :: SERIES_5:29

for b₁, b₂, b₃, b₄, b₅, b₆ being real number holds (((b₁ * b₂) + (b₃ * b₄)) + (b₅ * b₆)) ^2 <= (((b₁ ^2 ) + (b₃ ^2 )) + (b₅ ^2 )) * (((b₂ ^2 ) + (b₄ ^2 )) + (b₆ ^2 ))

proof end;

theorem Th30: :: SERIES_5:30

for b₁, b₂, b₃ being real positive number holds (((9 * b₁) * b₂) * b₃) / (((b₁ ^2 ) + (b₂ ^2 )) + (b₃ ^2 )) <= (b₁ + b₂) + b₃

proof end;

theorem Th31: :: SERIES_5:31

for b₁, b₂, b₃ being real positive number holds (b₁ + b₂) + b₃ <= ((sqrt ((((b₁ ^2 ) + (b₁ * b₂)) + (b₂ ^2 )) / 3)) + (sqrt ((((b₂ ^2 ) + (b₂ * b₃)) + (b₃ ^2 )) / 3))) + (sqrt ((((b₃ ^2 ) + (b₃ * b₁)) + (b₁ ^2 )) / 3))

proof end;

theorem Th32: :: SERIES_5:32

for b₁, b₂, b₃ being real positive number holds ((sqrt ((((b₁ ^2 ) + (b₁ * b₂)) + (b₂ ^2 )) / 3)) + (sqrt ((((b₂ ^2 ) + (b₂ * b₃)) + (b₃ ^2 )) / 3))) + (sqrt ((((b₃ ^2 ) + (b₃ * b₁)) + (b₁ ^2 )) / 3)) <= ((sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2)) + (sqrt (((b₂ ^2 ) + (b₃ ^2 )) / 2))) + (sqrt (((b₃ ^2 ) + (b₁ ^2 )) / 2))

proof end;

theorem Th33: :: SERIES_5:33

for b₁, b₂, b₃ being real positive number holds ((sqrt (((b₁ ^2 ) + (b₂ ^2 )) / 2)) + (sqrt (((b₂ ^2 ) + (b₃ ^2 )) / 2))) + (sqrt (((b₃ ^2 ) + (b₁ ^2 )) / 2)) <= sqrt (3 * (((b₁ ^2 ) + (b₂ ^2 )) + (b₃ ^2 )))

proof end;

theorem Th34: :: SERIES_5:34

for b₁, b₂, b₃ being real positive number holds sqrt (3 * (((b₁ ^2 ) + (b₂ ^2 )) + (b₃ ^2 ))) <= (((b₂ * b₃) / b₁) + ((b₃ * b₁) / b₂)) + ((b₁ * b₂) / b₃)

proof end;

theorem Th35: :: SERIES_5:35

for b₁, b₂ being real positive number st b₁ + b₂ = 1 holds
((1 / (b₁ ^2 )) - 1) * ((1 / (b₂ ^2 )) - 1) >= 9

proof end;

theorem Th36: :: SERIES_5:36

for b₁, b₂ being real positive number st b₁ + b₂ = 1 holds
(b₁ * b₂) + (1 / (b₁ * b₂)) >= 17 / 4

proof end;

theorem Th37: :: SERIES_5:37

for b₁, b₂, b₃ being real positive number st (b₁ + b₂) + b₃ = 1 holds
((1 / b₁) + (1 / b₂)) + (1 / b₃) >= 9

proof end;

theorem Th38: :: SERIES_5:38

for b₁, b₂, b₃ being real positive number st (b₁ + b₂) + b₃ = 1 holds
(((1 / b₁) - 1) * ((1 / b₂) - 1)) * ((1 / b₃) - 1) >= 8

proof end;

theorem Th39: :: SERIES_5:39

for b₁, b₂, b₃ being real positive number st (b₁ + b₂) + b₃ = 1 holds
((1 + (1 / b₁)) * (1 + (1 / b₂))) * (1 + (1 / b₃)) >= 64

proof end;

theorem Th40: :: SERIES_5:40

for b₁, b₂, b₃ being real number st (b₁ + b₂) + b₃ = 1 holds
((b₁ ^2 ) + (b₂ ^2 )) + (b₃ ^2 ) >= 1 / 3

proof end;

theorem Th41: :: SERIES_5:41

for b₁, b₂, b₃ being real number st (b₁ + b₂) + b₃ = 1 holds
((b₁ * b₂) + (b₂ * b₃)) + (b₃ * b₁) <= 1 / 3

proof end;

theorem Th42: :: SERIES_5:42

for b₁, b₂, b₃ being real positive number st (b₁ * b₂) * b₃ = 1 holds
((sqrt b₁) + (sqrt b₂)) + (sqrt b₃) <= ((1 / b₁) + (1 / b₂)) + (1 / b₃)

proof end;

theorem Th43: :: SERIES_5:43

for b₁, b₂, b₃ being real positive number st b₁ > b₂ & b₂ > b₃ holds
((b₁ to_power (2 * b₁)) * (b₂ to_power (2 * b₂))) * (b₃ to_power (2 * b₃)) > ((b₁ to_power (b₂ + b₃)) * (b₂ to_power (b₁ + b₃))) * (b₃ to_power (b₁ + b₂))

proof end;

theorem Th44: :: SERIES_5:44

for b₁, b₂ being real positive number
for b₃ being Nat st b₃ >= 1 holds
(b₁ |^ (b₃ + 1)) + (b₂ |^ (b₃ + 1)) >= ((b₁ |^ b₃) * b₂) + (b₁ * (b₂ |^ b₃))

proof end;

theorem Th45: :: SERIES_5:45

for b₁, b₂, b₃ being real positive number
for b₄ being Nat st (b₁ ^2 ) + (b₂ ^2 ) = b₃ ^2 & b₄ >= 3 holds
(b₁ |^ (b₄ + 2)) + (b₂ |^ (b₄ + 2)) < b₃ |^ (b₄ + 2)

proof end;

theorem Th46: :: SERIES_5:46

for b₁ being Nat st b₁ >= 1 holds
(1 + (1 / (b₁ + 1))) |^ b₁ < (1 + (1 / b₁)) |^ (b₁ + 1)

proof end;

theorem Th47: :: SERIES_5:47

for b₁, b₂ being real positive number
for b₃, b₄ being Nat st b₃ >= 1 & b₄ >= 1 holds
((b₁ |^ b₄) + (b₂ |^ b₄)) * ((b₁ |^ b₃) + (b₂ |^ b₃)) <= 2 * ((b₁ |^ (b₄ + b₃)) + (b₂ |^ (b₄ + b₃)))

proof end;

theorem Th48: :: SERIES_5:48

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 1 / (sqrt (b₂ + 1)) ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ < 2 * (sqrt (b₂ + 1))

proof end;

theorem Th49: :: SERIES_5:49

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 1 / ((b₂ + 1) ^2 ) ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ <= 2 - (1 / (b₂ + 1))

proof end;

theorem Th50: :: SERIES_5:50

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ = 1 / ((b₃ + 1) ^2 ) ) holds
(Partial_Sums b₂) . b₁ < 2

proof end;

theorem Th51: :: SERIES_5:51

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ < 1 ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ < b₂ + 1

proof end;

theorem Th52: :: SERIES_5:52

for b₁ being Real_Sequence st ( for b₂ being Nat holds
( b₁ . b₂ > 0 & b₁ . b₂ < 1 ) ) holds
for b₂ being Nat holds (Partial_Product b₁) . b₂ >= ((Partial_Sums b₁) . b₂) - b₂

proof end;

theorem Th53: :: SERIES_5:53

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ > 0 & b₂ . b₃ = 1 / (b₁ . b₃) ) ) holds
for b₃ being Nat holds (Partial_Sums b₂) . b₃ > 0

proof end;

theorem Th54: :: SERIES_5:54

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ > 0 & b₂ . b₃ = 1 / (b₁ . b₃) ) ) holds
for b₃ being Nat holds ((Partial_Sums b₁) . b₃) * ((Partial_Sums b₂) . b₃) >= (b₃ + 1) ^2

proof end;

theorem Th55: :: SERIES_5:55

for b₁ being Real_Sequence st ( for b₂ being Nat st b₂ >= 1 holds
( b₁ . b₂ = sqrt b₂ & b₁ . 0 = 0 ) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Sums b₁) . b₂ < ((1 / 6) * ((4 * b₂) + 3)) * (sqrt b₂)

proof end;

theorem Th56: :: SERIES_5:56

for b₁ being Real_Sequence st ( for b₂ being Nat st b₂ >= 1 holds
( b₁ . b₂ = sqrt b₂ & b₁ . 0 = 0 ) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Sums b₁) . b₂ > ((2 / 3) * b₂) * (sqrt b₂)

proof end;

theorem Th57: :: SERIES_5:57

for b₁ being Real_Sequence st ( for b₂ being Nat st b₂ >= 1 holds
( b₁ . b₂ = 1 + (1 / ((2 * b₂) + 1)) & b₁ . 0 = 1 ) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Product b₁) . b₂ > (1 / 2) * (sqrt ((2 * b₂) + 3))

proof end;

theorem Th58: :: SERIES_5:58

for b₁ being Real_Sequence st ( for b₂ being Nat st b₂ >= 1 holds
( b₁ . b₂ = sqrt (b₂ * (b₂ + 1)) & b₁ . 0 = 0 ) ) holds
for b₂ being Nat st b₂ >= 1 holds
(Partial_Sums b₁) . b₂ > (b₂ * (b₂ + 1)) / 2

proof end;