:: by Fuguo Ge and Xiquan Liang

::

:: Received July 6, 2005

:: Copyright (c) 2005-2016 Association of Mizar Users

Lm1: for x being Real holds x ^2 = x |^ 2

proof end;

Lm2: 2 |^ 3 = 8

proof end;

Lm3: 3 |^ 3 = 27

proof end;

Lm4: for x being Real holds (- x) |^ 3 = - (x |^ 3)

proof end;

Lm5: for x, y being Real holds (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3)

proof end;

Lm6: for x, y being Real holds (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2))

proof end;

Lm7: for x, y, z being Real st x ^2 <= y * z holds

|.x.| <= sqrt (y * z)

proof end;

theorem :: SERIES_3:14

for a, b, c being positive Real holds (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c)

proof end;

theorem :: SERIES_3:27

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

((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c)

((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c)

proof end;

theorem :: SERIES_3:28

for x, y, z being Real st x > 0 & y > 0 & z < 0 & (x + y) + z = 0 holds

(((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2)

(((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2)

proof end;

theorem :: SERIES_3:29

for a, b, c being positive Real st a >= 1 holds

(a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))

(a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))

proof end;

theorem :: SERIES_3:30

for a, b, c being positive Real st a >= b & b >= c holds

((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)

((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)

proof end;

theorem Th31: :: SERIES_3:31

for n being Nat

for a, b being non negative Real holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)

for a, b being non negative Real holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)

proof end;

theorem Th33: :: SERIES_3:33

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds

for n being Nat holds (Partial_Sums s) . n > 0

for n being Nat holds (Partial_Sums s) . n > 0

proof end;

theorem Th34: :: SERIES_3:34

for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds

for n being Nat holds (Partial_Sums s) . n >= 0

for n being Nat holds (Partial_Sums s) . n >= 0

proof end;

theorem Th35: :: SERIES_3:35

for n being Nat

for s being Real_Sequence st ( for n being Nat holds s . n < 0 ) holds

(Partial_Sums s) . n < 0

for s being Real_Sequence st ( for n being Nat holds s . n < 0 ) holds

(Partial_Sums s) . n < 0

proof end;

theorem Th36: :: SERIES_3:36

for s, s1 being Real_Sequence st s = s1 (#) s1 holds

for n being Nat holds (Partial_Sums s) . n >= 0

for n being Nat holds (Partial_Sums s) . n >= 0

proof end;

theorem :: SERIES_3:37

for n being Nat

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n > s . (n - 1) ) ) holds

(n + 1) * (s . (n + 1)) > (Partial_Sums s) . n

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n > s . (n - 1) ) ) holds

(n + 1) * (s . (n + 1)) > (Partial_Sums s) . n

proof end;

theorem Th38: :: SERIES_3:38

for n being Nat

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n >= s . (n - 1) ) ) holds

(n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n >= s . (n - 1) ) ) holds

(n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n

proof end;

theorem :: SERIES_3:39

for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds

( s1 . n >= 0 & s2 . n >= 0 ) ) holds

for n being Nat holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)

( s1 . n >= 0 & s2 . n >= 0 ) ) holds

for n being Nat holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)

proof end;

theorem :: SERIES_3:40

for n being Nat

for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds

( s1 . n < 0 & s2 . n < 0 ) ) holds

(Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)

for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds

( s1 . n < 0 & s2 . n < 0 ) ) holds

(Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)

proof end;

theorem Th41: :: SERIES_3:41

for s being Real_Sequence

for n being Nat holds |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n

for n being Nat holds |.((Partial_Sums s) . n).| <= (Partial_Sums (abs s)) . n

proof end;

definition

let s be Real_Sequence;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (s . (n + 1)) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (s . (n + 1)) ) & b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * (s . (n + 1)) ) holds

b_{1} = b_{2}

end;
func Partial_Product s -> Real_Sequence means :Def1: :: SERIES_3:def 1

( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) * (s . (n + 1)) ) );

existence ( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) * (s . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Partial_Product SERIES_3:def 1 :

for s, b_{2} being Real_Sequence holds

( b_{2} = Partial_Product s iff ( b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * (s . (n + 1)) ) ) );

for s, b

( b

theorem Th43: :: SERIES_3:43

for n being Nat

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds

(Partial_Product s) . n > 0

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds

(Partial_Product s) . n > 0

proof end;

theorem Th44: :: SERIES_3:44

for n being Nat

for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds

(Partial_Product s) . n >= 0

for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds

(Partial_Product s) . n >= 0

proof end;

theorem :: SERIES_3:45

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 > 0 & (Partial_Product s) . n < 1 )

( s . n > 0 & s . n < 1 ) ) holds

for n being Nat holds

( (Partial_Product s) . n > 0 & (Partial_Product s) . n < 1 )

proof end;

theorem :: SERIES_3:46

for s being Real_Sequence st ( for n being Nat holds s . n >= 1 ) holds

for n being Nat holds (Partial_Product s) . n >= 1

for n being Nat holds (Partial_Product s) . n >= 1

proof end;

theorem :: SERIES_3:47

for s1, s2 being Real_Sequence st ( for n being Nat holds

( s1 . n >= 0 & s2 . n >= 0 ) ) holds

for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n

( s1 . n >= 0 & s2 . n >= 0 ) ) holds

for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n

proof end;

theorem :: SERIES_3:48

for n being Nat

for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds

(Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))

for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds

(Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))

proof end;

Lm8: for s being Real_Sequence st ( for n being Nat holds

( s . n > - 1 & s . n < 0 ) ) holds

for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0

proof end;

theorem :: SERIES_3:49

for s, s1 being Real_Sequence st ( for n being Nat holds

( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ) holds

for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n

( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ) holds

for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n

proof end;

Lm9: for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds

for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0

proof end;

theorem :: SERIES_3:50

for s, s1 being Real_Sequence st ( for n being Nat holds

( s1 . n = 1 + (s . n) & s . n >= 0 ) ) holds

for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n

( s1 . n = 1 + (s . n) & s . n >= 0 ) ) holds

for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n

proof end;

theorem :: SERIES_3:51

for s1, s2, s3, s4, s5 being Real_Sequence st s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 holds

for n being Nat holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)

for n being Nat holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)

proof end;

Lm10: for n being Nat

for s, s1, s2 being Real_Sequence st ( for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds

(Partial_Sums s) . n >= 0

proof end;

theorem :: SERIES_3:52

for s1, s2, s3, s4, s5 being Real_Sequence st s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Nat holds

( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) holds

for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))

( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) holds

for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))

proof end;

Lm11: for n being Nat

for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds

(n + 1) -root ((Partial_Product s) . n) > 0

proof end;

Lm12: for n being Nat

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n >= s . (n - 1) ) ) holds

((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0

proof end;

theorem :: SERIES_3:53

for n being Nat

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n >= s . (n - 1) ) ) holds

(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))

for s being Real_Sequence st ( for n being Nat holds

( s . n > 0 & s . n >= s . (n - 1) ) ) holds

(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))

proof end;