:: On the Partial Product and Partial Sum of Series and Related BasicInequalities
:: by Fuguo Ge and Xiquan Liang
::
:: Received November 23, 2005
:: Copyright (c) 2005 Association of Mizar Users
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 :: SERIES_5:1
theorem :: SERIES_5:2
theorem Th3: :: SERIES_5:3
theorem Th4: :: SERIES_5:4
theorem Th5: :: SERIES_5:5
theorem :: SERIES_5:6
theorem Th7: :: SERIES_5:7
theorem Th8: :: SERIES_5:8
theorem :: SERIES_5:9
theorem Th10: :: SERIES_5:10
theorem :: SERIES_5:11
theorem :: SERIES_5:12
theorem :: SERIES_5:13
theorem :: SERIES_5:14
theorem :: SERIES_5:15
theorem :: SERIES_5:16
theorem :: SERIES_5:17
theorem :: SERIES_5:18
theorem :: SERIES_5:19
theorem Th20: :: SERIES_5:20
theorem :: SERIES_5:21
theorem :: SERIES_5:22
theorem :: SERIES_5:23
theorem :: SERIES_5:24
theorem :: SERIES_5:25
theorem :: SERIES_5:26
theorem :: SERIES_5:27
theorem :: SERIES_5:28
theorem Th29: :: SERIES_5:29
theorem :: SERIES_5:30
theorem :: SERIES_5:31
theorem :: SERIES_5:32
theorem :: SERIES_5:33
theorem :: SERIES_5:34
theorem :: SERIES_5:35
theorem :: SERIES_5:36
theorem :: SERIES_5:37
theorem :: SERIES_5:38
theorem :: SERIES_5:39
theorem :: SERIES_5:40
theorem :: SERIES_5:41
theorem :: SERIES_5:42
theorem :: SERIES_5:43
theorem :: SERIES_5:44
theorem :: SERIES_5:45
theorem :: SERIES_5:46
theorem :: SERIES_5:47
theorem Th48: :: SERIES_5:48
theorem :: SERIES_5:49
theorem Th50: :: SERIES_5:50
theorem :: SERIES_5:51
theorem Th52: :: SERIES_5:52
theorem :: SERIES_5:53
theorem :: SERIES_5:54
theorem :: SERIES_5:55
theorem :: SERIES_5:56
theorem :: SERIES_5:57