Metamath Proof Explorer

Theorem xrleid

Description: 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrleid 
|- ( A e. RR* -> A <_ A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 1 olci 
 |-  ( A < A \/ A = A )
3 xrleloe 
 |-  ( ( A e. RR* /\ A e. RR* ) -> ( A <_ A <-> ( A < A \/ A = A ) ) )
4 2 3 mpbiri 
 |-  ( ( A e. RR* /\ A e. RR* ) -> A <_ A )
5 4 anidms 
 |-  ( A e. RR* -> A <_ A )