Metamath Proof Explorer

Theorem releabs

Description: The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of Gleason p. 133. (Contributed by NM, 1-Apr-2005)

Ref Expression
Assertion releabs 
|- ( A e. CC -> ( Re ` A ) <_ ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
2 1 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
3 abscl 
 |-  ( ( Re ` A ) e. CC -> ( abs ` ( Re ` A ) ) e. RR )
4 2 3 syl 
 |-  ( A e. CC -> ( abs ` ( Re ` A ) ) e. RR )
5 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
6 leabs 
 |-  ( ( Re ` A ) e. RR -> ( Re ` A ) <_ ( abs ` ( Re ` A ) ) )
7 1 6 syl 
 |-  ( A e. CC -> ( Re ` A ) <_ ( abs ` ( Re ` A ) ) )
8 absrele 
 |-  ( A e. CC -> ( abs ` ( Re ` A ) ) <_ ( abs ` A ) )
9 1 4 5 7 8 letrd 
 |-  ( A e. CC -> ( Re ` A ) <_ ( abs ` A ) )