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

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 mullidd ⊢ ( 𝐴 ∈ ℂ → ( 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 ‘ 𝐴 ) )