begin
Lm1:
for x, y being real number holds (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2 ) + (x * y)) + (y ^2 ))
Lm2:
for a, b being real positive number holds 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b)
Lm3:
for x, y, z being real number holds ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z)
Lm4:
for a, c being real positive number
for b being real number holds (a / c) to_power (- b) = (c / a) to_power b
Lm5:
for a, b, c, d being real positive number holds (((sqrt (a * b)) ^2 ) + ((sqrt (c * d)) ^2 )) * (((sqrt (a * c)) ^2 ) + ((sqrt (b * d)) ^2 )) >= (b * c) * ((a + d) ^2 )
Lm6:
for x, y, z being real number holds ((x + y) + z) ^2 = (((((x ^2 ) + (y ^2 )) + (z ^2 )) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x)
;
Lm7:
for x being real number st abs x < 1 holds
x ^2 < 1
Lm8:
for x being real number st x ^2 < 1 holds
abs x < 1
Lm9:
for a, b, c being real positive number holds (((((((2 * (a ^2 )) * (sqrt (b * c))) * 2) * (b ^2 )) * (sqrt (a * c))) * 2) * (c ^2 )) * (sqrt (a * b)) = (((2 * a) * b) * c) |^ 3
Lm10:
for a, b being real positive number holds sqrt (((a ^2 ) + (a * b)) + (b ^2 )) = (1 / 2) * (sqrt ((4 * ((a ^2 ) + (b ^2 ))) + ((4 * a) * b)))
Lm11:
for a, b being real positive number holds sqrt (((a ^2 ) + (a * b)) + (b ^2 )) >= ((1 / 2) * (sqrt 3)) * (a + b)
Lm12:
for a, b being real positive number holds sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3) <= sqrt (((a ^2 ) + (b ^2 )) / 2)
Lm13:
for b, c, a being real positive number holds (((b * c) / a) ^2 ) + (((c * a) / b) ^2 ) >= 2 * (c ^2 )
Lm14:
for b, c, a being real positive number holds ((b * c) / a) * ((c * a) / b) = c ^2
Lm15:
for b, c, a being real positive number holds (((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)) = 2 * (((a ^2 ) + (b ^2 )) + (c ^2 ))
Lm16:
for b, c, a being real positive number holds ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2 ) + (((a * b) / c) ^2 )) + (((b * c) / a) ^2 )) + (2 * (((a ^2 ) + (b ^2 )) + (c ^2 )))
Lm17:
for a, b, c being real positive number st (a + b) + c = 1 holds
(1 / a) - 1 = (b + c) / a
Lm18:
for b, c, a being real positive number holds (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) = 8
Lm19:
for a, b, c being real positive number st (a + b) + c = 1 holds
1 + (1 / a) = 2 + ((b + c) / a)
Lm20:
for a, c, b being real positive number holds (1 + ((sqrt (a * c)) / b)) * ((sqrt (a * b)) / c) = ((sqrt (a * b)) / c) + (a / (sqrt (b * c)))
Lm21:
for b, c, a being real positive number holds (((sqrt (b * c)) / a) + (c / (sqrt (b * a)))) * ((sqrt (a * b)) / c) = (b / (sqrt (a * c))) + 1
Lm22:
for b, c, a being real positive number holds ((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)) = (((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)
Lm23:
for a, c, b being real positive number holds ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6
theorem
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th20:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th29:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th48:
theorem
theorem Th50:
theorem
theorem Th52:
theorem
theorem
theorem
theorem
theorem