Theorem nepnfltpnf

Description: An extended real that is not +oo is less than +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	nepnfltpnf.1	⊢ ( 𝜑 → 𝐴 ≠ +∞ )
	nepnfltpnf.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion	nepnfltpnf	⊢ ( 𝜑 → 𝐴 < +∞ )

Proof

Step	Hyp	Ref	Expression
1		nepnfltpnf.1	⊢ ( 𝜑 → 𝐴 ≠ +∞ )
2		nepnfltpnf.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
3	1	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = +∞ )
4		nltpnft	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) )
5	2 4	syl	⊢ ( 𝜑 → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) )
6	3 5	mtbid	⊢ ( 𝜑 → ¬ ¬ 𝐴 < +∞ )
7		notnotb	⊢ ( 𝐴 < +∞ ↔ ¬ ¬ 𝐴 < +∞ )
8	6 7	sylibr	⊢ ( 𝜑 → 𝐴 < +∞ )