Theorem sge0repnfmpt

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

	Ref	Expression
Hypotheses	sge0repnfmpt.k	⊢ Ⅎ 𝑘 𝜑
	sge0repnfmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0repnfmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion	sge0repnfmpt	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sge0repnfmpt.k	⊢ Ⅎ 𝑘 𝜑
2		sge0repnfmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0repnfmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
5	1 3 4	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
6	2 5	sge0repnf	⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) )