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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0rern.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	sge0rern.re	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
Assertion	sge0rern	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		sge0rern.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0rern.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		sge0rern.re	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
4	1	adantr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝑋 ∈ 𝑉 )
5	2	adantr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6		simpr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
7	4 5 6	sge0pnfval	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) = +∞ )
8	3	adantr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
9	4 5	sge0repnf	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
10	8 9	mpbid	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
11	7 10	pm2.65da	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )