let seq be nonnegative ExtREAL_sequence; :: thesis: ( not Partial_Sums seq is convergent_to_+infty implies for n being Nat holds seq . n is Real )
assume A2: not Partial_Sums seq is convergent_to_+infty ; :: thesis: for n being Nat holds seq . n is Real
given N being Nat such that A3: seq . N is not Real ; :: thesis: contradiction
not seq . N in REAL by A3;
then A4: ( seq . N = +infty or seq . N = -infty ) by XXREAL_0:14;
A6: Partial_Sums seq is non-decreasing by MESFUNC9:16;
now :: thesis: for g being Real st 0 < g holds
ex N being Nat st
for m being Nat st N <= m holds
g <= (Partial_Sums seq) . m
let g be Real; :: thesis: ( 0 < g implies ex N being Nat st
for m being Nat st N <= m holds
g <= (Partial_Sums seq) . m )
assume 0 < g ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
g <= (Partial_Sums seq) . m
take N = N; :: thesis: for m being Nat st N <= m holds
g <= (Partial_Sums seq) . m
hereby :: thesis: verum
let m be Nat; :: thesis: ( N <= m implies g <= (Partial_Sums seq) . b1 )
assume A7: N <= m ; :: thesis: g <= (Partial_Sums seq) . b1
per cases ( N = 0 or N <> 0 ) ;
suppose N <> 0 ; :: thesis: g <= (Partial_Sums seq) . b1
then consider N1 being Nat such that
A11: N = N1 + 1 by NAT_1:6;
A12: (Partial_Sums seq) . N1 >= 0 by SUPINF_2:51;
(Partial_Sums seq) . N = ((Partial_Sums seq) . N1) + (seq . N) by A11, MESFUNC9:def 1
.= +infty by A4, SUPINF_2:51, XXREAL_0:4, A12, XXREAL_3:39 ;
then (Partial_Sums seq) . m = +infty by A6, A7, RINFSUP2:7, XXREAL_0:4;
hence g <= (Partial_Sums seq) . m by XXREAL_0:3; :: thesis: verum
end;
end;
end;
end;
hence contradiction by A2, MESFUNC5:def 9; :: thesis: verum