Metamath Proof Explorer

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 ffvelrni ⊢ ( 𝑦 ∈ ( ℂ ∖ { 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 mulid1i ⊢ ( 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 mulid2i ⊢ ( 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 syl5eq ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝑆 ) → ( ( 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 addid2i ⊢ ( 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 mulid1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 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 syl5eq ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ↑ 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 mulid1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 + 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 ) ) ) )