Metamath Proof Explorer

Theorem pnfnlt

Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 pnfnre 
 |-  +oo e/ RR
2 1 neli 
 |-  -. +oo e. RR
3 2 intnanr 
 |-  -. ( +oo e. RR /\ A e. RR )
4 3 intnanr 
 |-  -. ( ( +oo e. RR /\ A e. RR ) /\ +oo
5 pnfnemnf 
 |-  +oo =/= -oo
6 5 neii 
 |-  -. +oo = -oo
7 6 intnanr 
 |-  -. ( +oo = -oo /\ A = +oo )
8 4 7 pm3.2ni 
 |-  -. ( ( ( +oo e. RR /\ A e. RR ) /\ +oo
9 2 intnanr 
 |-  -. ( +oo e. RR /\ A = +oo )
10 6 intnanr 
 |-  -. ( +oo = -oo /\ A e. RR )
11 9 10 pm3.2ni 
 |-  -. ( ( +oo e. RR /\ A = +oo ) \/ ( +oo = -oo /\ A e. RR ) )
12 8 11 pm3.2ni 
 |-  -. ( ( ( ( +oo e. RR /\ A e. RR ) /\ +oo
13 pnfxr 
 |-  +oo e. RR*
14 ltxr 
 |-  ( ( +oo e. RR* /\ A e. RR* ) -> ( +oo < A <-> ( ( ( ( +oo e. RR /\ A e. RR ) /\ +oo
15 13 14 mpan 
 |-  ( A e. RR* -> ( +oo < A <-> ( ( ( ( +oo e. RR /\ A e. RR ) /\ +oo
16 12 15 mtbiri 
 |-  ( A e. RR* -> -. +oo < A )