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 ) )