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	$$⊢\phi \to X\in ℂ$$
	cosargd.2	$$⊢\phi \to X\ne 0$$
Assertion	cosargd	$$⊢\phi \to \cos \Im \left(\log X\right)=\frac{\Re \left(X\right)}{\left|X\right|}$$

Proof

Step	Hyp	Ref	Expression
1		cosargd.1	$$⊢\phi \to X\in ℂ$$
2		cosargd.2	$$⊢\phi \to X\ne 0$$
3	1	cjcld	$$⊢\phi \to \bar{X}\in ℂ$$
4	1 3	addcld	$$⊢\phi \to X+\bar{X}\in ℂ$$
5	1	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
6	5	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
7		2cnd	$$⊢\phi \to 2\in ℂ$$
8	1 2	absne0d	$$⊢\phi \to \left|X\right|\ne 0$$
9		2ne0	$$⊢2\ne 0$$
10	9	a1i	$$⊢\phi \to 2\ne 0$$
11	4 6 7 8 10	divdiv32d	$$⊢\phi \to \frac{\frac{X+\bar{X}}{\left|X\right|}}{2}=\frac{\frac{X+\bar{X}}{2}}{\left|X\right|}$$
12	1 2	logcld	$$⊢\phi \to \log X\in ℂ$$
13	12	imcld	$$⊢\phi \to \Im \left(\log X\right)\in ℝ$$
14	13	recnd	$$⊢\phi \to \Im \left(\log X\right)\in ℂ$$
15		cosval	$$⊢\Im \left(\log X\right)\in ℂ\to \cos \Im \left(\log X\right)=\frac{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}}{2}$$
16	14 15	syl	$$⊢\phi \to \cos \Im \left(\log X\right)=\frac{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}}{2}$$
17		efiarg	$$⊢\left(X\in ℂ\wedge X\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}=\frac{X}{\left|X\right|}$$
18	1 2 17	syl2anc	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}=\frac{X}{\left|X\right|}$$
19		ax-icn	$$⊢\mathrm{i}\in ℂ$$
20	19	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
21	20 14	mulcld	$$⊢\phi \to \mathrm{i}\Im \left(\log X\right)\in ℂ$$
22		efcj	$$⊢\mathrm{i}\Im \left(\log X\right)\in ℂ\to {\mathrm{e}}^{\overline{\mathrm{i}\Im \left(\log X\right)}}=\overline{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}}$$
23	21 22	syl	$$⊢\phi \to {\mathrm{e}}^{\overline{\mathrm{i}\Im \left(\log X\right)}}=\overline{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}}$$
24	20 14	cjmuld	$$⊢\phi \to \overline{\mathrm{i}\Im \left(\log X\right)}=\bar{\mathrm{i}}\overline{\Im \left(\log X\right)}$$
25		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
26	25	a1i	$$⊢\phi \to \bar{\mathrm{i}}=-\mathrm{i}$$
27	13	cjred	$$⊢\phi \to \overline{\Im \left(\log X\right)}=\Im \left(\log X\right)$$
28	26 27	oveq12d	$$⊢\phi \to \bar{\mathrm{i}}\overline{\Im \left(\log X\right)}=\left(-\mathrm{i}\right)\Im \left(\log X\right)$$
29	24 28	eqtrd	$$⊢\phi \to \overline{\mathrm{i}\Im \left(\log X\right)}=\left(-\mathrm{i}\right)\Im \left(\log X\right)$$
30	29	fveq2d	$$⊢\phi \to {\mathrm{e}}^{\overline{\mathrm{i}\Im \left(\log X\right)}}={\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}$$
31	18	fveq2d	$$⊢\phi \to \overline{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}}=\overline{\frac{X}{\left|X\right|}}$$
32	23 30 31	3eqtr3d	$$⊢\phi \to {\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}=\overline{\frac{X}{\left|X\right|}}$$
33	1 6 8	cjdivd	$$⊢\phi \to \overline{\frac{X}{\left|X\right|}}=\frac{\bar{X}}{\overline{\left|X\right|}}$$
34	5	cjred	$$⊢\phi \to \overline{\left|X\right|}=\left|X\right|$$
35	34	oveq2d	$$⊢\phi \to \frac{\bar{X}}{\overline{\left|X\right|}}=\frac{\bar{X}}{\left|X\right|}$$
36	32 33 35	3eqtrd	$$⊢\phi \to {\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}=\frac{\bar{X}}{\left|X\right|}$$
37	18 36	oveq12d	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}=\left(\frac{X}{\left|X\right|}\right)+\left(\frac{\bar{X}}{\left|X\right|}\right)$$
38	1 3 6 8	divdird	$$⊢\phi \to \frac{X+\bar{X}}{\left|X\right|}=\left(\frac{X}{\left|X\right|}\right)+\left(\frac{\bar{X}}{\left|X\right|}\right)$$
39	37 38	eqtr4d	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}=\frac{X+\bar{X}}{\left|X\right|}$$
40	39	oveq1d	$$⊢\phi \to \frac{{\mathrm{e}}^{\mathrm{i}\Im \left(\log X\right)}+{\mathrm{e}}^{\left(-\mathrm{i}\right)\Im \left(\log X\right)}}{2}=\frac{\frac{X+\bar{X}}{\left|X\right|}}{2}$$
41	16 40	eqtrd	$$⊢\phi \to \cos \Im \left(\log X\right)=\frac{\frac{X+\bar{X}}{\left|X\right|}}{2}$$
42		reval	$$⊢X\in ℂ\to \Re \left(X\right)=\frac{X+\bar{X}}{2}$$
43	1 42	syl	$$⊢\phi \to \Re \left(X\right)=\frac{X+\bar{X}}{2}$$
44	43	oveq1d	$$⊢\phi \to \frac{\Re \left(X\right)}{\left|X\right|}=\frac{\frac{X+\bar{X}}{2}}{\left|X\right|}$$
45	11 41 44	3eqtr4d	$$⊢\phi \to \cos \Im \left(\log X\right)=\frac{\Re \left(X\right)}{\left|X\right|}$$