atantan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 5-Apr-2015)

		Ref	Expression
	Assertion	atantan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to arctan (\tan A) = A$

Proof

Step	Hyp	Ref	Expression
1		cosne0	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A \neq 0$
2		atandmtan	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A \in dom arctan$
3	1 2	syldan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \tan A \in dom arctan$
4		atanval	$⊢ \tan A \in dom arctan \to arctan (\tan A) = (\frac{i}{2}) (\log (1 - i \tan A) - \log (1 + i \tan A))$
5	3 4	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to arctan (\tan A) = (\frac{i}{2}) (\log (1 - i \tan A) - \log (1 + i \tan A))$
6		ax-1cn	$⊢ 1 \in ℂ$
7		ax-icn	$⊢ i \in ℂ$
8		tancl	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A \in ℂ$
9	1 8	syldan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \tan A \in ℂ$
10		mulcl	$⊢ (i \in ℂ \land \tan A \in ℂ) \to i \tan A \in ℂ$
11	7 9 10	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \tan A \in ℂ$
12		addcl	$⊢ (1 \in ℂ \land i \tan A \in ℂ) \to 1 + i \tan A \in ℂ$
13	6 11 12	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 + i \tan A \in ℂ$
14		atandm2	$⊢ \tan A \in dom arctan \leftrightarrow (\tan A \in ℂ \land 1 - i \tan A \neq 0 \land 1 + i \tan A \neq 0)$
15	3 14	sylib	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\tan A \in ℂ \land 1 - i \tan A \neq 0 \land 1 + i \tan A \neq 0)$
16	15	simp3d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 + i \tan A \neq 0$
17	13 16	logcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log (1 + i \tan A) \in ℂ$
18		subcl	$⊢ (1 \in ℂ \land i \tan A \in ℂ) \to 1 - i \tan A \in ℂ$
19	6 11 18	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 - i \tan A \in ℂ$
20	15	simp2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 - i \tan A \neq 0$
21	19 20	logcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log (1 - i \tan A) \in ℂ$
22	17 21	negsubdi2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - (\log (1 + i \tan A) - \log (1 - i \tan A)) = \log (1 - i \tan A) - \log (1 + i \tan A)$
23		efsub	$⊢ (\log (1 + i \tan A) \in ℂ \land \log (1 - i \tan A) \in ℂ) \to e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = \frac{e^{\log (1 + i \tan A)}}{e^{\log (1 - i \tan A)}}$
24	17 21 23	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = \frac{e^{\log (1 + i \tan A)}}{e^{\log (1 - i \tan A)}}$
25		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
26	25	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A \in ℂ$
27		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
28	27	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \sin A \in ℂ$
29		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
30	7 28 29	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \sin A \in ℂ$
31	26 30 26 1	divdird	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\cos A + i \sin A}{\cos A} = (\frac{\cos A}{\cos A}) + (\frac{i \sin A}{\cos A})$
32	26 1	dividd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\cos A}{\cos A} = 1$
33	7	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \in ℂ$
34	33 28 26 1	divassd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{i \sin A}{\cos A} = i (\frac{\sin A}{\cos A})$
35		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
36	1 35	syldan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \tan A = \frac{\sin A}{\cos A}$
37	36	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \tan A = i (\frac{\sin A}{\cos A})$
38	34 37	eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{i \sin A}{\cos A} = i \tan A$
39	32 38	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{\cos A}{\cos A}) + (\frac{i \sin A}{\cos A}) = 1 + i \tan A$
40	31 39	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\cos A + i \sin A}{\cos A} = 1 + i \tan A$
41		efival	$⊢ A \in ℂ \to e^{i A} = \cos A + i \sin A$
42	41	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i A} = \cos A + i \sin A$
43	42	oveq1d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{e^{i A}}{\cos A} = \frac{\cos A + i \sin A}{\cos A}$
44		eflog	$⊢ (1 + i \tan A \in ℂ \land 1 + i \tan A \neq 0) \to e^{\log (1 + i \tan A)} = 1 + i \tan A$
45	13 16 44	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{\log (1 + i \tan A)} = 1 + i \tan A$
46	40 43 45	3eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{e^{i A}}{\cos A} = e^{\log (1 + i \tan A)}$
47	26 30 26 1	divsubdird	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\cos A - i \sin A}{\cos A} = (\frac{\cos A}{\cos A}) - (\frac{i \sin A}{\cos A})$
48	32 38	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{\cos A}{\cos A}) - (\frac{i \sin A}{\cos A}) = 1 - i \tan A$
49	47 48	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\cos A - i \sin A}{\cos A} = 1 - i \tan A$
50		negcl	$⊢ A \in ℂ \to - A \in ℂ$
51	50	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - A \in ℂ$
52		efival	$⊢ - A \in ℂ \to e^{i (- A)} = \cos (- A) + i \sin (- A)$
53	51 52	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i (- A)} = \cos (- A) + i \sin (- A)$
54		cosneg	$⊢ A \in ℂ \to \cos (- A) = \cos A$
55	54	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos (- A) = \cos A$
56		sinneg	$⊢ A \in ℂ \to \sin (- A) = - \sin A$
57	56	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \sin (- A) = - \sin A$
58	57	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \sin (- A) = i (- \sin A)$
59		mulneg2	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i (- \sin A) = - i \sin A$
60	7 28 59	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i (- \sin A) = - i \sin A$
61	58 60	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i \sin (- A) = - i \sin A$
62	55 61	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos (- A) + i \sin (- A) = \cos A + (- i \sin A)$
63	53 62	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i (- A)} = \cos A + (- i \sin A)$
64		simpl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to A \in ℂ$
65		mulneg2	$⊢ (i \in ℂ \land A \in ℂ) \to i (- A) = - i A$
66	7 64 65	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i (- A) = - i A$
67	66	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i (- A)} = e^{- i A}$
68	26 30	negsubd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos A + (- i \sin A) = \cos A - i \sin A$
69	63 67 68	3eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{- i A} = \cos A - i \sin A$
70	69	oveq1d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{e^{- i A}}{\cos A} = \frac{\cos A - i \sin A}{\cos A}$
71		eflog	$⊢ (1 - i \tan A \in ℂ \land 1 - i \tan A \neq 0) \to e^{\log (1 - i \tan A)} = 1 - i \tan A$
72	19 20 71	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{\log (1 - i \tan A)} = 1 - i \tan A$
73	49 70 72	3eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{e^{- i A}}{\cos A} = e^{\log (1 - i \tan A)}$
74	46 73	oveq12d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\frac{e^{i A}}{\cos A}}{\frac{e^{- i A}}{\cos A}} = \frac{e^{\log (1 + i \tan A)}}{e^{\log (1 - i \tan A)}}$
75		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
76	7 64 75	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i A \in ℂ$
77		efcl	$⊢ i A \in ℂ \to e^{i A} \in ℂ$
78	76 77	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i A} \in ℂ$
79	76	negcld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - i A \in ℂ$
80		efcl	$⊢ - i A \in ℂ \to e^{- i A} \in ℂ$
81	79 80	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{- i A} \in ℂ$
82		efne0	$⊢ - i A \in ℂ \to e^{- i A} \neq 0$
83	79 82	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{- i A} \neq 0$
84	78 81 26 83 1	divcan7d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\frac{e^{i A}}{\cos A}}{\frac{e^{- i A}}{\cos A}} = \frac{e^{i A}}{e^{- i A}}$
85		efsub	$⊢ (i A \in ℂ \land - i A \in ℂ) \to e^{i A - (- i A)} = \frac{e^{i A}}{e^{- i A}}$
86	76 79 85	syl2anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i A - (- i A)} = \frac{e^{i A}}{e^{- i A}}$
87	76 76	subnegd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i A - (- i A) = i A + i A$
88	76	2timesd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 i A = i A + i A$
89	87 88	eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i A - (- i A) = 2 i A$
90	89	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{i A - (- i A)} = e^{2 i A}$
91	84 86 90	3eqtr2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{\frac{e^{i A}}{\cos A}}{\frac{e^{- i A}}{\cos A}} = e^{2 i A}$
92	24 74 91	3eqtr2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = e^{2 i A}$
93	92	fveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = \log e^{2 i A}$
94	64	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to A \in ℂ$
95	94	renegd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (- A) = - ℜ (A)$
96	94	recld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (A) \in ℝ$
97	96	renegcld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to - ℜ (A) \in ℝ$
98		simpr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (A) < 0$
99	96	lt0neg1d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to (ℜ (A) < 0 \leftrightarrow 0 < - ℜ (A))$
100	98 99	mpbid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to 0 < - ℜ (A)$
101		eliooord	$⊢ ℜ (A) \in (- \frac{π}{2}, \frac{π}{2}) \to (- \frac{π}{2} < ℜ (A) \land ℜ (A) < \frac{π}{2})$
102	101	adantl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (- \frac{π}{2} < ℜ (A) \land ℜ (A) < \frac{π}{2})$
103	102	simpld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - \frac{π}{2} < ℜ (A)$
104	103	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to - \frac{π}{2} < ℜ (A)$
105		halfpire	$⊢ \frac{π}{2} \in ℝ$
106		ltnegcon1	$⊢ (\frac{π}{2} \in ℝ \land ℜ (A) \in ℝ) \to (- \frac{π}{2} < ℜ (A) \leftrightarrow - ℜ (A) < \frac{π}{2})$
107	105 96 106	sylancr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to (- \frac{π}{2} < ℜ (A) \leftrightarrow - ℜ (A) < \frac{π}{2})$
108	104 107	mpbid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to - ℜ (A) < \frac{π}{2}$
109		0xr	$⊢ 0 \in ℝ^{*}$
110	105	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
111		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (- ℜ (A) \in (0, \frac{π}{2}) \leftrightarrow (- ℜ (A) \in ℝ \land 0 < - ℜ (A) \land - ℜ (A) < \frac{π}{2}))$
112	109 110 111	mp2an	$⊢ - ℜ (A) \in (0, \frac{π}{2}) \leftrightarrow (- ℜ (A) \in ℝ \land 0 < - ℜ (A) \land - ℜ (A) < \frac{π}{2})$
113	97 100 108 112	syl3anbrc	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to - ℜ (A) \in (0, \frac{π}{2})$
114	95 113	eqeltrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (- A) \in (0, \frac{π}{2})$
115		tanregt0	$⊢ (- A \in ℂ \land ℜ (- A) \in (0, \frac{π}{2})) \to 0 < ℜ (\tan (- A))$
116	51 114 115	syl2an2r	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to 0 < ℜ (\tan (- A))$
117		tanneg	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan (- A) = - \tan A$
118	1 117	syldan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \tan (- A) = - \tan A$
119	118	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to \tan (- A) = - \tan A$
120	119	fveq2d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (\tan (- A)) = ℜ (- \tan A)$
121	9	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to \tan A \in ℂ$
122	121	renegd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (- \tan A) = - ℜ (\tan A)$
123	120 122	eqtrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (\tan (- A)) = - ℜ (\tan A)$
124	116 123	breqtrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to 0 < - ℜ (\tan A)$
125	9	recld	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (\tan A) \in ℝ$
126	125	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (\tan A) \in ℝ$
127	126	lt0neg1d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to (ℜ (\tan A) < 0 \leftrightarrow 0 < - ℜ (\tan A))$
128	124 127	mpbird	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (\tan A) < 0$
129	128	lt0ne0d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to ℜ (\tan A) \neq 0$
130		atanlogsub	$⊢ (\tan A \in dom arctan \land ℜ (\tan A) \neq 0) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
131	3 129 130	syl2an2r	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) < 0) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
132		1re	$⊢ 1 \in ℝ$
133		ioossre	$⊢ (- 1, 1) \subseteq ℝ$
134	7	a1i	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \in ℂ$
135	11	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \tan A \in ℂ$
136		ine0	$⊢ i \neq 0$
137	136	a1i	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \neq 0$
138		ixi	$⊢ i i = - 1$
139	138	oveq1i	$⊢ i i \tan A = -1 \tan A$
140	9	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \tan A \in ℂ$
141	140	mulm1d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to -1 \tan A = - \tan A$
142	118	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \tan (- A) = - \tan A$
143	141 142	eqtr4d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to -1 \tan A = \tan (- A)$
144	139 143	eqtrid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i i \tan A = \tan (- A)$
145	134 134 140	mulassd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i i \tan A = i i \tan A$
146	138	oveq1i	$⊢ i i A = -1 A$
147	64	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to A \in ℂ$
148	147	mulm1d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to -1 A = - A$
149	146 148	eqtrid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i i A = - A$
150	134 134 147	mulassd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i i A = i i A$
151	149 150	eqtr3d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to - A = i i A$
152	151	fveq2d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \tan (- A) = \tan i i A$
153	144 145 152	3eqtr3d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i i \tan A = \tan i i A$
154	134 135 137 153	mvllmuld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \tan A = \frac{\tan i i A}{i}$
155	76	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i A \in ℂ$
156		reim	$⊢ A \in ℂ \to ℜ (A) = ℑ (i A)$
157	156	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (A) = ℑ (i A)$
158	157	eqeq1d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (ℜ (A) = 0 \leftrightarrow ℑ (i A) = 0)$
159	158	biimpa	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to ℑ (i A) = 0$
160	155 159	reim0bd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i A \in ℝ$
161		tanhbnd	$⊢ i A \in ℝ \to \frac{\tan i i A}{i} \in (- 1, 1)$
162	160 161	syl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \frac{\tan i i A}{i} \in (- 1, 1)$
163	154 162	eqeltrd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \tan A \in (- 1, 1)$
164	133 163	sselid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \tan A \in ℝ$
165		readdcl	$⊢ (1 \in ℝ \land i \tan A \in ℝ) \to 1 + i \tan A \in ℝ$
166	132 164 165	sylancr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 1 + i \tan A \in ℝ$
167		df-neg	$⊢ - 1 = 0 - 1$
168		eliooord	$⊢ i \tan A \in (- 1, 1) \to (- 1 < i \tan A \land i \tan A < 1)$
169	163 168	syl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to (- 1 < i \tan A \land i \tan A < 1)$
170	169	simpld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to - 1 < i \tan A$
171	167 170	eqbrtrrid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 0 - 1 < i \tan A$
172		0red	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 0 \in ℝ$
173	132	a1i	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 1 \in ℝ$
174	172 173 164	ltsubadd2d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to (0 - 1 < i \tan A \leftrightarrow 0 < 1 + i \tan A)$
175	171 174	mpbid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 0 < 1 + i \tan A$
176	166 175	elrpd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 1 + i \tan A \in ℝ^{+}$
177	176	relogcld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \log (1 + i \tan A) \in ℝ$
178	169	simprd	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to i \tan A < 1$
179		difrp	$⊢ (i \tan A \in ℝ \land 1 \in ℝ) \to (i \tan A < 1 \leftrightarrow 1 - i \tan A \in ℝ^{+})$
180	164 132 179	sylancl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to (i \tan A < 1 \leftrightarrow 1 - i \tan A \in ℝ^{+})$
181	178 180	mpbid	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to 1 - i \tan A \in ℝ^{+}$
182	181	relogcld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \log (1 - i \tan A) \in ℝ$
183	177 182	resubcld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ℝ$
184		relogrn	$⊢ \log (1 + i \tan A) - \log (1 - i \tan A) \in ℝ \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
185	183 184	syl	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land ℜ (A) = 0) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
186	64	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to A \in ℂ$
187	186	recld	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to ℜ (A) \in ℝ$
188		simpr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to 0 < ℜ (A)$
189	102	simprd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (A) < \frac{π}{2}$
190	189	adantr	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to ℜ (A) < \frac{π}{2}$
191		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (ℜ (A) \in (0, \frac{π}{2}) \leftrightarrow (ℜ (A) \in ℝ \land 0 < ℜ (A) \land ℜ (A) < \frac{π}{2}))$
192	109 110 191	mp2an	$⊢ ℜ (A) \in (0, \frac{π}{2}) \leftrightarrow (ℜ (A) \in ℝ \land 0 < ℜ (A) \land ℜ (A) < \frac{π}{2})$
193	187 188 190 192	syl3anbrc	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to ℜ (A) \in (0, \frac{π}{2})$
194		tanregt0	$⊢ (A \in ℂ \land ℜ (A) \in (0, \frac{π}{2})) \to 0 < ℜ (\tan A)$
195	64 193 194	syl2an2r	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to 0 < ℜ (\tan A)$
196	195	gt0ne0d	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to ℜ (\tan A) \neq 0$
197	3 196 130	syl2an2r	$⊢ ((A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \land 0 < ℜ (A)) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
198		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
199	198	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℜ (A) \in ℝ$
200		0re	$⊢ 0 \in ℝ$
201		lttri4	$⊢ (ℜ (A) \in ℝ \land 0 \in ℝ) \to (ℜ (A) < 0 \lor ℜ (A) = 0 \lor 0 < ℜ (A))$
202	199 200 201	sylancl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (ℜ (A) < 0 \lor ℜ (A) = 0 \lor 0 < ℜ (A))$
203	131 185 197 202	mpjao3dan	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log$
204		logef	$⊢ \log (1 + i \tan A) - \log (1 - i \tan A) \in ran log \to \log e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = \log (1 + i \tan A) - \log (1 - i \tan A)$
205	203 204	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log e^{\log (1 + i \tan A) - \log (1 - i \tan A)} = \log (1 + i \tan A) - \log (1 - i \tan A)$
206		2cn	$⊢ 2 \in ℂ$
207		mulcl	$⊢ (2 \in ℂ \land i A \in ℂ) \to 2 i A \in ℂ$
208	206 76 207	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 i A \in ℂ$
209		picn	$⊢ π \in ℂ$
210		2ne0	$⊢ 2 \neq 0$
211		divneg	$⊢ (π \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{π}{2} = \frac{- π}{2}$
212	209 206 210 211	mp3an	$⊢ - \frac{π}{2} = \frac{- π}{2}$
213	212 103	eqbrtrrid	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{- π}{2} < ℜ (A)$
214		pire	$⊢ π \in ℝ$
215	214	renegcli	$⊢ - π \in ℝ$
216	215	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - π \in ℝ$
217		2re	$⊢ 2 \in ℝ$
218	217	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 \in ℝ$
219		2pos	$⊢ 0 < 2$
220	219	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 0 < 2$
221		ltdivmul	$⊢ (- π \in ℝ \land ℜ (A) \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{- π}{2} < ℜ (A) \leftrightarrow - π < 2 ℜ (A))$
222	216 199 218 220 221	syl112anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{- π}{2} < ℜ (A) \leftrightarrow - π < 2 ℜ (A))$
223	213 222	mpbid	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - π < 2 ℜ (A)$
224		immul2	$⊢ (2 \in ℝ \land i A \in ℂ) \to ℑ (2 i A) = 2 ℑ (i A)$
225	217 76 224	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (2 i A) = 2 ℑ (i A)$
226	157	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 ℜ (A) = 2 ℑ (i A)$
227	225 226	eqtr4d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (2 i A) = 2 ℜ (A)$
228	223 227	breqtrrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - π < ℑ (2 i A)$
229		remulcl	$⊢ (2 \in ℝ \land ℜ (A) \in ℝ) \to 2 ℜ (A) \in ℝ$
230	217 199 229	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 ℜ (A) \in ℝ$
231	214	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to π \in ℝ$
232		ltmuldiv2	$⊢ (ℜ (A) \in ℝ \land π \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 ℜ (A) < π \leftrightarrow ℜ (A) < \frac{π}{2})$
233	199 231 218 220 232	syl112anc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (2 ℜ (A) < π \leftrightarrow ℜ (A) < \frac{π}{2})$
234	189 233	mpbird	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 ℜ (A) < π$
235	230 231 234	ltled	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 ℜ (A) \leq π$
236	227 235	eqbrtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to ℑ (2 i A) \leq π$
237		ellogrn	$⊢ 2 i A \in ran log \leftrightarrow (2 i A \in ℂ \land - π < ℑ (2 i A) \land ℑ (2 i A) \leq π)$
238	208 228 236 237	syl3anbrc	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 i A \in ran log$
239		logef	$⊢ 2 i A \in ran log \to \log e^{2 i A} = 2 i A$
240	238 239	syl	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log e^{2 i A} = 2 i A$
241	93 205 240	3eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log (1 + i \tan A) - \log (1 - i \tan A) = 2 i A$
242	241	negeqd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to - (\log (1 + i \tan A) - \log (1 - i \tan A)) = - 2 i A$
243	22 242	eqtr3d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \log (1 - i \tan A) - \log (1 + i \tan A) = - 2 i A$
244	243	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{i}{2}) (\log (1 - i \tan A) - \log (1 + i \tan A)) = (\frac{i}{2}) (- 2 i A)$
245		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
246	7 245	mp1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to \frac{i}{2} \in ℂ$
247	206	a1i	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 \in ℂ$
248	246 247 79	mulassd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{i}{2}) \cdot 2 (- i A) = (\frac{i}{2}) 2 (- i A)$
249	7 206 210	divcan1i	$⊢ (\frac{i}{2}) \cdot 2 = i$
250	249	oveq1i	$⊢ (\frac{i}{2}) \cdot 2 (- i A) = i (- i A)$
251	33 33 51	mulassd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i i (- A) = i i (- A)$
252	138	oveq1i	$⊢ i i (- A) = -1 (- A)$
253		mul2neg	$⊢ (1 \in ℂ \land A \in ℂ) \to -1 (- A) = 1 A$
254	6 64 253	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to -1 (- A) = 1 A$
255		mullid	$⊢ A \in ℂ \to 1 A = A$
256	255	adantr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 1 A = A$
257	254 256	eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to -1 (- A) = A$
258	252 257	eqtrid	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i i (- A) = A$
259	66	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i i (- A) = i (- i A)$
260	251 258 259	3eqtr3rd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to i (- i A) = A$
261	250 260	eqtrid	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{i}{2}) \cdot 2 (- i A) = A$
262		mulneg2	$⊢ (2 \in ℂ \land i A \in ℂ) \to 2 (- i A) = - 2 i A$
263	206 76 262	sylancr	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to 2 (- i A) = - 2 i A$
264	263	oveq2d	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{i}{2}) 2 (- i A) = (\frac{i}{2}) (- 2 i A)$
265	248 261 264	3eqtr3rd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to (\frac{i}{2}) (- 2 i A) = A$
266	5 244 265	3eqtrd	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to arctan (\tan A) = A$

Metamath Proof Explorer

Theorem atantan

Proof