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\in ℂ\to \Re \left(A\right)\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
2	1	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
3		abscl	$$⊢\Re \left(A\right)\in ℂ\to \left|\Re \left(A\right)\right|\in ℝ$$
4	2 3	syl	$$⊢A\in ℂ\to \left|\Re \left(A\right)\right|\in ℝ$$
5		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
6		leabs	$$⊢\Re \left(A\right)\in ℝ\to \Re \left(A\right)\le \left|\Re \left(A\right)\right|$$
7	1 6	syl	$$⊢A\in ℂ\to \Re \left(A\right)\le \left|\Re \left(A\right)\right|$$
8		absrele	$$⊢A\in ℂ\to \left|\Re \left(A\right)\right|\le \left|A\right|$$
9	1 4 5 7 8	letrd	$$⊢A\in ℂ\to \Re \left(A\right)\le \left|A\right|$$