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 ‘ 𝑋 ) ) )