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	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		recl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
3		abscl	⊢ ( ( ℜ ‘ 𝐴 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
4	2 3	syl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
5		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
6		leabs	⊢ ( ( ℜ ‘ 𝐴 ) ∈ ℝ → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ ( ℜ ‘ 𝐴 ) ) )
7	1 6	syl	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ ( ℜ ‘ 𝐴 ) ) )
8		absrele	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℜ ‘ 𝐴 ) ) ≤ ( abs ‘ 𝐴 ) )
9	1 4 5 7 8	letrd	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ≤ ( abs ‘ 𝐴 ) )