Metamath Proof Explorer

Theorem nltmnf

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

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

Proof

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