This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℂ → ℜ ⁡ A ≤ A

Proof

Step Hyp Ref Expression
1 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
2 1 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
3 abscl ⊢ ℜ ⁡ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
4 2 3 syl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
5 abscl ⊢ A ∈ ℂ → A ∈ ℝ
6 leabs ⊢ ℜ ⁡ A ∈ ℝ → ℜ ⁡ A ≤ ℜ ⁡ A
7 1 6 syl ⊢ A ∈ ℂ → ℜ ⁡ A ≤ ℜ ⁡ A
8 absrele ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A
9 1 4 5 7 8 letrd ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A