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 +∞