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

Metamath Proof Explorer

Theorem xrleloe

Description: 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrleloe 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )

Proof

Step Hyp Ref Expression
1 xrlenlt 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
2 xrlttri 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B < A <-> -. ( B = A \/ A < B ) ) )
3 2 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B < A <-> -. ( B = A \/ A < B ) ) )
4 3 con2bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( B = A \/ A < B ) <-> -. B < A ) )
5 eqcom 
 |-  ( B = A <-> A = B )
6 5 orbi1i 
 |-  ( ( B = A \/ A < B ) <-> ( A = B \/ A < B ) )
7 orcom 
 |-  ( ( A = B \/ A < B ) <-> ( A < B \/ A = B ) )
8 6 7 bitri 
 |-  ( ( B = A \/ A < B ) <-> ( A < B \/ A = B ) )
9 4 8 bitr3di 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. B < A <-> ( A < B \/ A = B ) ) )
10 1 9 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )