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	$⊢ (A \in ℂ \land ℜ (A) \neq 0) \to \tan ℑ (\log A) = \frac{ℑ (A)}{ℜ (A)}$

Proof

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

Metamath Proof Explorer

Theorem tanarg

Proof