Metamath Proof Explorer

Theorem mnfltpnf

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

Ref Expression
Assertion mnfltpnf 
|- -oo < +oo

Proof

Step Hyp Ref Expression
1 eqid 
 |-  -oo = -oo
2 eqid 
 |-  +oo = +oo
3 olc 
 |-  ( ( -oo = -oo /\ +oo = +oo ) -> ( ( ( -oo e. RR /\ +oo e. RR ) /\ -oo
4 1 2 3 mp2an 
 |-  ( ( ( -oo e. RR /\ +oo e. RR ) /\ -oo
5 4 orci 
 |-  ( ( ( ( -oo e. RR /\ +oo e. RR ) /\ -oo
6 mnfxr 
 |-  -oo e. RR*
7 pnfxr 
 |-  +oo e. RR*
8 ltxr 
 |-  ( ( -oo e. RR* /\ +oo e. RR* ) -> ( -oo < +oo <-> ( ( ( ( -oo e. RR /\ +oo e. RR ) /\ -oo
9 6 7 8 mp2an 
 |-  ( -oo < +oo <-> ( ( ( ( -oo e. RR /\ +oo e. RR ) /\ -oo
10 5 9 mpbir 
 |-  -oo < +oo