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 
|- ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )

Proof

Step Hyp Ref Expression
1 negicn 
 |-  -u _i e. CC
2 1 a1i 
 |-  ( A e. CC -> -u _i e. CC )
3 id 
 |-  ( A e. CC -> A e. CC )
4 2 3 mulcld 
 |-  ( A e. CC -> ( -u _i x. A ) e. CC )
5 absrele 
 |-  ( ( -u _i x. A ) e. CC -> ( abs ` ( Re ` ( -u _i x. A ) ) ) <_ ( abs ` ( -u _i x. A ) ) )
6 4 5 syl 
 |-  ( A e. CC -> ( abs ` ( Re ` ( -u _i x. A ) ) ) <_ ( abs ` ( -u _i x. A ) ) )
7 imre 
 |-  ( A e. CC -> ( Im ` A ) = ( Re ` ( -u _i x. A ) ) )
8 7 fveq2d 
 |-  ( A e. CC -> ( abs ` ( Im ` A ) ) = ( abs ` ( Re ` ( -u _i x. A ) ) ) )
9 absmul 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( abs ` ( -u _i x. A ) ) = ( ( abs ` -u _i ) x. ( abs ` A ) ) )
10 1 9 mpan 
 |-  ( A e. CC -> ( abs ` ( -u _i x. A ) ) = ( ( abs ` -u _i ) x. ( abs ` A ) ) )
11 ax-icn 
 |-  _i e. CC
12 absneg 
 |-  ( _i e. CC -> ( abs ` -u _i ) = ( abs ` _i ) )
13 11 12 ax-mp 
 |-  ( abs ` -u _i ) = ( abs ` _i )
14 absi 
 |-  ( abs ` _i ) = 1
15 13 14 eqtri 
 |-  ( abs ` -u _i ) = 1
16 15 oveq1i 
 |-  ( ( abs ` -u _i ) x. ( abs ` A ) ) = ( 1 x. ( abs ` A ) )
17 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
18 17 recnd 
 |-  ( A e. CC -> ( abs ` A ) e. CC )
19 18 mullidd 
 |-  ( A e. CC -> ( 1 x. ( abs ` A ) ) = ( abs ` A ) )
20 16 19 eqtrid 
 |-  ( A e. CC -> ( ( abs ` -u _i ) x. ( abs ` A ) ) = ( abs ` A ) )
21 10 20 eqtr2d 
 |-  ( A e. CC -> ( abs ` A ) = ( abs ` ( -u _i x. A ) ) )
22 6 8 21 3brtr4d 
 |-  ( A e. CC -> ( abs ` ( Im ` A ) ) <_ ( abs ` A ) )