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 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
cosargd.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion cosargd ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cosargd.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2 cosargd.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3 1 cjcld ⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ∈ ℂ )
4 1 3 addcld ⊢ ( 𝜑 → ( 𝑋 + ( ∗ ‘ 𝑋 ) ) ∈ ℂ )
5 1 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
7 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
8 1 2 absne0d ⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≠ 0 )
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
11 4 6 7 8 10 divdiv32d ⊢ ( 𝜑 → ( ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / ( abs ‘ 𝑋 ) ) / 2 ) = ( ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / 2 ) / ( abs ‘ 𝑋 ) ) )
12 1 2 logcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )
13 12 imcld ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ )
14 13 recnd ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℂ )
15 cosval ⊢ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℂ → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) + ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) / 2 ) )
16 14 15 syl ⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) + ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) / 2 ) )
17 efiarg ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( 𝑋 / ( abs ‘ 𝑋 ) ) )
18 1 2 17 syl2anc ⊢ ( 𝜑 → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( 𝑋 / ( abs ‘ 𝑋 ) ) )
19 ax-icn ⊢ i ∈ ℂ
20 19 a1i ⊢ ( 𝜑 → i ∈ ℂ )
21 20 14 mulcld ⊢ ( 𝜑 → ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ∈ ℂ )
22 efcj ⊢ ( ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ∈ ℂ → ( exp ‘ ( ∗ ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( ∗ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) )
23 21 22 syl ⊢ ( 𝜑 → ( exp ‘ ( ∗ ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( ∗ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) )
24 20 14 cjmuld ⊢ ( 𝜑 → ( ∗ ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) )
25 cji ⊢ ( ∗ ‘ i ) = - i
26 25 a1i ⊢ ( 𝜑 → ( ∗ ‘ i ) = - i )
27 13 cjred ⊢ ( 𝜑 → ( ∗ ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ℑ ‘ ( log ‘ 𝑋 ) ) )
28 26 27 oveq12d ⊢ ( 𝜑 → ( ( ∗ ‘ i ) · ( ∗ ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) )
29 24 28 eqtrd ⊢ ( 𝜑 → ( ∗ ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( exp ‘ ( ∗ ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) )
31 18 fveq2d ⊢ ( 𝜑 → ( ∗ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( ∗ ‘ ( 𝑋 / ( abs ‘ 𝑋 ) ) ) )
32 23 30 31 3eqtr3d ⊢ ( 𝜑 → ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( ∗ ‘ ( 𝑋 / ( abs ‘ 𝑋 ) ) ) )
33 1 6 8 cjdivd ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑋 / ( abs ‘ 𝑋 ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( ∗ ‘ ( abs ‘ 𝑋 ) ) ) )
34 5 cjred ⊢ ( 𝜑 → ( ∗ ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
35 34 oveq2d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑋 ) / ( ∗ ‘ ( abs ‘ 𝑋 ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )
36 32 33 35 3eqtrd ⊢ ( 𝜑 → ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) = ( ( ∗ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )
37 18 36 oveq12d ⊢ ( 𝜑 → ( ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) + ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( ( 𝑋 / ( abs ‘ 𝑋 ) ) + ( ( ∗ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) ) )
38 1 3 6 8 divdird ⊢ ( 𝜑 → ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / ( abs ‘ 𝑋 ) ) = ( ( 𝑋 / ( abs ‘ 𝑋 ) ) + ( ( ∗ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) ) )
39 37 38 eqtr4d ⊢ ( 𝜑 → ( ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) + ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) = ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / ( abs ‘ 𝑋 ) ) )
40 39 oveq1d ⊢ ( 𝜑 → ( ( ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) + ( exp ‘ ( - i · ( ℑ ‘ ( log ‘ 𝑋 ) ) ) ) ) / 2 ) = ( ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / ( abs ‘ 𝑋 ) ) / 2 ) )
41 16 40 eqtrd ⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / ( abs ‘ 𝑋 ) ) / 2 ) )
42 reval ⊢ ( 𝑋 ∈ ℂ → ( ℜ ‘ 𝑋 ) = ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / 2 ) )
43 1 42 syl ⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) = ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / 2 ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) = ( ( ( 𝑋 + ( ∗ ‘ 𝑋 ) ) / 2 ) / ( abs ‘ 𝑋 ) ) )
45 11 41 44 3eqtr4d ⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )