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

Metamath Proof Explorer

Theorem absrele

Description: The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005)

Ref Expression
Assertion absrele ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A

Proof

Step Hyp Ref Expression
1 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
2 1 sqge0d ⊢ A ∈ ℂ → 0 ≤ ℑ ⁡ A 2
3 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
4 3 resqcld ⊢ A ∈ ℂ → ℜ ⁡ A 2 ∈ ℝ
5 1 resqcld ⊢ A ∈ ℂ → ℑ ⁡ A 2 ∈ ℝ
6 4 5 addge01d ⊢ A ∈ ℂ → 0 ≤ ℑ ⁡ A 2 ↔ ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
7 2 6 mpbid ⊢ A ∈ ℂ → ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
8 3 sqge0d ⊢ A ∈ ℂ → 0 ≤ ℜ ⁡ A 2
9 4 5 readdcld ⊢ A ∈ ℂ → ℜ ⁡ A 2 + ℑ ⁡ A 2 ∈ ℝ
10 4 5 8 2 addge0d ⊢ A ∈ ℂ → 0 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
11 sqrtle ⊢ ℜ ⁡ A 2 ∈ ℝ ∧ 0 ≤ ℜ ⁡ A 2 ∧ ℜ ⁡ A 2 + ℑ ⁡ A 2 ∈ ℝ ∧ 0 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2 → ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2 ↔ ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
12 4 8 9 10 11 syl22anc ⊢ A ∈ ℂ → ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2 ↔ ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
13 7 12 mpbid ⊢ A ∈ ℂ → ℜ ⁡ A 2 ≤ ℜ ⁡ A 2 + ℑ ⁡ A 2
14 absre ⊢ ℜ ⁡ A ∈ ℝ → ℜ ⁡ A = ℜ ⁡ A 2
15 3 14 syl ⊢ A ∈ ℂ → ℜ ⁡ A = ℜ ⁡ A 2
16 absval2 ⊢ A ∈ ℂ → A = ℜ ⁡ A 2 + ℑ ⁡ A 2
17 13 15 16 3brtr4d ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A