:: SERIES_3 semantic presentation

registration

let c₁ be real number ;
cluster abs a₁ -> non negative ;
coherence by COMPLEX1:132;

end;

Lemma1: for b₁ being real number holds b₁ ^2 = b₁ |^ 2

proof end;

Lemma2: 1 |^ 3 = 1
by NEWTON:15;

Lemma3: 2 |^ 3 = 8

proof end;

Lemma4: 3 |^ 3 = 27

proof end;

Lemma5: for b₁ being real number holds (- b₁) |^ 3 = - (b₁ |^ 3)

proof end;

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

proof end;

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

proof end;

Lemma8: for b₁, b₂, b₃ being real number st b₁ ^2 <= b₂ * b₃ holds
abs b₁ <= sqrt (b₂ * b₃)

proof end;

theorem Th1: :: SERIES_3:1

for b₁, b₂, b₃ being real number st b₁ > b₂ & b₂ >= 0 & b₃ >= 0 holds
b₂ / b₁ <= (b₂ + b₃) / (b₁ + b₃)

proof end;

theorem Th2: :: SERIES_3:2

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

proof end;

theorem Th3: :: SERIES_3:3

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

proof end;

theorem Th4: :: SERIES_3:4

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

proof end;

theorem Th5: :: SERIES_3:5

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

proof end;

theorem Th6: :: SERIES_3:6

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

proof end;

theorem Th7: :: SERIES_3:7

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

proof end;

theorem Th8: :: SERIES_3:8

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

proof end;

theorem Th9: :: SERIES_3:9

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

proof end;

theorem Th10: :: SERIES_3:10

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

proof end;

theorem Th11: :: SERIES_3:11

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

proof end;

theorem Th12: :: SERIES_3:12

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

proof end;

theorem Th13: :: SERIES_3:13

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

proof end;

theorem Th14: :: SERIES_3:14

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

proof end;

theorem Th15: :: SERIES_3:15

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

proof end;

theorem Th16: :: SERIES_3:16

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

proof end;

theorem Th17: :: SERIES_3:17

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

proof end;

theorem Th18: :: SERIES_3:18

for b₁, b₂ being real number st b₁ + b₂ = 1 holds
b₁ * b₂ <= 1 / 4

proof end;

theorem Th19: :: SERIES_3:19

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

proof end;

theorem Th20: :: SERIES_3:20

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

proof end;

theorem Th21: :: SERIES_3:21

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

proof end;

theorem Th22: :: SERIES_3:22

for b₁, b₂ being real positive number st b₁ + b₂ = 1 holds
(b₁ |^ 3) + (b₂ |^ 3) < 1

proof end;

theorem Th23: :: SERIES_3:23

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

proof end;

theorem Th24: :: SERIES_3:24

for b₁ being real positive number
for b₂ being real number st abs b₂ <= b₁ holds
b₂ ^2 <= b₁ ^2

proof end;

theorem Th25: :: SERIES_3:25

for b₁ being real positive number
for b₂ being real number st abs b₂ >= b₁ holds
b₂ ^2 >= b₁ ^2

proof end;

theorem Th26: :: SERIES_3:26

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

proof end;

theorem Th27: :: SERIES_3:27

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

proof end;

theorem Th28: :: SERIES_3:28

for b₁, b₂, b₃ being real number st b₁ > 0 & b₂ > 0 & b₃ < 0 & (b₁ + b₂) + b₃ = 0 holds
(((b₁ |^ 2) + (b₂ |^ 2)) + (b₃ |^ 2)) |^ 3 >= 6 * ((((b₁ |^ 3) + (b₂ |^ 3)) + (b₃ |^ 3)) ^2 )

proof end;

theorem Th29: :: SERIES_3:29

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

proof end;

theorem Th30: :: SERIES_3:30

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

proof end;

theorem Th31: :: SERIES_3:31

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

proof end;

theorem Th32: :: SERIES_3:32

for b₁, b₂ being real positive number
for b₃ being Nat holds ((b₁ |^ b₃) + (b₂ |^ b₃)) / 2 >= ((b₁ + b₂) / 2) |^ b₃

proof end;

theorem Th33: :: SERIES_3:33

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ > 0 ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ > 0

proof end;

theorem Th34: :: SERIES_3:34

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ >= 0 ) holds
for b₂ being Nat holds (Partial_Sums b₁) . b₂ >= 0

proof end;

theorem Th35: :: SERIES_3:35

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ < 0 ) holds
(Partial_Sums b₂) . b₁ < 0

proof end;

theorem Th36: :: SERIES_3:36

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

proof end;

theorem Th37: :: SERIES_3:37

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₂ . b₃ > 0 & b₂ . b₃ > b₂ . (b₃ - 1) ) ) holds
(b₁ + 1) * (b₂ . (b₁ + 1)) > (Partial_Sums b₂) . b₁

proof end;

theorem Th38: :: SERIES_3:38

for b₁, b₂, b₃ being Real_Sequence st b₁ = b₂ (#) b₃ & ( for b₄ being Nat holds
( b₂ . b₄ >= 0 & b₃ . b₄ >= 0 ) ) holds
for b₄ being Nat holds (Partial_Sums b₁) . b₄ <= ((Partial_Sums b₂) . b₄) * ((Partial_Sums b₃) . b₄)

proof end;

theorem Th39: :: SERIES_3:39

for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence st b₂ = b₃ (#) b₄ & ( for b₅ being Nat holds
( b₃ . b₅ < 0 & b₄ . b₅ < 0 ) ) holds
(Partial_Sums b₂) . b₁ <= ((Partial_Sums b₃) . b₁) * ((Partial_Sums b₄) . b₁)

proof end;

theorem Th40: :: SERIES_3:40

for b₁ being Real_Sequence
for b₂ being Nat holds abs ((Partial_Sums b₁) . b₂) <= (Partial_Sums (abs b₁)) . b₂

proof end;

theorem Th41: :: SERIES_3:41

for b₁ being Nat
for b₂ being Real_Sequence holds (Partial_Sums b₂) . b₁ <= (Partial_Sums (abs b₂)) . b₁

proof end;

definition

let c₁ be Real_Sequence;
func Partial_Product c₁ -> Real_Sequence means :Def1: :: SERIES_3:def 1
( a₂ . 0 = a₁ . 0 & ( for b₁ being Nat holds a₂ . (b₁ + 1) = (a₂ . b₁) * (a₁ . (b₁ + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Product SERIES_3:def 1 :

theorem Th42: :: SERIES_3:42

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ > 0 ) holds
(Partial_Product b₂) . b₁ > 0

proof end;

theorem Th43: :: SERIES_3:43

for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ >= 0 ) holds
(Partial_Product b₂) . b₁ >= 0

proof end;

theorem Th44: :: SERIES_3:44

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₂ > 0 & (Partial_Product b₁) . b₂ < 1 )

proof end;

theorem Th45: :: SERIES_3:45

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ >= 1 ) holds
for b₂ being Nat holds (Partial_Product b₁) . b₂ >= 1

proof end;

theorem Th46: :: SERIES_3:46

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₁ . b₃ >= 0 & b₂ . b₃ >= 0 ) ) holds
for b₃ being Nat holds ((Partial_Product b₁) . b₃) + ((Partial_Product b₂) . b₃) <= (Partial_Product (b₁ + b₂)) . b₃

proof end;

theorem Th47: :: SERIES_3:47

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

proof end;

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

proof end;

theorem Th48: :: SERIES_3:48

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

proof end;

Lemma31: for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ >= 0 ) holds
for b₂ being Nat holds ((Partial_Sums b₁) . b₂) * (b₁ . (b₂ + 1)) >= 0

proof end;

theorem Th49: :: SERIES_3:49

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

proof end;

theorem Th50: :: SERIES_3:50

for b₁, b₂, b₃, b₄, b₅ being Real_Sequence st b₁ = b₂ (#) b₃ & b₄ = b₂ (#) b₂ & b₅ = b₃ (#) b₃ holds
for b₆ being Nat holds ((Partial_Sums b₁) . b₆) ^2 <= ((Partial_Sums b₄) . b₆) * ((Partial_Sums b₅) . b₆)

proof end;

Lemma32: for b₁ being Nat
for b₂, b₃, b₄ being Real_Sequence st ( for b₅ being Nat holds b₂ . b₅ = ((b₃ . b₅) + (b₄ . b₅)) ^2 ) holds
(Partial_Sums b₂) . b₁ >= 0

proof end;

theorem Th51: :: SERIES_3:51

for b₁, b₂, b₃, b₄, b₅ being Real_Sequence st b₁ = b₂ (#) b₂ & b₃ = b₄ (#) b₄ & ( for b₆ being Nat holds
( b₂ . b₆ >= 0 & b₄ . b₆ >= 0 & b₅ . b₆ = ((b₂ . b₆) + (b₄ . b₆)) ^2 ) ) holds
for b₆ being Nat holds sqrt ((Partial_Sums b₅) . b₆) <= (sqrt ((Partial_Sums b₁) . b₆)) + (sqrt ((Partial_Sums b₃) . b₆))

proof end;

Lemma33: for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds b₂ . b₃ > 0 ) holds
(b₁ + 1) -root ((Partial_Product b₂) . b₁) > 0

proof end;

Lemma34: for b₁ being Nat
for b₂ being Real_Sequence st ( for b₃ being Nat holds
( b₂ . b₃ > 0 & b₂ . b₃ > b₂ . (b₃ - 1) ) ) holds
((b₂ . (b₁ + 1)) - (((Partial_Sums b₂) . b₁) / (b₁ + 1))) / (b₁ + 2) > 0

proof end;

theorem Th52: :: SERIES_3:52

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

proof end;