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

Proof

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