Theorem dvatan

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

	Ref	Expression
Hypotheses	atansopn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
	atansopn.s	⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion	dvatan	⊢ ( ℂ D ( arctan ↾ 𝑆 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 1 / ( 1 + ( 𝑥 ↑ 2 ) ) ) )

Proof

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