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

Metamath Proof Explorer

Theorem leloe

Description: 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by NM, 13-May-1999)

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

Proof

Step Hyp Ref Expression
1 lenlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
2 axlttri 
 |-  ( ( 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 ) ) )