Metamath Proof Explorer

Theorem sge0rern

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

Ref Expression
Hypotheses sge0rern.x ⊢ φ → X ∈ V
sge0rern.f ⊢ φ → F : X ⟶ 0 +∞
sge0rern.re ⊢ φ → sum^ ⁡ F ∈ ℝ
Assertion sge0rern ⊢ φ → ¬ +∞ ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 sge0rern.x ⊢ φ → X ∈ V
2 sge0rern.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0rern.re ⊢ φ → sum^ ⁡ F ∈ ℝ
4 1 adantr ⊢ φ ∧ +∞ ∈ ran ⁡ F → X ∈ V
5 2 adantr ⊢ φ ∧ +∞ ∈ ran ⁡ F → F : X ⟶ 0 +∞
6 simpr ⊢ φ ∧ +∞ ∈ ran ⁡ F → +∞ ∈ ran ⁡ F
7 4 5 6 sge0pnfval ⊢ φ ∧ +∞ ∈ ran ⁡ F → sum^ ⁡ F = +∞
8 3 adantr ⊢ φ ∧ +∞ ∈ ran ⁡ F → sum^ ⁡ F ∈ ℝ
9 4 5 sge0repnf ⊢ φ ∧ +∞ ∈ ran ⁡ F → sum^ ⁡ F ∈ ℝ ↔ ¬ sum^ ⁡ F = +∞
10 8 9 mpbid ⊢ φ ∧ +∞ ∈ ran ⁡ F → ¬ sum^ ⁡ F = +∞
11 7 10 pm2.65da ⊢ φ → ¬ +∞ ∈ ran ⁡ F