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 ‘ 𝐴 ) )