Metamath Proof Explorer

Theorem cosargd

Description: The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses cosargd.1 
|- ( ph -> X e. CC )
cosargd.2 
|- ( ph -> X =/= 0 )
Assertion cosargd 
|- ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( Re ` X ) / ( abs ` X ) ) )

Proof

Step Hyp Ref Expression
1 cosargd.1 
 |-  ( ph -> X e. CC )
2 cosargd.2 
 |-  ( ph -> X =/= 0 )
3 1 cjcld 
 |-  ( ph -> ( * ` X ) e. CC )
4 1 3 addcld 
 |-  ( ph -> ( X + ( * ` X ) ) e. CC )
5 1 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
6 5 recnd 
 |-  ( ph -> ( abs ` X ) e. CC )
7 2cnd 
 |-  ( ph -> 2 e. CC )
8 1 2 absne0d 
 |-  ( ph -> ( abs ` X ) =/= 0 )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( ph -> 2 =/= 0 )
11 4 6 7 8 10 divdiv32d 
 |-  ( ph -> ( ( ( X + ( * ` X ) ) / ( abs ` X ) ) / 2 ) = ( ( ( X + ( * ` X ) ) / 2 ) / ( abs ` X ) ) )
12 1 2 logcld 
 |-  ( ph -> ( log ` X ) e. CC )
13 12 imcld 
 |-  ( ph -> ( Im ` ( log ` X ) ) e. RR )
14 13 recnd 
 |-  ( ph -> ( Im ` ( log ` X ) ) e. CC )
15 cosval 
 |-  ( ( Im ` ( log ` X ) ) e. CC -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) + ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) ) / 2 ) )
16 14 15 syl 
 |-  ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) + ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) ) / 2 ) )
17 efiarg 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) = ( X / ( abs ` X ) ) )
18 1 2 17 syl2anc 
 |-  ( ph -> ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) = ( X / ( abs ` X ) ) )
19 ax-icn 
 |-  _i e. CC
20 19 a1i 
 |-  ( ph -> _i e. CC )
21 20 14 mulcld 
 |-  ( ph -> ( _i x. ( Im ` ( log ` X ) ) ) e. CC )
22 efcj 
 |-  ( ( _i x. ( Im ` ( log ` X ) ) ) e. CC -> ( exp ` ( * ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) = ( * ` ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) )
23 21 22 syl 
 |-  ( ph -> ( exp ` ( * ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) = ( * ` ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) )
24 20 14 cjmuld 
 |-  ( ph -> ( * ` ( _i x. ( Im ` ( log ` X ) ) ) ) = ( ( * ` _i ) x. ( * ` ( Im ` ( log ` X ) ) ) ) )
25 cji 
 |-  ( * ` _i ) = -u _i
26 25 a1i 
 |-  ( ph -> ( * ` _i ) = -u _i )
27 13 cjred 
 |-  ( ph -> ( * ` ( Im ` ( log ` X ) ) ) = ( Im ` ( log ` X ) ) )
28 26 27 oveq12d 
 |-  ( ph -> ( ( * ` _i ) x. ( * ` ( Im ` ( log ` X ) ) ) ) = ( -u _i x. ( Im ` ( log ` X ) ) ) )
29 24 28 eqtrd 
 |-  ( ph -> ( * ` ( _i x. ( Im ` ( log ` X ) ) ) ) = ( -u _i x. ( Im ` ( log ` X ) ) ) )
30 29 fveq2d 
 |-  ( ph -> ( exp ` ( * ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) = ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) )
31 18 fveq2d 
 |-  ( ph -> ( * ` ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) ) = ( * ` ( X / ( abs ` X ) ) ) )
32 23 30 31 3eqtr3d 
 |-  ( ph -> ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) = ( * ` ( X / ( abs ` X ) ) ) )
33 1 6 8 cjdivd 
 |-  ( ph -> ( * ` ( X / ( abs ` X ) ) ) = ( ( * ` X ) / ( * ` ( abs ` X ) ) ) )
34 5 cjred 
 |-  ( ph -> ( * ` ( abs ` X ) ) = ( abs ` X ) )
35 34 oveq2d 
 |-  ( ph -> ( ( * ` X ) / ( * ` ( abs ` X ) ) ) = ( ( * ` X ) / ( abs ` X ) ) )
36 32 33 35 3eqtrd 
 |-  ( ph -> ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) = ( ( * ` X ) / ( abs ` X ) ) )
37 18 36 oveq12d 
 |-  ( ph -> ( ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) + ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) ) = ( ( X / ( abs ` X ) ) + ( ( * ` X ) / ( abs ` X ) ) ) )
38 1 3 6 8 divdird 
 |-  ( ph -> ( ( X + ( * ` X ) ) / ( abs ` X ) ) = ( ( X / ( abs ` X ) ) + ( ( * ` X ) / ( abs ` X ) ) ) )
39 37 38 eqtr4d 
 |-  ( ph -> ( ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) + ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) ) = ( ( X + ( * ` X ) ) / ( abs ` X ) ) )
40 39 oveq1d 
 |-  ( ph -> ( ( ( exp ` ( _i x. ( Im ` ( log ` X ) ) ) ) + ( exp ` ( -u _i x. ( Im ` ( log ` X ) ) ) ) ) / 2 ) = ( ( ( X + ( * ` X ) ) / ( abs ` X ) ) / 2 ) )
41 16 40 eqtrd 
 |-  ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( ( X + ( * ` X ) ) / ( abs ` X ) ) / 2 ) )
42 reval 
 |-  ( X e. CC -> ( Re ` X ) = ( ( X + ( * ` X ) ) / 2 ) )
43 1 42 syl 
 |-  ( ph -> ( Re ` X ) = ( ( X + ( * ` X ) ) / 2 ) )
44 43 oveq1d 
 |-  ( ph -> ( ( Re ` X ) / ( abs ` X ) ) = ( ( ( X + ( * ` X ) ) / 2 ) / ( abs ` X ) ) )
45 11 41 44 3eqtr4d 
 |-  ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( Re ` X ) / ( abs ` X ) ) )