Theorem sge0repnf

Description: The of nonnegative extended reals is a real number if and only if it is not +oo . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0repnf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0repnf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion	sge0repnf	⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sge0repnf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0repnf.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		renepnf	⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ℝ → ( Σ^ ‘ 𝐹 ) ≠ +∞ )
4	3	neneqd	⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ℝ → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
5	4	a1i	⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ → ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
6		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
7		0xr	⊢ 0 ∈ ℝ*
8	7	a1i	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → 0 ∈ ℝ* )
9		pnfxr	⊢ +∞ ∈ ℝ*
10	9	a1i	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → +∞ ∈ ℝ* )
11	1 2	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
12	11	adantr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
13	1 2	sge0ge0	⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ 𝐹 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → 0 ≤ ( Σ^ ‘ 𝐹 ) )
15		simpr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
16		nltpnft	⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ℝ* → ( ( Σ^ ‘ 𝐹 ) = +∞ ↔ ¬ ( Σ^ ‘ 𝐹 ) < +∞ ) )
17	11 16	syl	⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) = +∞ ↔ ¬ ( Σ^ ‘ 𝐹 ) < +∞ ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ 𝐹 ) = +∞ ↔ ¬ ( Σ^ ‘ 𝐹 ) < +∞ ) )
19	15 18	mtbid	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ¬ ¬ ( Σ^ ‘ 𝐹 ) < +∞ )
20	19	notnotrd	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) < +∞ )
21	8 10 12 14 20	elicod	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,) +∞ ) )
22	6 21	sseldi	⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
23	22	ex	⊢ ( 𝜑 → ( ¬ ( Σ^ ‘ 𝐹 ) = +∞ → ( Σ^ ‘ 𝐹 ) ∈ ℝ ) )
24	5 23	impbid	⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )