Theorem absimle

Description: The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absimle	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negicn	⊢ - i ∈ ℂ
2	1	a1i	⊢ ( 𝐴 ∈ ℂ → - i ∈ ℂ )
3		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
4	2 3	mulcld	⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
5		absrele	⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ ( - i · 𝐴 ) ) ) ≤ ( abs ‘ ( - i · 𝐴 ) ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℜ ‘ ( - i · 𝐴 ) ) ) ≤ ( abs ‘ ( - i · 𝐴 ) ) )
7		imre	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ℜ ‘ ( - i · 𝐴 ) ) )
8	7	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝐴 ) ) = ( abs ‘ ( ℜ ‘ ( - i · 𝐴 ) ) ) )
9		absmul	⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( - i · 𝐴 ) ) = ( ( abs ‘ - i ) · ( abs ‘ 𝐴 ) ) )
10	1 9	mpan	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( - i · 𝐴 ) ) = ( ( abs ‘ - i ) · ( abs ‘ 𝐴 ) ) )
11		ax-icn	⊢ i ∈ ℂ
12		absneg	⊢ ( i ∈ ℂ → ( abs ‘ - i ) = ( abs ‘ i ) )
13	11 12	ax-mp	⊢ ( abs ‘ - i ) = ( abs ‘ i )
14		absi	⊢ ( abs ‘ i ) = 1
15	13 14	eqtri	⊢ ( abs ‘ - i ) = 1
16	15	oveq1i	⊢ ( ( abs ‘ - i ) · ( abs ‘ 𝐴 ) ) = ( 1 · ( abs ‘ 𝐴 ) )
17		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
18	17	recnd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℂ )
19	18	mulid2d	⊢ ( 𝐴 ∈ ℂ → ( 1 · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
20	16 19	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ - i ) · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
21	10 20	eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( abs ‘ ( - i · 𝐴 ) ) )
22	6 8 21	3brtr4d	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ 𝐴 ) )