let F1, F2 be Function of NAT,ExtREAL; :: thesis: ( F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable implies F1 is summable )
assume F1 is nonnegative ; :: thesis: ( ex n being Element of NAT st not F1 . n <= F2 . n or not F2 is summable or F1 is summable )
then A1: 0. <= (Ser F1) . 0 by Th59;
(Ser F1) . 0 <= sup (rng (Ser F1)) by FUNCT_2:6, XXREAL_2:4;
then A2: SUM F1 <> -infty by A1, XXREAL_0:2, XXREAL_0:6;
assume A3: for n being Element of NAT holds F1 . n <= F2 . n ; :: thesis: ( not F2 is summable or F1 is summable )
assume F2 is summable ; :: thesis: F1 is summable
then SUM F2 in REAL by Def24;
then A4: not SUM F1 = +infty by A3, Th62, XXREAL_0:9;
( SUM F1 in REAL or SUM F1 in {-infty,+infty} ) by XBOOLE_0:def 3;
hence F1 is summable by A4, A2, Def24, TARSKI:def 2; :: thesis: verum