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	|- ( ph -> A =/= +oo )
	nepnfltpnf.2	|- ( ph -> A e. RR* )
Assertion	nepnfltpnf	|- ( ph -> A < +oo )

Proof

Step	Hyp	Ref	Expression
1		nepnfltpnf.1	|- ( ph -> A =/= +oo )
2		nepnfltpnf.2	|- ( ph -> A e. RR* )
3	1	neneqd	|- ( ph -> -. A = +oo )
4		nltpnft	|- ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
5	2 4	syl	|- ( ph -> ( A = +oo <-> -. A < +oo ) )
6	3 5	mtbid	|- ( ph -> -. -. A < +oo )
7		notnotb	|- ( A < +oo <-> -. -. A < +oo )
8	6 7	sylibr	|- ( ph -> A < +oo )