let F be sequence of ExtREAL; :: thesis: ( F is nonnegative & ex n being Element of NAT st F . n = +infty implies SUM F = +infty )

assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds not F . n = +infty or SUM F = +infty )

given n being Element of NAT such that A2: F . n = +infty ; :: thesis: SUM F = +infty

A3: ( ex k being Nat st n = k + 1 implies SUM F = +infty )

assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds not F . n = +infty or SUM F = +infty )

given n being Element of NAT such that A2: F . n = +infty ; :: thesis: SUM F = +infty

A3: ( ex k being Nat st n = k + 1 implies SUM F = +infty )

proof

( n = 0 implies SUM F = +infty )
given k being Nat such that A4:
n = k + 1
; :: thesis: SUM F = +infty

reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider y = (Ser F) . k as R_eal ;

reconsider x = (Ser F) . (k + 1) as R_eal ;

A5: (Ser F) . (k + 1) = y + (F . (k + 1)) by Def11;

(Ser F) . k <> -infty by A1, Th39, XXREAL_0:6;

then A6: x = +infty by A2, A4, A5, XXREAL_3:def 2;

then x is UpperBound of rng (Ser F) by XXREAL_2:41;

hence SUM F = +infty by A6, FUNCT_2:4, XXREAL_2:55; :: thesis: verum

end;reconsider k = k as Element of NAT by ORDINAL1:def 12;

reconsider y = (Ser F) . k as R_eal ;

reconsider x = (Ser F) . (k + 1) as R_eal ;

A5: (Ser F) . (k + 1) = y + (F . (k + 1)) by Def11;

(Ser F) . k <> -infty by A1, Th39, XXREAL_0:6;

then A6: x = +infty by A2, A4, A5, XXREAL_3:def 2;

then x is UpperBound of rng (Ser F) by XXREAL_2:41;

hence SUM F = +infty by A6, FUNCT_2:4, XXREAL_2:55; :: thesis: verum

proof

hence
SUM F = +infty
by A3, NAT_1:6; :: thesis: verum
reconsider x = (Ser F) . 0 as R_eal ;

assume n = 0 ; :: thesis: SUM F = +infty

then A7: (Ser F) . 0 = +infty by A2, Def11;

then x is UpperBound of rng (Ser F) by XXREAL_2:41;

hence SUM F = +infty by A7, FUNCT_2:4, XXREAL_2:55; :: thesis: verum

end;assume n = 0 ; :: thesis: SUM F = +infty

then A7: (Ser F) . 0 = +infty by A2, Def11;

then x is UpperBound of rng (Ser F) by XXREAL_2:41;

hence SUM F = +infty by A7, FUNCT_2:4, XXREAL_2:55; :: thesis: verum