Metamath Proof Explorer

Theorem ltpnf

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion ltpnf 
|- ( A e. RR -> A < +oo )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  +oo = +oo
2 orc 
 |-  ( ( A e. RR /\ +oo = +oo ) -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
3 1 2 mpan2 
 |-  ( A e. RR -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
4 3 olcd 
 |-  ( A e. RR -> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A
5 rexr 
 |-  ( A e. RR -> A e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 ltxr 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A < +oo <-> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A
8 5 6 7 sylancl 
 |-  ( A e. RR -> ( A < +oo <-> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A
9 4 8 mpbird 
 |-  ( A e. RR -> A < +oo )