begin
Lm1:
for x being real number holds x ^2 = x |^ 2
Lm2:
1 |^ 3 = 1
by NEWTON:10;
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)
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
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
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
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