:: SERIES_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let x be real number ;
cluster abs x -> non negative ;
coherence
not abs x is negative
by COMPLEX1:132;
end;

Lm1: for x being real number holds x ^2 = x |^ 2
proof end;

Lm2: 1 |^ 3 = 1
by NEWTON:15;

Lm3: 2 |^ 3 = 8
proof end;

Lm4: 3 |^ 3 = 27
proof end;

Lm5: for x being real number holds (- x) |^ 3 = - (x |^ 3)
proof end;

Lm6: for x, y being real number holds (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3)
proof end;

Lm7: for x, y being real number holds (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2 ) - (x * y)) + (y ^2 ))
proof end;

Lm8: for x, y, z being real number st x ^2 <= y * z holds
abs x <= sqrt (y * z)
proof end;

theorem :: SERIES_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, m being real number st y > x & x >= 0 & m >= 0 holds
x / y <= (x + m) / (y + m)
proof end;

theorem Th2: :: SERIES_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number holds (a + b) / 2 >= sqrt (a * b)
proof end;

theorem :: SERIES_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b, a being real positive number holds (b / a) + (a / b) >= 2
proof end;

theorem Th4: :: SERIES_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds ((x + y) / 2) ^2 >= x * y
proof end;

theorem :: SERIES_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds ((x ^2 ) + (y ^2 )) / 2 >= ((x + y) / 2) ^2
proof end;

theorem Th6: :: SERIES_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds (x ^2 ) + (y ^2 ) >= (2 * x) * y
proof end;

theorem Th7: :: SERIES_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds ((x ^2 ) + (y ^2 )) / 2 >= x * y
proof end;

theorem Th8: :: SERIES_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds (x ^2 ) + (y ^2 ) >= (2 * (abs x)) * (abs y)
proof end;

theorem Th9: :: SERIES_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds (x + y) ^2 >= (4 * x) * y
proof end;

theorem Th10: :: SERIES_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number holds ((x ^2 ) + (y ^2 )) + (z ^2 ) >= ((x * y) + (y * z)) + (x * z)
proof end;

theorem :: SERIES_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number holds ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z))
proof end;

theorem Th12: :: SERIES_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number holds ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c
proof end;

theorem Th13: :: SERIES_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number holds (((a |^ 3) + (b |^ 3)) + (c |^ 3)) / 3 >= (a * b) * c
proof end;

theorem :: SERIES_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number holds (((a / b) |^ 3) + ((b / c) |^ 3)) + ((c / a) |^ 3) >= ((b / a) + (c / b)) + (a / c)
proof end;

theorem Th15: :: SERIES_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number holds (a + b) + c >= 3 * (3 -root ((a * b) * c))
proof end;

theorem :: SERIES_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number holds ((a + b) + c) / 3 >= 3 -root ((a * b) * c)
proof end;

theorem :: SERIES_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number st (x + y) + z = 1 holds
((x * y) + (y * z)) + (x * z) <= 1 / 3
proof end;

theorem Th18: :: SERIES_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x + y = 1 holds
x * y <= 1 / 4
proof end;

theorem :: SERIES_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x + y = 1 holds
(x ^2 ) + (y ^2 ) >= 1 / 2
proof end;

theorem :: SERIES_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number st a + b = 1 holds
(1 + (1 / a)) * (1 + (1 / b)) >= 9
proof end;

theorem :: SERIES_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st x + y = 1 holds
(x |^ 3) + (y |^ 3) >= 1 / 4
proof end;

theorem :: SERIES_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number st a + b = 1 holds
(a |^ 3) + (b |^ 3) < 1
proof end;

theorem :: SERIES_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number st a + b = 1 holds
(a + (1 / a)) * (b + (1 / b)) >= 25 / 4
proof end;

theorem :: SERIES_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real positive number
for x being real number st abs x <= a holds
x ^2 <= a ^2
proof end;

theorem :: SERIES_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real positive number
for x being real number st abs x >= a holds
x ^2 >= a ^2
proof end;

theorem :: SERIES_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number holds abs ((abs x) - (abs y)) <= (abs x) + (abs y)
proof end;

theorem :: SERIES_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number st (a * b) * c = 1 holds
((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c)
proof end;

theorem :: SERIES_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number st x > 0 & y > 0 & z < 0 & (x + y) + z = 0 holds
(((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 )
proof end;

theorem :: SERIES_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number st a >= 1 holds
(a to_power b) + (a to_power c) >= 2 * (a to_power (sqrt (b * c)))
proof end;

theorem :: SERIES_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real positive number st a >= b & b >= c holds
((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)
proof end;

theorem Th31: :: SERIES_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number
for n being Nat holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)
proof end;

theorem :: SERIES_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real positive number
for n being Nat holds ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n
proof end;

theorem Th33: :: SERIES_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
for n being Nat holds (Partial_Sums s) . n > 0
proof end;

theorem Th34: :: SERIES_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds
for n being Nat holds (Partial_Sums s) . n >= 0
proof end;

theorem Th35: :: SERIES_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n < 0 ) holds
(Partial_Sums s) . n < 0
proof end;

theorem Th36: :: SERIES_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, s1 being Real_Sequence st s = s1 (#) s1 holds
for n being Nat holds (Partial_Sums s) . n >= 0
proof end;

theorem Th37: :: SERIES_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n > s . (n - 1) ) ) holds
(n + 1) * (s . (n + 1)) > (Partial_Sums s) . n
proof end;

theorem :: SERIES_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 ) ) holds
for n being Nat holds (Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)
proof end;

theorem :: SERIES_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s, s1, s2 being Real_Sequence st s = s1 (#) s2 & ( for n being Nat holds
( s1 . n < 0 & s2 . n < 0 ) ) holds
(Partial_Sums s) . n <= ((Partial_Sums s1) . n) * ((Partial_Sums s2) . n)
proof end;

theorem Th40: :: SERIES_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence
for n being Nat holds abs ((Partial_Sums s) . n) <= (Partial_Sums (abs s)) . n
proof end;

theorem :: SERIES_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence holds (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n
proof end;

definition
let s be Real_Sequence;
func Partial_Product s -> Real_Sequence means :Def1: :: SERIES_3:def 1
( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) * (s . (n + 1)) ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being Real_Sequence st b1 . 0 = s . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) * (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: 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 Nat holds b2 . (n + 1) = (b2 . n) * (s . (n + 1)) ) ) );

theorem Th42: :: SERIES_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
(Partial_Product s) . n > 0
proof end;

theorem Th43: :: SERIES_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds
(Partial_Product s) . n >= 0
proof end;

theorem :: SERIES_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n < 1 ) ) holds
for n being Nat holds
( (Partial_Product s) . n > 0 & (Partial_Product s) . n < 1 )
proof end;

theorem :: SERIES_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence st ( for n being Nat holds s . n >= 1 ) holds
for n being Nat holds (Partial_Product s) . n >= 1
proof end;

theorem :: SERIES_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being Real_Sequence st ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 ) ) holds
for n being Nat holds ((Partial_Product s1) . n) + ((Partial_Product s2) . n) <= (Partial_Product (s1 + s2)) . n
proof end;

theorem :: SERIES_3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n = ((2 * n) + 1) / ((2 * n) + 2) ) holds
(Partial_Product s) . n <= 1 / (sqrt ((3 * n) + 4))
proof end;

Lm9: for s being Real_Sequence st ( for n being Nat holds
( s . n > - 1 & s . n < 0 ) ) holds
for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
proof end;

theorem :: SERIES_3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s being Real_Sequence st ( for n being Nat holds
( s1 . n = 1 + (s . n) & s . n > - 1 & s . n < 0 ) ) holds
for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n
proof end;

Lm10: for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds
for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
proof end;

theorem :: SERIES_3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s being Real_Sequence st ( for n being Nat holds
( s1 . n = 1 + (s . n) & s . n >= 0 ) ) holds
for n being Nat holds 1 + ((Partial_Sums s) . n) <= (Partial_Product s1) . n
proof end;

theorem :: SERIES_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s3, s1, s2, s4, s5 being Real_Sequence st s3 = s1 (#) s2 & s4 = s1 (#) s1 & s5 = s2 (#) s2 holds
for n being Nat holds ((Partial_Sums s3) . n) ^2 <= ((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)
proof end;

Lm11: for n being Nat
for s, s1, s2 being Real_Sequence st ( for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds
(Partial_Sums s) . n >= 0
proof end;

theorem :: SERIES_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s4, s1, s5, s2, s3 being Real_Sequence st s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) holds
for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
proof end;

Lm12: for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
(n + 1) -root ((Partial_Product s) . n) > 0
proof end;

Lm13: for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n > s . (n - 1) ) ) holds
((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) > 0
proof end;

theorem :: SERIES_3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n > s . (n - 1) ) ) holds
(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))
proof end;