dvatan

Description: The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	atansopn.d	$⊢ D = ℂ ∖ (−∞, 0]$
	atansopn.s	$⊢ S = \{y \in ℂ \| 1 + y^{2} \in D\}$
Assertion	dvatan	$⊢ ℂ D ({arctan ↾}_{S}) = (x \in S ⟼ \frac{1}{1 + x^{2}})$

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		atansopn.s	$⊢ S = \{y \in ℂ \| 1 + y^{2} \in D\}$
3		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
4	3	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
5		ax-1cn	$⊢ 1 \in ℂ$
6		ax-icn	$⊢ i \in ℂ$
7	1 2	atansssdm	$⊢ S \subseteq dom arctan$
8		simpr	$⊢ (⊤ \land x \in S) \to x \in S$
9	7 8	sselid	$⊢ (⊤ \land x \in S) \to x \in dom arctan$
10		atandm2	$⊢ x \in dom arctan \leftrightarrow (x \in ℂ \land 1 - i x \neq 0 \land 1 + i x \neq 0)$
11	9 10	sylib	$⊢ (⊤ \land x \in S) \to (x \in ℂ \land 1 - i x \neq 0 \land 1 + i x \neq 0)$
12	11	simp1d	$⊢ (⊤ \land x \in S) \to x \in ℂ$
13		mulcl	$⊢ (i \in ℂ \land x \in ℂ) \to i x \in ℂ$
14	6 12 13	sylancr	$⊢ (⊤ \land x \in S) \to i x \in ℂ$
15		subcl	$⊢ (1 \in ℂ \land i x \in ℂ) \to 1 - i x \in ℂ$
16	5 14 15	sylancr	$⊢ (⊤ \land x \in S) \to 1 - i x \in ℂ$
17	11	simp2d	$⊢ (⊤ \land x \in S) \to 1 - i x \neq 0$
18	16 17	logcld	$⊢ (⊤ \land x \in S) \to \log (1 - i x) \in ℂ$
19		addcl	$⊢ (1 \in ℂ \land i x \in ℂ) \to 1 + i x \in ℂ$
20	5 14 19	sylancr	$⊢ (⊤ \land x \in S) \to 1 + i x \in ℂ$
21	11	simp3d	$⊢ (⊤ \land x \in S) \to 1 + i x \neq 0$
22	20 21	logcld	$⊢ (⊤ \land x \in S) \to \log (1 + i x) \in ℂ$
23	18 22	subcld	$⊢ (⊤ \land x \in S) \to \log (1 - i x) - \log (1 + i x) \in ℂ$
24		ovexd	$⊢ (⊤ \land x \in S) \to \frac{\frac{2}{i}}{1 + x^{2}} \in V$
25		ovexd	$⊢ (⊤ \land x \in S) \to \frac{1}{x + i} \in V$
26	1 2	atans2	$⊢ x \in S \leftrightarrow (x \in ℂ \land 1 - i x \in D \land 1 + i x \in D)$
27	26	simp2bi	$⊢ x \in S \to 1 - i x \in D$
28	27	adantl	$⊢ (⊤ \land x \in S) \to 1 - i x \in D$
29		negex	$⊢ - i \in V$
30	29	a1i	$⊢ (⊤ \land x \in S) \to - i \in V$
31	1	logdmss	$⊢ D \subseteq ℂ ∖ \{0\}$
32		simpr	$⊢ (⊤ \land y \in D) \to y \in D$
33	31 32	sselid	$⊢ (⊤ \land y \in D) \to y \in (ℂ ∖ \{0\})$
34		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
35		f1of	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to log : ℂ ∖ \{0\} ⟶ ran log$
36	34 35	ax-mp	$⊢ log : ℂ ∖ \{0\} ⟶ ran log$
37	36	ffvelrni	$⊢ y \in (ℂ ∖ \{0\}) \to \log y \in ran log$
38		logrncn	$⊢ \log y \in ran log \to \log y \in ℂ$
39	33 37 38	3syl	$⊢ (⊤ \land y \in D) \to \log y \in ℂ$
40		ovexd	$⊢ (⊤ \land y \in D) \to \frac{1}{y} \in V$
41	6	a1i	$⊢ ⊤ \to i \in ℂ$
42	41 13	sylan	$⊢ (⊤ \land x \in ℂ) \to i x \in ℂ$
43	5 42 15	sylancr	$⊢ (⊤ \land x \in ℂ) \to 1 - i x \in ℂ$
44	29	a1i	$⊢ (⊤ \land x \in ℂ) \to - i \in V$
45		1cnd	$⊢ (⊤ \land x \in ℂ) \to 1 \in ℂ$
46		0cnd	$⊢ (⊤ \land x \in ℂ) \to 0 \in ℂ$
47		1cnd	$⊢ ⊤ \to 1 \in ℂ$
48	4 47	dvmptc	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
49	6	a1i	$⊢ (⊤ \land x \in ℂ) \to i \in ℂ$
50		simpr	$⊢ (⊤ \land x \in ℂ) \to x \in ℂ$
51	4	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
52	4 50 45 51 41	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = (x \in ℂ ⟼ i \cdot 1)$
53	6	mulid1i	$⊢ i \cdot 1 = i$
54	53	mpteq2i	$⊢ (x \in ℂ ⟼ i \cdot 1) = (x \in ℂ ⟼ i)$
55	52 54	eqtrdi	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ i x)}{d_{ℂ} x} = (x \in ℂ ⟼ i)$
56	4 45 46 48 42 49 55	dvmptsub	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - i x)}{d_{ℂ} x} = (x \in ℂ ⟼ 0 - i)$
57		df-neg	$⊢ - i = 0 - i$
58	57	mpteq2i	$⊢ (x \in ℂ ⟼ - i) = (x \in ℂ ⟼ 0 - i)$
59	56 58	eqtr4di	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - i x)}{d_{ℂ} x} = (x \in ℂ ⟼ - i)$
60	2	ssrab3	$⊢ S \subseteq ℂ$
61	60	a1i	$⊢ ⊤ \to S \subseteq ℂ$
62		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
63	62	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
64	63	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
65	1 2	atansopn	$⊢ S \in TopOpen (ℂ_{fld})$
66	65	a1i	$⊢ ⊤ \to S \in TopOpen (ℂ_{fld})$
67	4 43 44 59 61 64 62 66	dvmptres	$⊢ ⊤ \to \frac{d (x \in S⟼ 1 - i x)}{d_{ℂ} x} = (x \in S ⟼ - i)$
68		fssres	$⊢ (log : ℂ ∖ \{0\} ⟶ ran log \land D \subseteq ℂ ∖ \{0\}) \to ({log ↾}_{D}) : D ⟶ ran log$
69	36 31 68	mp2an	$⊢ ({log ↾}_{D}) : D ⟶ ran log$
70	69	a1i	$⊢ ⊤ \to ({log ↾}_{D}) : D ⟶ ran log$
71	70	feqmptd	$⊢ ⊤ \to {log ↾}_{D} = (y \in D ⟼ ({log ↾}_{D}) (y))$
72		fvres	$⊢ y \in D \to ({log ↾}_{D}) (y) = \log y$
73	72	mpteq2ia	$⊢ (y \in D ⟼ ({log ↾}_{D}) (y)) = (y \in D ⟼ \log y)$
74	71 73	eqtr2di	$⊢ ⊤ \to (y \in D ⟼ \log y) = {log ↾}_{D}$
75	74	oveq2d	$⊢ ⊤ \to \frac{d (y \in D⟼ \log y)}{d_{ℂ} y} = ℂ D ({log ↾}_{D})$
76	1	dvlog	$⊢ ℂ D ({log ↾}_{D}) = (y \in D ⟼ \frac{1}{y})$
77	75 76	eqtrdi	$⊢ ⊤ \to \frac{d (y \in D⟼ \log y)}{d_{ℂ} y} = (y \in D ⟼ \frac{1}{y})$
78		fveq2	$⊢ y = 1 - i x \to \log y = \log (1 - i x)$
79		oveq2	$⊢ y = 1 - i x \to \frac{1}{y} = \frac{1}{1 - i x}$
80	4 4 28 30 39 40 67 77 78 79	dvmptco	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 - i x))}{d_{ℂ} x} = (x \in S ⟼ (\frac{1}{1 - i x}) (- i))$
81		irec	$⊢ \frac{1}{i} = - i$
82	81	oveq2i	$⊢ (\frac{1}{1 - i x}) (\frac{1}{i}) = (\frac{1}{1 - i x}) (- i)$
83	6	a1i	$⊢ (⊤ \land x \in S) \to i \in ℂ$
84		ine0	$⊢ i \neq 0$
85	84	a1i	$⊢ (⊤ \land x \in S) \to i \neq 0$
86	16 83 17 85	recdiv2d	$⊢ (⊤ \land x \in S) \to \frac{\frac{1}{1 - i x}}{i} = \frac{1}{(1 - i x) i}$
87	16 17	reccld	$⊢ (⊤ \land x \in S) \to \frac{1}{1 - i x} \in ℂ$
88	87 83 85	divrecd	$⊢ (⊤ \land x \in S) \to \frac{\frac{1}{1 - i x}}{i} = (\frac{1}{1 - i x}) (\frac{1}{i})$
89		1cnd	$⊢ (⊤ \land x \in S) \to 1 \in ℂ$
90	89 14 83	subdird	$⊢ (⊤ \land x \in S) \to (1 - i x) i = 1 i - i x i$
91	6	mulid2i	$⊢ 1 i = i$
92	91	a1i	$⊢ (⊤ \land x \in S) \to 1 i = i$
93	83 12 83	mul32d	$⊢ (⊤ \land x \in S) \to i x i = i i x$
94		ixi	$⊢ i i = - 1$
95	94	oveq1i	$⊢ i i x = -1 x$
96	12	mulm1d	$⊢ (⊤ \land x \in S) \to -1 x = - x$
97	95 96	syl5eq	$⊢ (⊤ \land x \in S) \to i i x = - x$
98	93 97	eqtrd	$⊢ (⊤ \land x \in S) \to i x i = - x$
99	92 98	oveq12d	$⊢ (⊤ \land x \in S) \to 1 i - i x i = i - (- x)$
100		subneg	$⊢ (i \in ℂ \land x \in ℂ) \to i - (- x) = i + x$
101	6 12 100	sylancr	$⊢ (⊤ \land x \in S) \to i - (- x) = i + x$
102	90 99 101	3eqtrd	$⊢ (⊤ \land x \in S) \to (1 - i x) i = i + x$
103	83 12 102	comraddd	$⊢ (⊤ \land x \in S) \to (1 - i x) i = x + i$
104	103	oveq2d	$⊢ (⊤ \land x \in S) \to \frac{1}{(1 - i x) i} = \frac{1}{x + i}$
105	86 88 104	3eqtr3d	$⊢ (⊤ \land x \in S) \to (\frac{1}{1 - i x}) (\frac{1}{i}) = \frac{1}{x + i}$
106	82 105	eqtr3id	$⊢ (⊤ \land x \in S) \to (\frac{1}{1 - i x}) (- i) = \frac{1}{x + i}$
107	106	mpteq2dva	$⊢ ⊤ \to (x \in S ⟼ (\frac{1}{1 - i x}) (- i)) = (x \in S ⟼ \frac{1}{x + i})$
108	80 107	eqtrd	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 - i x))}{d_{ℂ} x} = (x \in S ⟼ \frac{1}{x + i})$
109		ovexd	$⊢ (⊤ \land x \in S) \to \frac{1}{x - i} \in V$
110	26	simp3bi	$⊢ x \in S \to 1 + i x \in D$
111	110	adantl	$⊢ (⊤ \land x \in S) \to 1 + i x \in D$
112	5 42 19	sylancr	$⊢ (⊤ \land x \in ℂ) \to 1 + i x \in ℂ$
113	4 45 46 48 42 49 55	dvmptadd	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 + i x)}{d_{ℂ} x} = (x \in ℂ ⟼ 0 + i)$
114	6	addid2i	$⊢ 0 + i = i$
115	114	mpteq2i	$⊢ (x \in ℂ ⟼ 0 + i) = (x \in ℂ ⟼ i)$
116	113 115	eqtrdi	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 + i x)}{d_{ℂ} x} = (x \in ℂ ⟼ i)$
117	4 112 49 116 61 64 62 66	dvmptres	$⊢ ⊤ \to \frac{d (x \in S⟼ 1 + i x)}{d_{ℂ} x} = (x \in S ⟼ i)$
118		fveq2	$⊢ y = 1 + i x \to \log y = \log (1 + i x)$
119		oveq2	$⊢ y = 1 + i x \to \frac{1}{y} = \frac{1}{1 + i x}$
120	4 4 111 83 39 40 117 77 118 119	dvmptco	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 + i x))}{d_{ℂ} x} = (x \in S ⟼ (\frac{1}{1 + i x}) i)$
121	89 20 83 21 85	divdiv2d	$⊢ (⊤ \land x \in S) \to \frac{1}{\frac{1 + i x}{i}} = \frac{1 i}{1 + i x}$
122	89 14 83 85	divdird	$⊢ (⊤ \land x \in S) \to \frac{1 + i x}{i} = (\frac{1}{i}) + (\frac{i x}{i})$
123	81	a1i	$⊢ (⊤ \land x \in S) \to \frac{1}{i} = - i$
124	12 83 85	divcan3d	$⊢ (⊤ \land x \in S) \to \frac{i x}{i} = x$
125	123 124	oveq12d	$⊢ (⊤ \land x \in S) \to (\frac{1}{i}) + (\frac{i x}{i}) = - i + x$
126		negicn	$⊢ - i \in ℂ$
127		addcom	$⊢ (- i \in ℂ \land x \in ℂ) \to - i + x = x + (- i)$
128	126 12 127	sylancr	$⊢ (⊤ \land x \in S) \to - i + x = x + (- i)$
129		negsub	$⊢ (x \in ℂ \land i \in ℂ) \to x + (- i) = x - i$
130	12 6 129	sylancl	$⊢ (⊤ \land x \in S) \to x + (- i) = x - i$
131	128 130	eqtrd	$⊢ (⊤ \land x \in S) \to - i + x = x - i$
132	122 125 131	3eqtrd	$⊢ (⊤ \land x \in S) \to \frac{1 + i x}{i} = x - i$
133	132	oveq2d	$⊢ (⊤ \land x \in S) \to \frac{1}{\frac{1 + i x}{i}} = \frac{1}{x - i}$
134	89 83 20 21	div23d	$⊢ (⊤ \land x \in S) \to \frac{1 i}{1 + i x} = (\frac{1}{1 + i x}) i$
135	121 133 134	3eqtr3rd	$⊢ (⊤ \land x \in S) \to (\frac{1}{1 + i x}) i = \frac{1}{x - i}$
136	135	mpteq2dva	$⊢ ⊤ \to (x \in S ⟼ (\frac{1}{1 + i x}) i) = (x \in S ⟼ \frac{1}{x - i})$
137	120 136	eqtrd	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 + i x))}{d_{ℂ} x} = (x \in S ⟼ \frac{1}{x - i})$
138	4 18 25 108 22 109 137	dvmptsub	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 - i x) - \log (1 + i x))}{d_{ℂ} x} = (x \in S ⟼ (\frac{1}{x + i}) - (\frac{1}{x - i}))$
139		subcl	$⊢ (x \in ℂ \land i \in ℂ) \to x - i \in ℂ$
140	12 6 139	sylancl	$⊢ (⊤ \land x \in S) \to x - i \in ℂ$
141		addcl	$⊢ (x \in ℂ \land i \in ℂ) \to x + i \in ℂ$
142	12 6 141	sylancl	$⊢ (⊤ \land x \in S) \to x + i \in ℂ$
143	12	sqcld	$⊢ (⊤ \land x \in S) \to x^{2} \in ℂ$
144		addcl	$⊢ (1 \in ℂ \land x^{2} \in ℂ) \to 1 + x^{2} \in ℂ$
145	5 143 144	sylancr	$⊢ (⊤ \land x \in S) \to 1 + x^{2} \in ℂ$
146		atandm4	$⊢ x \in dom arctan \leftrightarrow (x \in ℂ \land 1 + x^{2} \neq 0)$
147	146	simprbi	$⊢ x \in dom arctan \to 1 + x^{2} \neq 0$
148	9 147	syl	$⊢ (⊤ \land x \in S) \to 1 + x^{2} \neq 0$
149	140 142 145 148	divsubdird	$⊢ (⊤ \land x \in S) \to \frac{x - i - (x + i)}{1 + x^{2}} = (\frac{x - i}{1 + x^{2}}) - (\frac{x + i}{1 + x^{2}})$
150	130	oveq1d	$⊢ (⊤ \land x \in S) \to x + (- i) - (x + i) = x - i - (x + i)$
151	126	a1i	$⊢ (⊤ \land x \in S) \to - i \in ℂ$
152	12 151 83	pnpcand	$⊢ (⊤ \land x \in S) \to x + (- i) - (x + i) = - i - i$
153	150 152	eqtr3d	$⊢ (⊤ \land x \in S) \to x - i - (x + i) = - i - i$
154		2cn	$⊢ 2 \in ℂ$
155	154 6 84	divreci	$⊢ \frac{2}{i} = 2 (\frac{1}{i})$
156	81	oveq2i	$⊢ 2 (\frac{1}{i}) = 2 (- i)$
157	155 156	eqtri	$⊢ \frac{2}{i} = 2 (- i)$
158	126	2timesi	$⊢ 2 (- i) = - i + (- i)$
159	126 6	negsubi	$⊢ - i + (- i) = - i - i$
160	157 158 159	3eqtri	$⊢ \frac{2}{i} = - i - i$
161	153 160	eqtr4di	$⊢ (⊤ \land x \in S) \to x - i - (x + i) = \frac{2}{i}$
162	161	oveq1d	$⊢ (⊤ \land x \in S) \to \frac{x - i - (x + i)}{1 + x^{2}} = \frac{\frac{2}{i}}{1 + x^{2}}$
163	140	mulid1d	$⊢ (⊤ \land x \in S) \to (x - i) \cdot 1 = x - i$
164	140 142	mulcomd	$⊢ (⊤ \land x \in S) \to (x - i) (x + i) = (x + i) (x - i)$
165		i2	$⊢ i^{2} = - 1$
166	165	oveq2i	$⊢ x^{2} - i^{2} = x^{2} - -1$
167		subneg	$⊢ (x^{2} \in ℂ \land 1 \in ℂ) \to x^{2} - -1 = x^{2} + 1$
168	143 5 167	sylancl	$⊢ (⊤ \land x \in S) \to x^{2} - -1 = x^{2} + 1$
169	166 168	syl5eq	$⊢ (⊤ \land x \in S) \to x^{2} - i^{2} = x^{2} + 1$
170		subsq	$⊢ (x \in ℂ \land i \in ℂ) \to x^{2} - i^{2} = (x + i) (x - i)$
171	12 6 170	sylancl	$⊢ (⊤ \land x \in S) \to x^{2} - i^{2} = (x + i) (x - i)$
172		addcom	$⊢ (x^{2} \in ℂ \land 1 \in ℂ) \to x^{2} + 1 = 1 + x^{2}$
173	143 5 172	sylancl	$⊢ (⊤ \land x \in S) \to x^{2} + 1 = 1 + x^{2}$
174	169 171 173	3eqtr3d	$⊢ (⊤ \land x \in S) \to (x + i) (x - i) = 1 + x^{2}$
175	164 174	eqtrd	$⊢ (⊤ \land x \in S) \to (x - i) (x + i) = 1 + x^{2}$
176	163 175	oveq12d	$⊢ (⊤ \land x \in S) \to \frac{(x - i) \cdot 1}{(x - i) (x + i)} = \frac{x - i}{1 + x^{2}}$
177		subneg	$⊢ (x \in ℂ \land i \in ℂ) \to x - (- i) = x + i$
178	12 6 177	sylancl	$⊢ (⊤ \land x \in S) \to x - (- i) = x + i$
179		atandm	$⊢ x \in dom arctan \leftrightarrow (x \in ℂ \land x \neq - i \land x \neq i)$
180	9 179	sylib	$⊢ (⊤ \land x \in S) \to (x \in ℂ \land x \neq - i \land x \neq i)$
181	180	simp2d	$⊢ (⊤ \land x \in S) \to x \neq - i$
182		subeq0	$⊢ (x \in ℂ \land - i \in ℂ) \to (x - (- i) = 0 \leftrightarrow x = - i)$
183	182	necon3bid	$⊢ (x \in ℂ \land - i \in ℂ) \to (x - (- i) \neq 0 \leftrightarrow x \neq - i)$
184	12 126 183	sylancl	$⊢ (⊤ \land x \in S) \to (x - (- i) \neq 0 \leftrightarrow x \neq - i)$
185	181 184	mpbird	$⊢ (⊤ \land x \in S) \to x - (- i) \neq 0$
186	178 185	eqnetrrd	$⊢ (⊤ \land x \in S) \to x + i \neq 0$
187	180	simp3d	$⊢ (⊤ \land x \in S) \to x \neq i$
188		subeq0	$⊢ (x \in ℂ \land i \in ℂ) \to (x - i = 0 \leftrightarrow x = i)$
189	188	necon3bid	$⊢ (x \in ℂ \land i \in ℂ) \to (x - i \neq 0 \leftrightarrow x \neq i)$
190	12 6 189	sylancl	$⊢ (⊤ \land x \in S) \to (x - i \neq 0 \leftrightarrow x \neq i)$
191	187 190	mpbird	$⊢ (⊤ \land x \in S) \to x - i \neq 0$
192	89 142 140 186 191	divcan5d	$⊢ (⊤ \land x \in S) \to \frac{(x - i) \cdot 1}{(x - i) (x + i)} = \frac{1}{x + i}$
193	176 192	eqtr3d	$⊢ (⊤ \land x \in S) \to \frac{x - i}{1 + x^{2}} = \frac{1}{x + i}$
194	142	mulid1d	$⊢ (⊤ \land x \in S) \to (x + i) \cdot 1 = x + i$
195	194 174	oveq12d	$⊢ (⊤ \land x \in S) \to \frac{(x + i) \cdot 1}{(x + i) (x - i)} = \frac{x + i}{1 + x^{2}}$
196	89 140 142 191 186	divcan5d	$⊢ (⊤ \land x \in S) \to \frac{(x + i) \cdot 1}{(x + i) (x - i)} = \frac{1}{x - i}$
197	195 196	eqtr3d	$⊢ (⊤ \land x \in S) \to \frac{x + i}{1 + x^{2}} = \frac{1}{x - i}$
198	193 197	oveq12d	$⊢ (⊤ \land x \in S) \to (\frac{x - i}{1 + x^{2}}) - (\frac{x + i}{1 + x^{2}}) = (\frac{1}{x + i}) - (\frac{1}{x - i})$
199	149 162 198	3eqtr3rd	$⊢ (⊤ \land x \in S) \to (\frac{1}{x + i}) - (\frac{1}{x - i}) = \frac{\frac{2}{i}}{1 + x^{2}}$
200	199	mpteq2dva	$⊢ ⊤ \to (x \in S ⟼ (\frac{1}{x + i}) - (\frac{1}{x - i})) = (x \in S ⟼ \frac{\frac{2}{i}}{1 + x^{2}})$
201	138 200	eqtrd	$⊢ ⊤ \to \frac{d (x \in S⟼ \log (1 - i x) - \log (1 + i x))}{d_{ℂ} x} = (x \in S ⟼ \frac{\frac{2}{i}}{1 + x^{2}})$
202		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
203	6 202	mp1i	$⊢ ⊤ \to \frac{i}{2} \in ℂ$
204	4 23 24 201 203	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in S⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))}{d_{ℂ} x} = (x \in S ⟼ (\frac{i}{2}) (\frac{\frac{2}{i}}{1 + x^{2}}))$
205		df-atan	$⊢ arctan = (x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
206	205	reseq1i	$⊢ {arctan ↾}_{S} = {(x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x))) ↾}_{S}$
207		atanf	$⊢ arctan : ℂ ∖ \{- i, i\} ⟶ ℂ$
208	207	fdmi	$⊢ dom arctan = ℂ ∖ \{- i, i\}$
209	7 208	sseqtri	$⊢ S \subseteq ℂ ∖ \{- i, i\}$
210		resmpt	$⊢ S \subseteq ℂ ∖ \{- i, i\} \to {(x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x))) ↾}_{S} = (x \in S ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
211	209 210	ax-mp	$⊢ {(x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x))) ↾}_{S} = (x \in S ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
212	206 211	eqtri	$⊢ {arctan ↾}_{S} = (x \in S ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
213	212	a1i	$⊢ ⊤ \to {arctan ↾}_{S} = (x \in S ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
214	213	oveq2d	$⊢ ⊤ \to ℂ D ({arctan ↾}_{S}) = \frac{d (x \in S⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))}{d_{ℂ} x}$
215		2ne0	$⊢ 2 \neq 0$
216		divcan6	$⊢ ((i \in ℂ \land i \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{i}{2}) (\frac{2}{i}) = 1$
217	6 84 154 215 216	mp4an	$⊢ (\frac{i}{2}) (\frac{2}{i}) = 1$
218	217	oveq1i	$⊢ \frac{(\frac{i}{2}) (\frac{2}{i})}{1 + x^{2}} = \frac{1}{1 + x^{2}}$
219	6 202	mp1i	$⊢ (⊤ \land x \in S) \to \frac{i}{2} \in ℂ$
220	154 6 84	divcli	$⊢ \frac{2}{i} \in ℂ$
221	220	a1i	$⊢ (⊤ \land x \in S) \to \frac{2}{i} \in ℂ$
222	219 221 145 148	divassd	$⊢ (⊤ \land x \in S) \to \frac{(\frac{i}{2}) (\frac{2}{i})}{1 + x^{2}} = (\frac{i}{2}) (\frac{\frac{2}{i}}{1 + x^{2}})$
223	218 222	eqtr3id	$⊢ (⊤ \land x \in S) \to \frac{1}{1 + x^{2}} = (\frac{i}{2}) (\frac{\frac{2}{i}}{1 + x^{2}})$
224	223	mpteq2dva	$⊢ ⊤ \to (x \in S ⟼ \frac{1}{1 + x^{2}}) = (x \in S ⟼ (\frac{i}{2}) (\frac{\frac{2}{i}}{1 + x^{2}}))$
225	204 214 224	3eqtr4d	$⊢ ⊤ \to ℂ D ({arctan ↾}_{S}) = (x \in S ⟼ \frac{1}{1 + x^{2}})$
226	225	mptru	$⊢ ℂ D ({arctan ↾}_{S}) = (x \in S ⟼ \frac{1}{1 + x^{2}})$

Metamath Proof Explorer

Theorem dvatan

Proof