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 sselid ⊢φ∧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+∞