Theorem tanarg

Description: The basic relation between the "arg" function Im o. log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Assertion	tanarg	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \tan \Im \left(\log A\right)=\frac{\Im \left(A\right)}{\Re \left(A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=0\to \Re \left(A\right)=\Re \left(0\right)$$
2		re0	$$⊢\Re \left(0\right)=0$$
3	1 2	eqtrdi	$$⊢A=0\to \Re \left(A\right)=0$$
4	3	necon3i	$$⊢\Re \left(A\right)\ne 0\to A\ne 0$$
5		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
6	4 5	sylan2	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \log A\in ℂ$$
7	6	imcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
8	7	recnd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Im \left(\log A\right)\in ℂ$$
9		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
10	9	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2\in ℂ$$
11		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
12	11	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left|A\right|\in ℝ$$
13	12	recnd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left|A\right|\in ℂ$$
14	13	sqcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left|A\right|}^2\in ℂ$$
15		absrpcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$
16	4 15	sylan2	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$
17	16	rpne0d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left|A\right|\ne 0$$
18		sqne0	$$⊢\left|A\right|\in ℂ\to \left({\left|A\right|}^2\ne 0\leftrightarrow \left|A\right|\ne 0\right)$$
19	13 18	syl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left({\left|A\right|}^2\ne 0\leftrightarrow \left|A\right|\ne 0\right)$$
20	17 19	mpbird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left|A\right|}^2\ne 0$$
21	10 14 14 20	divdird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{A^2+{\left|A\right|}^2}{{\left|A\right|}^2}=\left(\frac{A^2}{{\left|A\right|}^2}\right)+\left(\frac{{\left|A\right|}^2}{{\left|A\right|}^2}\right)$$
22		ax-icn	$$⊢\mathrm{i}\in ℂ$$
23		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(\log A\right)\in ℂ\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
24	22 8 23	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
25		2z	$$⊢2\in \mathbb{Z}$$
26		efexp	$$⊢\left(\mathrm{i}\Im \left(\log A\right)\in ℂ\wedge 2\in \mathbb{Z}\right)\to {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}={{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}}^2$$
27	24 25 26	sylancl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}={{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}}^2$$
28		efiarg	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$
29	4 28	sylan2	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}=\frac{A}{\left|A\right|}$$
30	29	oveq1d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {{\mathrm{e}}^{\mathrm{i}\Im \left(\log A\right)}}^2={\left(\frac{A}{\left|A\right|}\right)}^2$$
31		simpl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A\in ℂ$$
32	31 13 17	sqdivd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left(\frac{A}{\left|A\right|}\right)}^2=\frac{A^2}{{\left|A\right|}^2}$$
33	27 30 32	3eqtrrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{A^2}{{\left|A\right|}^2}={\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}$$
34	14 20	dividd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{{\left|A\right|}^2}{{\left|A\right|}^2}=1$$
35	33 34	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(\frac{A^2}{{\left|A\right|}^2}\right)+\left(\frac{{\left|A\right|}^2}{{\left|A\right|}^2}\right)={\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1$$
36	21 35	eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1=\frac{A^2+{\left|A\right|}^2}{{\left|A\right|}^2}$$
37	10 14	addcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2+{\left|A\right|}^2\in ℂ$$
38	22	a1i	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\in ℂ$$
39		2cn	$$⊢2\in ℂ$$
40		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
41	40	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\in ℝ$$
42	41	recnd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\in ℂ$$
43	42	sqcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2\in ℂ$$
44		mulcl	$$⊢\left(2\in ℂ\wedge {\Re \left(A\right)}^2\in ℂ\right)\to 2{\Re \left(A\right)}^2\in ℂ$$
45	39 43 44	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Re \left(A\right)}^2\in ℂ$$
46	39	a1i	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\in ℂ$$
47		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
48	47	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Im \left(A\right)\in ℝ$$
49	48	recnd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Im \left(A\right)\in ℂ$$
50	42 49	mulcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\Im \left(A\right)\in ℂ$$
51	38 46 50	mul12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}2\Re \left(A\right)\Im \left(A\right)=2\mathrm{i}\Re \left(A\right)\Im \left(A\right)$$
52	38 42 49	mul12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\Re \left(A\right)\Im \left(A\right)=\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
53	52	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\mathrm{i}\Re \left(A\right)\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
54	51 53	eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}2\Re \left(A\right)\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
55		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
56	22 49 55	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
57	42 56	mulcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\mathrm{i}\Im \left(A\right)\in ℂ$$
58		mulcl	$$⊢\left(2\in ℂ\wedge \Re \left(A\right)\mathrm{i}\Im \left(A\right)\in ℂ\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)\in ℂ$$
59	39 57 58	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)\in ℂ$$
60	54 59	eqeltrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}2\Re \left(A\right)\Im \left(A\right)\in ℂ$$
61	38 45 60	adddid	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(2{\Re \left(A\right)}^2+\mathrm{i}2\Re \left(A\right)\Im \left(A\right)\right)=\mathrm{i}2{\Re \left(A\right)}^2+\mathrm{i}\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
62		mulcl	$$⊢\left(\Re \left(A\right)\in ℂ\wedge \mathrm{i}\in ℂ\right)\to \Re \left(A\right)\mathrm{i}\in ℂ$$
63	42 22 62	sylancl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\mathrm{i}\in ℂ$$
64	46 63 42	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Re \left(A\right)=2\Re \left(A\right)\mathrm{i}\Re \left(A\right)$$
65	42	sqvald	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2=\Re \left(A\right)\Re \left(A\right)$$
66	65	oveq1d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2\mathrm{i}=\Re \left(A\right)\Re \left(A\right)\mathrm{i}$$
67		mulcom	$$⊢\left({\Re \left(A\right)}^2\in ℂ\wedge \mathrm{i}\in ℂ\right)\to {\Re \left(A\right)}^2\mathrm{i}=\mathrm{i}{\Re \left(A\right)}^2$$
68	43 22 67	sylancl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2\mathrm{i}=\mathrm{i}{\Re \left(A\right)}^2$$
69	42 42 38	mul32d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\Re \left(A\right)\mathrm{i}=\Re \left(A\right)\mathrm{i}\Re \left(A\right)$$
70	66 68 69	3eqtr3d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}{\Re \left(A\right)}^2=\Re \left(A\right)\mathrm{i}\Re \left(A\right)$$
71	70	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\mathrm{i}{\Re \left(A\right)}^2=2\Re \left(A\right)\mathrm{i}\Re \left(A\right)$$
72	46 38 43	mul12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\mathrm{i}{\Re \left(A\right)}^2=\mathrm{i}2{\Re \left(A\right)}^2$$
73	64 71 72	3eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Re \left(A\right)=\mathrm{i}2{\Re \left(A\right)}^2$$
74		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
75	74	oveq1i	$$⊢\mathrm{i}\mathrm{i}2\Im \left(A\right)\Re \left(A\right)=-12\Im \left(A\right)\Re \left(A\right)$$
76		mulcl	$$⊢\left(2\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to 2\Im \left(A\right)\in ℂ$$
77	39 49 76	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\in ℂ$$
78	77 42	mulcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\Re \left(A\right)\in ℂ$$
79	38 38 78	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\mathrm{i}2\Im \left(A\right)\Re \left(A\right)=\mathrm{i}\mathrm{i}2\Im \left(A\right)\Re \left(A\right)$$
80	75 79	eqtr3id	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to -12\Im \left(A\right)\Re \left(A\right)=\mathrm{i}\mathrm{i}2\Im \left(A\right)\Re \left(A\right)$$
81	78	mulm1d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to -12\Im \left(A\right)\Re \left(A\right)=-2\Im \left(A\right)\Re \left(A\right)$$
82	46 49 42	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\Re \left(A\right)=2\Im \left(A\right)\Re \left(A\right)$$
83	49 42	mulcomd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Im \left(A\right)\Re \left(A\right)=\Re \left(A\right)\Im \left(A\right)$$
84	83	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\Re \left(A\right)=2\Re \left(A\right)\Im \left(A\right)$$
85	82 84	eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\Re \left(A\right)=2\Re \left(A\right)\Im \left(A\right)$$
86	85	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}2\Im \left(A\right)\Re \left(A\right)=\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
87	86	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\mathrm{i}2\Im \left(A\right)\Re \left(A\right)=\mathrm{i}\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
88	80 81 87	3eqtr3d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to -2\Im \left(A\right)\Re \left(A\right)=\mathrm{i}\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
89	73 88	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Re \left(A\right)+\left(-2\Im \left(A\right)\Re \left(A\right)\right)=\mathrm{i}2{\Re \left(A\right)}^2+\mathrm{i}\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
90		mulcl	$$⊢\left(2\in ℂ\wedge \Re \left(A\right)\mathrm{i}\in ℂ\right)\to 2\Re \left(A\right)\mathrm{i}\in ℂ$$
91	39 63 90	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\in ℂ$$
92	91 42	mulcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Re \left(A\right)\in ℂ$$
93	92 78	negsubd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Re \left(A\right)+\left(-2\Im \left(A\right)\Re \left(A\right)\right)=2\Re \left(A\right)\mathrm{i}\Re \left(A\right)-2\Im \left(A\right)\Re \left(A\right)$$
94	61 89 93	3eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(2{\Re \left(A\right)}^2+\mathrm{i}2\Re \left(A\right)\Im \left(A\right)\right)=2\Re \left(A\right)\mathrm{i}\Re \left(A\right)-2\Im \left(A\right)\Re \left(A\right)$$
95	49	sqcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Im \left(A\right)}^2\in ℂ$$
96	59 95	subcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\in ℂ$$
97	43 96 43 95	add4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)+{\Re \left(A\right)}^2+{\Im \left(A\right)}^2={\Re \left(A\right)}^2+{\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)+{\Im \left(A\right)}^2$$
98		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
99	98	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
100	99	oveq1d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2={\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)}^2$$
101		binom2	$$⊢\left(\Re \left(A\right)\in ℂ\wedge \mathrm{i}\Im \left(A\right)\in ℂ\right)\to {\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)}^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)+{\mathrm{i}\Im \left(A\right)}^2$$
102	42 56 101	syl2anc	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)}^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)+{\mathrm{i}\Im \left(A\right)}^2$$
103		sqmul	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to {\mathrm{i}\Im \left(A\right)}^2={\mathrm{i}}^2{\Im \left(A\right)}^2$$
104	22 49 103	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{i}\Im \left(A\right)}^2={\mathrm{i}}^2{\Im \left(A\right)}^2$$
105		i2	$$⊢{\mathrm{i}}^2=-1$$
106	105	oveq1i	$$⊢{\mathrm{i}}^2{\Im \left(A\right)}^2=-1{\Im \left(A\right)}^2$$
107	104 106	eqtrdi	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{i}\Im \left(A\right)}^2=-1{\Im \left(A\right)}^2$$
108	95	mulm1d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to -1{\Im \left(A\right)}^2=-{\Im \left(A\right)}^2$$
109	107 108	eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{i}\Im \left(A\right)}^2=-{\Im \left(A\right)}^2$$
110	109	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)+{\mathrm{i}\Im \left(A\right)}^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)+\left(-{\Im \left(A\right)}^2\right)$$
111	43 59	addcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)\in ℂ$$
112	111 95	negsubd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)+\left(-{\Im \left(A\right)}^2\right)={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2$$
113	102 110 112	3eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)}^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2$$
114	43 59 95	addsubassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2$$
115	100 113 114	3eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2={\Re \left(A\right)}^2+2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2$$
116		absvalsq2	$$⊢A\in ℂ\to {\left|A\right|}^2={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
117	116	adantr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\left|A\right|}^2={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
118	115 117	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2+{\left|A\right|}^2={\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)+{\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
119	43	2timesd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Re \left(A\right)}^2={\Re \left(A\right)}^2+{\Re \left(A\right)}^2$$
120	59 95	npcand	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2+{\Im \left(A\right)}^2=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
121	53 51 120	3eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}2\Re \left(A\right)\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2+{\Im \left(A\right)}^2$$
122	119 121	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Re \left(A\right)}^2+\mathrm{i}2\Re \left(A\right)\Im \left(A\right)={\Re \left(A\right)}^2+{\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)+{\Im \left(A\right)}^2$$
123	97 118 122	3eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2+{\left|A\right|}^2=2{\Re \left(A\right)}^2+\mathrm{i}2\Re \left(A\right)\Im \left(A\right)$$
124	123	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)=\mathrm{i}\left(2{\Re \left(A\right)}^2+\mathrm{i}2\Re \left(A\right)\Im \left(A\right)\right)$$
125	91 77 42	subdird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Re \left(A\right)=2\Re \left(A\right)\mathrm{i}\Re \left(A\right)-2\Im \left(A\right)\Re \left(A\right)$$
126	94 124 125	3eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)=\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Re \left(A\right)$$
127	91 77	subcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\in ℂ$$
128		mulcom	$$⊢\left(\Re \left(A\right)\in ℂ\wedge \mathrm{i}\in ℂ\right)\to \Re \left(A\right)\mathrm{i}=\mathrm{i}\Re \left(A\right)$$
129	42 22 128	sylancl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\mathrm{i}=\mathrm{i}\Re \left(A\right)$$
130		simpr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\ne 0$$
131		eleq1	$$⊢\mathrm{i}\Re \left(A\right)=\Im \left(A\right)\to \left(\mathrm{i}\Re \left(A\right)\in ℝ\leftrightarrow \Im \left(A\right)\in ℝ\right)$$
132	48 131	syl5ibrcom	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(\mathrm{i}\Re \left(A\right)=\Im \left(A\right)\to \mathrm{i}\Re \left(A\right)\in ℝ\right)$$
133		rimul	$$⊢\left(\Re \left(A\right)\in ℝ\wedge \mathrm{i}\Re \left(A\right)\in ℝ\right)\to \Re \left(A\right)=0$$
134	41 132 133	syl6an	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(\mathrm{i}\Re \left(A\right)=\Im \left(A\right)\to \Re \left(A\right)=0\right)$$
135	134	necon3d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(\Re \left(A\right)\ne 0\to \mathrm{i}\Re \left(A\right)\ne \Im \left(A\right)\right)$$
136	130 135	mpd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\Re \left(A\right)\ne \Im \left(A\right)$$
137	129 136	eqnetrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\mathrm{i}\ne \Im \left(A\right)$$
138	91 77	subeq0ad	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)=0\leftrightarrow 2\Re \left(A\right)\mathrm{i}=2\Im \left(A\right)\right)$$
139		2ne0	$$⊢2\ne 0$$
140	139	a1i	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\ne 0$$
141	63 49 46 140	mulcand	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}=2\Im \left(A\right)\leftrightarrow \Re \left(A\right)\mathrm{i}=\Im \left(A\right)\right)$$
142	138 141	bitrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)=0\leftrightarrow \Re \left(A\right)\mathrm{i}=\Im \left(A\right)\right)$$
143	142	necon3bid	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\ne 0\leftrightarrow \Re \left(A\right)\mathrm{i}\ne \Im \left(A\right)\right)$$
144	137 143	mpbird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\ne 0$$
145	127 42 144 130	mulne0d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Re \left(A\right)\ne 0$$
146	126 145	eqnetrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)\ne 0$$
147		oveq2	$$⊢A^2+{\left|A\right|}^2=0\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)=\mathrm{i}\cdot 0$$
148		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
149	147 148	eqtrdi	$$⊢A^2+{\left|A\right|}^2=0\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)=0$$
150	149	necon3i	$$⊢\mathrm{i}\left(A^2+{\left|A\right|}^2\right)\ne 0\to A^2+{\left|A\right|}^2\ne 0$$
151	146 150	syl	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2+{\left|A\right|}^2\ne 0$$
152	37 14 151 20	divne0d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{A^2+{\left|A\right|}^2}{{\left|A\right|}^2}\ne 0$$
153	36 152	eqnetrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\ne 0$$
154		tanval3	$$⊢\left(\Im \left(\log A\right)\in ℂ\wedge {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\ne 0\right)\to \tan \Im \left(\log A\right)=\frac{{\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\right)}$$
155	8 153 154	syl2anc	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \tan \Im \left(\log A\right)=\frac{{\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\right)}$$
156	10 14 14 20	divsubdird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{A^2-{\left|A\right|}^2}{{\left|A\right|}^2}=\left(\frac{A^2}{{\left|A\right|}^2}\right)-\left(\frac{{\left|A\right|}^2}{{\left|A\right|}^2}\right)$$
157	33 34	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(\frac{A^2}{{\left|A\right|}^2}\right)-\left(\frac{{\left|A\right|}^2}{{\left|A\right|}^2}\right)={\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}-1$$
158	156 157	eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}-1=\frac{A^2-{\left|A\right|}^2}{{\left|A\right|}^2}$$
159	36	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\right)=\mathrm{i}\left(\frac{A^2+{\left|A\right|}^2}{{\left|A\right|}^2}\right)$$
160	38 37 14 20	divassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}{{\left|A\right|}^2}=\mathrm{i}\left(\frac{A^2+{\left|A\right|}^2}{{\left|A\right|}^2}\right)$$
161	159 160	eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\right)=\frac{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}{{\left|A\right|}^2}$$
162	158 161	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{{\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}-1}{\mathrm{i}\left({\mathrm{e}}^{2\mathrm{i}\Im \left(\log A\right)}+1\right)}=\frac{\frac{A^2-{\left|A\right|}^2}{{\left|A\right|}^2}}{\frac{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}{{\left|A\right|}^2}}$$
163	10 14	subcld	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2-{\left|A\right|}^2\in ℂ$$
164		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A^2+{\left|A\right|}^2\in ℂ\right)\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)\in ℂ$$
165	22 37 164	sylancr	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \mathrm{i}\left(A^2+{\left|A\right|}^2\right)\in ℂ$$
166	163 165 14 146 20	divcan7d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{\frac{A^2-{\left|A\right|}^2}{{\left|A\right|}^2}}{\frac{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}{{\left|A\right|}^2}}=\frac{A^2-{\left|A\right|}^2}{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}$$
167	115 117	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2-{\left|A\right|}^2={\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)-\left({\Re \left(A\right)}^2+{\Im \left(A\right)}^2\right)$$
168	43 96 95	pnpcand	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Re \left(A\right)}^2+\left(2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2\right)-\left({\Re \left(A\right)}^2+{\Im \left(A\right)}^2\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2-{\Im \left(A\right)}^2$$
169	59 95 95	subsub4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2-{\Im \left(A\right)}^2=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-\left({\Im \left(A\right)}^2+{\Im \left(A\right)}^2\right)$$
170	95	2timesd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Im \left(A\right)}^2={\Im \left(A\right)}^2+{\Im \left(A\right)}^2$$
171	170	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-2{\Im \left(A\right)}^2=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-\left({\Im \left(A\right)}^2+{\Im \left(A\right)}^2\right)$$
172	46 63 49	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
173	42 38 49	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \Re \left(A\right)\mathrm{i}\Im \left(A\right)=\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
174	173	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
175	172 174	eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)$$
176	49	sqvald	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to {\Im \left(A\right)}^2=\Im \left(A\right)\Im \left(A\right)$$
177	176	oveq2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Im \left(A\right)}^2=2\Im \left(A\right)\Im \left(A\right)$$
178	46 49 49	mulassd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Im \left(A\right)\Im \left(A\right)=2\Im \left(A\right)\Im \left(A\right)$$
179	177 178	eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2{\Im \left(A\right)}^2=2\Im \left(A\right)\Im \left(A\right)$$
180	175 179	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-2{\Im \left(A\right)}^2=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-2\Im \left(A\right)\Im \left(A\right)$$
181	91 77 49	subdird	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)=2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-2\Im \left(A\right)\Im \left(A\right)$$
182	180 181	eqtr4d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-2{\Im \left(A\right)}^2=\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)$$
183	169 171 182	3eqtr2d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to 2\Re \left(A\right)\mathrm{i}\Im \left(A\right)-{\Im \left(A\right)}^2-{\Im \left(A\right)}^2=\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)$$
184	167 168 183	3eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to A^2-{\left|A\right|}^2=\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)$$
185	184 126	oveq12d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{A^2-{\left|A\right|}^2}{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}=\frac{\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)}{\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Re \left(A\right)}$$
186	49 42 127 130 144	divcan5d	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Im \left(A\right)}{\left(2\Re \left(A\right)\mathrm{i}-2\Im \left(A\right)\right)\Re \left(A\right)}=\frac{\Im \left(A\right)}{\Re \left(A\right)}$$
187	166 185 186	3eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \frac{\frac{A^2-{\left|A\right|}^2}{{\left|A\right|}^2}}{\frac{\mathrm{i}\left(A^2+{\left|A\right|}^2\right)}{{\left|A\right|}^2}}=\frac{\Im \left(A\right)}{\Re \left(A\right)}$$
188	155 162 187	3eqtrd	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\ne 0\right)\to \tan \Im \left(\log A\right)=\frac{\Im \left(A\right)}{\Re \left(A\right)}$$