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	$$⊢\phi \to A\ne \mathrm{+\infty }$$
	nepnfltpnf.2	$$⊢\phi \to A\in {ℝ}^{*}$$
Assertion	nepnfltpnf	$$⊢\phi \to A<\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		nepnfltpnf.1	$$⊢\phi \to A\ne \mathrm{+\infty }$$
2		nepnfltpnf.2	$$⊢\phi \to A\in {ℝ}^{*}$$
3	1	neneqd	$$⊢\phi \to \neg A=\mathrm{+\infty }$$
4		nltpnft	$$⊢A\in {ℝ}^{*}\to \left(A=\mathrm{+\infty }\leftrightarrow \neg A<\mathrm{+\infty }\right)$$
5	2 4	syl	$$⊢\phi \to \left(A=\mathrm{+\infty }\leftrightarrow \neg A<\mathrm{+\infty }\right)$$
6	3 5	mtbid	$$⊢\phi \to \neg \neg A<\mathrm{+\infty }$$
7		notnotb	$$⊢A<\mathrm{+\infty }\leftrightarrow \neg \neg A<\mathrm{+\infty }$$
8	6 7	sylibr	$$⊢\phi \to A<\mathrm{+\infty }$$