Metamath Proof Explorer


Theorem sge0rernmpt

Description: If the sum of nonnegative extended reals is not +oo then no term is +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0rernmpt.xph x φ
sge0rernmpt.a φ A V
sge0rernmpt.b φ x A B 0 +∞
sge0rernmpt.re φ sum^ x A B
Assertion sge0rernmpt φ x A B 0 +∞

Proof

Step Hyp Ref Expression
1 sge0rernmpt.xph x φ
2 sge0rernmpt.a φ A V
3 sge0rernmpt.b φ x A B 0 +∞
4 sge0rernmpt.re φ sum^ x A B
5 0xr 0 *
6 5 a1i φ x A 0 *
7 pnfxr +∞ *
8 7 a1i φ x A +∞ *
9 iccssxr 0 +∞ *
10 9 3 sseldi φ x A B *
11 iccgelb 0 * +∞ * B 0 +∞ 0 B
12 6 8 3 11 syl3anc φ x A 0 B
13 simpr φ x A ¬ B < +∞ ¬ B < +∞
14 nltpnft B * B = +∞ ¬ B < +∞
15 10 14 syl φ x A B = +∞ ¬ B < +∞
16 15 adantr φ x A ¬ B < +∞ B = +∞ ¬ B < +∞
17 13 16 mpbird φ x A ¬ B < +∞ B = +∞
18 17 eqcomd φ x A ¬ B < +∞ +∞ = B
19 simpr φ x A x A
20 eqid x A B = x A B
21 20 elrnmpt1 x A B 0 +∞ B ran x A B
22 19 3 21 syl2anc φ x A B ran x A B
23 22 adantr φ x A ¬ B < +∞ B ran x A B
24 18 23 eqeltrd φ x A ¬ B < +∞ +∞ ran x A B
25 1 3 20 fmptdf φ x A B : A 0 +∞
26 2 25 4 sge0rern φ ¬ +∞ ran x A B
27 26 ad2antrr φ x A ¬ B < +∞ ¬ +∞ ran x A B
28 24 27 condan φ x A B < +∞
29 6 8 10 12 28 elicod φ x A B 0 +∞