Metamath Proof Explorer

Theorem leabs

Description: A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005)

Ref Expression
Assertion leabs 
|- ( A e. RR -> A <_ ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( A e. RR -> 0 e. RR )
2 id 
 |-  ( A e. RR -> A e. RR )
3 absid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
4 eqcom 
 |-  ( ( abs ` A ) = A <-> A = ( abs ` A ) )
5 eqle 
 |-  ( ( A e. RR /\ A = ( abs ` A ) ) -> A <_ ( abs ` A ) )
6 4 5 sylan2b 
 |-  ( ( A e. RR /\ ( abs ` A ) = A ) -> A <_ ( abs ` A ) )
7 3 6 syldan 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A <_ ( abs ` A ) )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
10 8 9 syl 
 |-  ( A e. RR -> 0 <_ ( abs ` A ) )
11 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
12 8 11 syl 
 |-  ( A e. RR -> ( abs ` A ) e. RR )
13 0re 
 |-  0 e. RR
14 letr 
 |-  ( ( A e. RR /\ 0 e. RR /\ ( abs ` A ) e. RR ) -> ( ( A <_ 0 /\ 0 <_ ( abs ` A ) ) -> A <_ ( abs ` A ) ) )
15 13 14 mp3an2 
 |-  ( ( A e. RR /\ ( abs ` A ) e. RR ) -> ( ( A <_ 0 /\ 0 <_ ( abs ` A ) ) -> A <_ ( abs ` A ) ) )
16 12 15 mpdan 
 |-  ( A e. RR -> ( ( A <_ 0 /\ 0 <_ ( abs ` A ) ) -> A <_ ( abs ` A ) ) )
17 10 16 mpan2d 
 |-  ( A e. RR -> ( A <_ 0 -> A <_ ( abs ` A ) ) )
18 17 imp 
 |-  ( ( A e. RR /\ A <_ 0 ) -> A <_ ( abs ` A ) )
19 1 2 7 18 lecasei 
 |-  ( A e. RR -> A <_ ( abs ` A ) )