This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ngtmnft

Description: An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 xrltnr 
 |-  ( -oo e. RR* -> -. -oo < -oo )
3 1 2 ax-mp 
 |-  -. -oo < -oo
4 breq2 
 |-  ( A = -oo -> ( -oo < A <-> -oo < -oo ) )
5 3 4 mtbiri 
 |-  ( A = -oo -> -. -oo < A )
6 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
7 xrleloe 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo <_ A <-> ( -oo < A \/ -oo = A ) ) )
8 1 7 mpan 
 |-  ( A e. RR* -> ( -oo <_ A <-> ( -oo < A \/ -oo = A ) ) )
9 6 8 mpbid 
 |-  ( A e. RR* -> ( -oo < A \/ -oo = A ) )
10 9 ord 
 |-  ( A e. RR* -> ( -. -oo < A -> -oo = A ) )
11 eqcom 
 |-  ( -oo = A <-> A = -oo )
12 10 11 imbitrdi 
 |-  ( A e. RR* -> ( -. -oo < A -> A = -oo ) )
13 5 12 impbid2 
 |-  ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )