:: On the Partial Product of Series and Related Basic Inequalities
:: by Fuguo Ge and Xiquan Liang
::
:: Received July 6, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for x being real number holds x ^2 = x |^ 2
Lm2:
1 |^ 3 = 1
by NEWTON:15;
Lm3:
2 |^ 3 = 8
Lm4:
3 |^ 3 = 27
Lm5:
for x being real number holds (- x) |^ 3 = - (x |^ 3)
Lm6:
for x, y being real number holds (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3)
Lm7:
for x, y being real number holds (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2 ) - (x * y)) + (y ^2 ))
Lm8:
for x, y, z being real number st x ^2 <= y * z holds
abs x <= sqrt (y * z)
theorem :: SERIES_3:1
theorem Th2: :: SERIES_3:2
theorem :: SERIES_3:3
theorem Th4: :: SERIES_3:4
theorem :: SERIES_3:5
theorem Th6: :: SERIES_3:6
theorem Th7: :: SERIES_3:7
theorem Th8: :: SERIES_3:8
theorem Th9: :: SERIES_3:9
theorem Th10: :: SERIES_3:10
theorem :: SERIES_3:11
theorem Th12: :: SERIES_3:12
theorem Th13: :: SERIES_3:13
theorem :: SERIES_3:14
theorem Th15: :: SERIES_3:15
theorem :: SERIES_3:16
theorem :: SERIES_3:17
theorem Th18: :: SERIES_3:18
theorem :: SERIES_3:19
theorem :: SERIES_3:20
theorem :: SERIES_3:21
theorem :: SERIES_3:22
theorem :: SERIES_3:23
theorem :: SERIES_3:24
theorem :: SERIES_3:25
theorem :: SERIES_3:26
theorem :: SERIES_3:27
theorem :: SERIES_3:28
theorem :: SERIES_3:29
theorem :: SERIES_3:30
theorem Th31: :: SERIES_3:31
theorem :: SERIES_3:32
theorem Th33: :: SERIES_3:33
theorem Th34: :: SERIES_3:34
theorem Th35: :: SERIES_3:35
theorem Th36: :: SERIES_3:36
theorem :: SERIES_3:37
theorem Th38: :: SERIES_3:38
theorem :: SERIES_3:39
theorem :: SERIES_3:40
theorem Th41: :: SERIES_3:41
theorem :: SERIES_3:42
:: deftheorem Def1 defines Partial_Product SERIES_3:def 1 :
theorem Th43: :: SERIES_3:43
theorem Th44: :: SERIES_3:44
theorem :: SERIES_3:45
theorem :: SERIES_3:46
theorem :: SERIES_3:47
theorem :: SERIES_3:48
Lm9:
for s being Real_Sequence st ( for n being Element of NAT holds
( s . n > - 1 & s . n < 0 ) ) holds
for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
theorem :: SERIES_3:49
Lm10:
for s being Real_Sequence st ( for n being Element of NAT holds s . n >= 0 ) holds
for n being Element of NAT holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
theorem :: SERIES_3:50
theorem :: SERIES_3:51
Lm11:
for n being Element of NAT
for s, s1, s2 being Real_Sequence st ( for n being Element of NAT holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds
(Partial_Sums s) . n >= 0
theorem :: SERIES_3:52
Lm12:
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) holds
(n + 1) -root ((Partial_Product s) . n) > 0
Lm13:
for n being Element of NAT
for s being Real_Sequence st ( for n being Element of NAT holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0
theorem :: SERIES_3:53