Metamath Proof Explorer


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 eqtrid ( 𝐴 ∈ ℂ → ( ( abs ‘ - i ) · ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
21 10 20 eqtr2d ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( abs ‘ ( - i · 𝐴 ) ) )
22 6 8 21 3brtr4d ( 𝐴 ∈ ℂ → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ 𝐴 ) )