begin
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
theorem Th2:
theorem
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
theorem
theorem Th18:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem
theorem
theorem Th41:
theorem
:: deftheorem Def1 defines Partial_Product SERIES_3:def 1 :
for s, b2 being Real_Sequence holds
( b2 = Partial_Product s iff ( b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) ) );
theorem Th43:
theorem Th44:
theorem
theorem
theorem
theorem
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
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
theorem
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
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