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

Lm1: ( 1 / 1 = 1 & 1 / (- 1) = - 1 )
;

theorem Th1: :: SERIES_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Real_Sequence st 0 < a & a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
proof end;

theorem Th2: :: SERIES_1:2  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 a being real number st a <> 0 holds
(abs a) to_power n = abs (a to_power n)
proof end;

theorem Th3: :: SERIES_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Real_Sequence st abs a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
proof end;

definition
let s be Real_Sequence;
func Partial_Sums s -> Real_Sequence means :Def1: :: SERIES_1: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_Sums SERIES_1:def 1 :
for s, b2 being Real_Sequence holds
( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) );

definition
let s be Real_Sequence;
attr s is summable means :Def2: :: SERIES_1:def 2
Partial_Sums s is convergent;
func Sum s -> Real equals :: SERIES_1:def 3
lim (Partial_Sums s);
correctness
coherence
lim (Partial_Sums s) is Real
;
;
end;

:: deftheorem Def2 defines summable SERIES_1:def 2 :
for s being Real_Sequence holds
( s is summable iff Partial_Sums s is convergent );

:: deftheorem defines Sum SERIES_1:def 3 :
for s being Real_Sequence holds Sum s = lim (Partial_Sums s);

theorem :: SERIES_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SERIES_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SERIES_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: SERIES_1:7  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 s is summable holds
( s is convergent & lim s = 0 )
proof end;

theorem Th8: :: SERIES_1:8  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 holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
proof end;

theorem Th9: :: SERIES_1:9  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 holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
proof end;

theorem :: SERIES_1:10  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 s1 is summable & s2 is summable holds
( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) )
proof end;

theorem :: SERIES_1:11  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 s1 is summable & s2 is summable holds
( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) )
proof end;

theorem Th12: :: SERIES_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)
proof end;

theorem Th13: :: SERIES_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )
proof end;

theorem Th14: :: SERIES_1:14  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 ( for n being Nat holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
proof end;

theorem Th15: :: SERIES_1:15  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 s is summable holds
for n being Nat holds s ^\ n is summable
proof end;

theorem Th16: :: SERIES_1:16  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 ex n being Nat st s ^\ n is summable holds
s is summable
proof end;

theorem Th17: :: SERIES_1:17  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 <= s2 . n ) holds
for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n
proof end;

theorem :: SERIES_1:18  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 s is summable holds
for n being Nat holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))
proof end;

theorem Th19: :: SERIES_1:19  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 0 <= s . n ) holds
Partial_Sums s is non-decreasing
proof end;

theorem Th20: :: SERIES_1:20  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 0 <= s . n ) holds
( Partial_Sums s is bounded_above iff s is summable )
proof end;

theorem :: SERIES_1:21  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 s is summable & ( for n being Nat holds 0 <= s . n ) holds
0 <= Sum s
proof end;

theorem Th22: :: SERIES_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s2, s1 being Real_Sequence st ( for n being Nat holds 0 <= s2 . n ) & s1 is summable & ex m being Nat st
for n being Nat st m <= n holds
s2 . n <= s1 . n holds
s2 is summable
proof end;

theorem :: SERIES_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SERIES_1:24  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
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds
( s1 is summable & Sum s1 <= Sum s2 )
proof end;

theorem Th25: :: SERIES_1:25  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 holds
( s is summable iff for r being real number st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
proof end;

theorem Th26: :: SERIES_1:26  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 a being real number st a <> 1 holds
(Partial_Sums (a GeoSeq )) . n = (1 - (a to_power (n + 1))) / (1 - a)
proof end;

theorem :: SERIES_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds
for n being Nat holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a)
proof end;

theorem Th28: :: SERIES_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st abs a < 1 holds
( a GeoSeq is summable & Sum (a GeoSeq ) = 1 / (1 - a) )
proof end;

theorem :: SERIES_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Real_Sequence st abs a < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0) / (1 - a) )
proof end;

theorem Th30: :: SERIES_1:30  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 ( for n being Nat holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable
proof end;

theorem :: SERIES_1:31  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 ) & ex m being Nat st
for n being Nat st n >= m holds
(s . (n + 1)) / (s . n) >= 1 holds
not s is summable
proof end;

theorem Th32: :: SERIES_1:32  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 ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable
proof end;

theorem Th33: :: SERIES_1:33  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 ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Nat st
for n being Nat st m <= n holds
s1 . n >= 1 holds
not s is summable
proof end;

theorem :: SERIES_1:34  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 ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds
not s is summable
proof end;

definition
let k, n be Nat;
:: original: to_power
redefine func k to_power n -> Nat;
coherence
k to_power n is Nat
proof end;
end;

theorem Th35: :: SERIES_1:35  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 is non-increasing & ( for n being Nat holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) holds
( s is summable iff s1 is summable )
proof end;

theorem :: SERIES_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number
for s being Real_Sequence st p > 1 & ( for n being Nat st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
s is summable
proof end;

theorem :: SERIES_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being real number
for s being Real_Sequence st p <= 1 & ( for n being Nat st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
not s is summable
proof end;

definition
let s be Real_Sequence;
canceled;
attr s is absolutely_summable means :Def5: :: SERIES_1:def 5
abs s is summable;
end;

:: deftheorem SERIES_1:def 4 :
canceled;

:: deftheorem Def5 defines absolutely_summable SERIES_1:def 5 :
for s being Real_Sequence holds
( s is absolutely_summable iff abs s is summable );

theorem :: SERIES_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th39: :: SERIES_1:39  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, m being Nat st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n))
proof end;

theorem :: SERIES_1: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 st s is absolutely_summable holds
s is summable
proof end;

theorem :: SERIES_1:41  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 0 <= s . n ) & s is summable holds
s is absolutely_summable
proof end;

theorem :: SERIES_1:42  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 ( for n being Nat holds
( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is absolutely_summable
proof end;

theorem Th43: :: SERIES_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for s being Real_Sequence st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
abs (s . n) >= r & s is convergent holds
lim s <> 0
proof end;

theorem :: SERIES_1: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 ) & ex m being Nat st
for n being Nat st n >= m holds
((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds
not s is summable
proof end;

theorem :: SERIES_1:45  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 = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 holds
s is absolutely_summable
proof end;

theorem :: SERIES_1:46  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 = n -root ((abs s) . n) ) & ex m being Nat st
for n being Nat st m <= n holds
s1 . n >= 1 holds
not s is summable
proof end;

theorem :: SERIES_1:47  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 = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 holds
not s is summable
proof end;