MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvatan Structured version   Visualization version   GIF version

Theorem dvatan 24953
Description: The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypotheses
Ref Expression
atansopn.d 𝐷 = (ℂ ∖ (-∞(,]0))
atansopn.s 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}
Assertion
Ref Expression
dvatan (ℂ D (arctan ↾ 𝑆)) = (𝑥𝑆 ↦ (1 / (1 + (𝑥↑2))))
Distinct variable groups:   𝑥,𝑦,𝐷   𝑥,𝑆
Allowed substitution hint:   𝑆(𝑦)

Proof of Theorem dvatan
StepHypRef Expression
1 cnelprrecn 10282 . . . . 5 ℂ ∈ {ℝ, ℂ}
21a1i 11 . . . 4 (⊤ → ℂ ∈ {ℝ, ℂ})
3 ax-1cn 10247 . . . . . . 7 1 ∈ ℂ
4 ax-icn 10248 . . . . . . . 8 i ∈ ℂ
5 atansopn.d . . . . . . . . . . . 12 𝐷 = (ℂ ∖ (-∞(,]0))
6 atansopn.s . . . . . . . . . . . 12 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}
75, 6atansssdm 24951 . . . . . . . . . . 11 𝑆 ⊆ dom arctan
8 simpr 477 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → 𝑥𝑆)
97, 8sseldi 3759 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → 𝑥 ∈ dom arctan)
10 atandm2 24895 . . . . . . . . . 10 (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ (1 − (i · 𝑥)) ≠ 0 ∧ (1 + (i · 𝑥)) ≠ 0))
119, 10sylib 209 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (𝑥 ∈ ℂ ∧ (1 − (i · 𝑥)) ≠ 0 ∧ (1 + (i · 𝑥)) ≠ 0))
1211simp1d 1172 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → 𝑥 ∈ ℂ)
13 mulcl 10273 . . . . . . . 8 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
144, 12, 13sylancr 581 . . . . . . 7 ((⊤ ∧ 𝑥𝑆) → (i · 𝑥) ∈ ℂ)
15 subcl 10534 . . . . . . 7 ((1 ∈ ℂ ∧ (i · 𝑥) ∈ ℂ) → (1 − (i · 𝑥)) ∈ ℂ)
163, 14, 15sylancr 581 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 − (i · 𝑥)) ∈ ℂ)
1711simp2d 1173 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 − (i · 𝑥)) ≠ 0)
1816, 17logcld 24608 . . . . 5 ((⊤ ∧ 𝑥𝑆) → (log‘(1 − (i · 𝑥))) ∈ ℂ)
19 addcl 10271 . . . . . . 7 ((1 ∈ ℂ ∧ (i · 𝑥) ∈ ℂ) → (1 + (i · 𝑥)) ∈ ℂ)
203, 14, 19sylancr 581 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 + (i · 𝑥)) ∈ ℂ)
2111simp3d 1174 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 + (i · 𝑥)) ≠ 0)
2220, 21logcld 24608 . . . . 5 ((⊤ ∧ 𝑥𝑆) → (log‘(1 + (i · 𝑥))) ∈ ℂ)
2318, 22subcld 10646 . . . 4 ((⊤ ∧ 𝑥𝑆) → ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))) ∈ ℂ)
24 ovexd 6876 . . . 4 ((⊤ ∧ 𝑥𝑆) → ((2 / i) / (1 + (𝑥↑2))) ∈ V)
25 ovexd 6876 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 / (𝑥 + i)) ∈ V)
265, 6atans2 24949 . . . . . . . . . 10 (𝑥𝑆 ↔ (𝑥 ∈ ℂ ∧ (1 − (i · 𝑥)) ∈ 𝐷 ∧ (1 + (i · 𝑥)) ∈ 𝐷))
2726simp2bi 1176 . . . . . . . . 9 (𝑥𝑆 → (1 − (i · 𝑥)) ∈ 𝐷)
2827adantl 473 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (1 − (i · 𝑥)) ∈ 𝐷)
29 negex 10533 . . . . . . . . 9 -i ∈ V
3029a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → -i ∈ V)
315logdmss 24679 . . . . . . . . . 10 𝐷 ⊆ (ℂ ∖ {0})
32 simpr 477 . . . . . . . . . 10 ((⊤ ∧ 𝑦𝐷) → 𝑦𝐷)
3331, 32sseldi 3759 . . . . . . . . 9 ((⊤ ∧ 𝑦𝐷) → 𝑦 ∈ (ℂ ∖ {0}))
34 logf1o 24602 . . . . . . . . . . 11 log:(ℂ ∖ {0})–1-1-onto→ran log
35 f1of 6320 . . . . . . . . . . 11 (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
3634, 35ax-mp 5 . . . . . . . . . 10 log:(ℂ ∖ {0})⟶ran log
3736ffvelrni 6548 . . . . . . . . 9 (𝑦 ∈ (ℂ ∖ {0}) → (log‘𝑦) ∈ ran log)
38 logrncn 24600 . . . . . . . . 9 ((log‘𝑦) ∈ ran log → (log‘𝑦) ∈ ℂ)
3933, 37, 383syl 18 . . . . . . . 8 ((⊤ ∧ 𝑦𝐷) → (log‘𝑦) ∈ ℂ)
40 ovexd 6876 . . . . . . . 8 ((⊤ ∧ 𝑦𝐷) → (1 / 𝑦) ∈ V)
414a1i 11 . . . . . . . . . . 11 (⊤ → i ∈ ℂ)
4241, 13sylan 575 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
433, 42, 15sylancr 581 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (i · 𝑥)) ∈ ℂ)
4429a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → -i ∈ V)
45 1cnd 10288 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
46 0cnd 10286 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℂ)
47 1cnd 10288 . . . . . . . . . . . 12 (⊤ → 1 ∈ ℂ)
482, 47dvmptc 24012 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
494a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → i ∈ ℂ)
50 simpr 477 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
512dvmptid 24011 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
522, 50, 45, 51, 41dvmptcmul 24018 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i · 1)))
534mulid1i 10298 . . . . . . . . . . . . 13 (i · 1) = i
5453mpteq2i 4900 . . . . . . . . . . . 12 (𝑥 ∈ ℂ ↦ (i · 1)) = (𝑥 ∈ ℂ ↦ i)
5552, 54syl6eq 2815 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i))
562, 45, 46, 48, 42, 49, 55dvmptsub 24021 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ (0 − i)))
57 df-neg 10523 . . . . . . . . . . 11 -i = (0 − i)
5857mpteq2i 4900 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ -i) = (𝑥 ∈ ℂ ↦ (0 − i))
5956, 58syl6eqr 2817 . . . . . . . . 9 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ -i))
60 eqid 2765 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
6160cnfldtopon 22865 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
625, 6atansopn 24950 . . . . . . . . . . 11 𝑆 ∈ (TopOpen‘ℂfld)
63 toponss 21011 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ∈ (TopOpen‘ℂfld)) → 𝑆 ⊆ ℂ)
6461, 62, 63mp2an 683 . . . . . . . . . 10 𝑆 ⊆ ℂ
6564a1i 11 . . . . . . . . 9 (⊤ → 𝑆 ⊆ ℂ)
6661toponrestid 21005 . . . . . . . . 9 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
6762a1i 11 . . . . . . . . 9 (⊤ → 𝑆 ∈ (TopOpen‘ℂfld))
682, 43, 44, 59, 65, 66, 60, 67dvmptres 24017 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝑆 ↦ (1 − (i · 𝑥)))) = (𝑥𝑆 ↦ -i))
69 fssres 6252 . . . . . . . . . . . . . 14 ((log:(ℂ ∖ {0})⟶ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log ↾ 𝐷):𝐷⟶ran log)
7036, 31, 69mp2an 683 . . . . . . . . . . . . 13 (log ↾ 𝐷):𝐷⟶ran log
7170a1i 11 . . . . . . . . . . . 12 (⊤ → (log ↾ 𝐷):𝐷⟶ran log)
7271feqmptd 6438 . . . . . . . . . . 11 (⊤ → (log ↾ 𝐷) = (𝑦𝐷 ↦ ((log ↾ 𝐷)‘𝑦)))
73 fvres 6394 . . . . . . . . . . . 12 (𝑦𝐷 → ((log ↾ 𝐷)‘𝑦) = (log‘𝑦))
7473mpteq2ia 4899 . . . . . . . . . . 11 (𝑦𝐷 ↦ ((log ↾ 𝐷)‘𝑦)) = (𝑦𝐷 ↦ (log‘𝑦))
7572, 74syl6req 2816 . . . . . . . . . 10 (⊤ → (𝑦𝐷 ↦ (log‘𝑦)) = (log ↾ 𝐷))
7675oveq2d 6858 . . . . . . . . 9 (⊤ → (ℂ D (𝑦𝐷 ↦ (log‘𝑦))) = (ℂ D (log ↾ 𝐷)))
775dvlog 24688 . . . . . . . . 9 (ℂ D (log ↾ 𝐷)) = (𝑦𝐷 ↦ (1 / 𝑦))
7876, 77syl6eq 2815 . . . . . . . 8 (⊤ → (ℂ D (𝑦𝐷 ↦ (log‘𝑦))) = (𝑦𝐷 ↦ (1 / 𝑦)))
79 fveq2 6375 . . . . . . . 8 (𝑦 = (1 − (i · 𝑥)) → (log‘𝑦) = (log‘(1 − (i · 𝑥))))
80 oveq2 6850 . . . . . . . 8 (𝑦 = (1 − (i · 𝑥)) → (1 / 𝑦) = (1 / (1 − (i · 𝑥))))
812, 2, 28, 30, 39, 40, 68, 78, 79, 80dvmptco 24026 . . . . . . 7 (⊤ → (ℂ D (𝑥𝑆 ↦ (log‘(1 − (i · 𝑥))))) = (𝑥𝑆 ↦ ((1 / (1 − (i · 𝑥))) · -i)))
82 irec 13171 . . . . . . . . . 10 (1 / i) = -i
8382oveq2i 6853 . . . . . . . . 9 ((1 / (1 − (i · 𝑥))) · (1 / i)) = ((1 / (1 − (i · 𝑥))) · -i)
844a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → i ∈ ℂ)
85 ine0 10719 . . . . . . . . . . . 12 i ≠ 0
8685a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → i ≠ 0)
8716, 84, 17, 86recdiv2d 11073 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((1 / (1 − (i · 𝑥))) / i) = (1 / ((1 − (i · 𝑥)) · i)))
8816, 17reccld 11048 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → (1 / (1 − (i · 𝑥))) ∈ ℂ)
8988, 84, 86divrecd 11058 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((1 / (1 − (i · 𝑥))) / i) = ((1 / (1 − (i · 𝑥))) · (1 / i)))
90 1cnd 10288 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥𝑆) → 1 ∈ ℂ)
9190, 14, 84subdird 10741 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥𝑆) → ((1 − (i · 𝑥)) · i) = ((1 · i) − ((i · 𝑥) · i)))
924mulid2i 10299 . . . . . . . . . . . . . . 15 (1 · i) = i
9392a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥𝑆) → (1 · i) = i)
9484, 12, 84mul32d 10500 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥𝑆) → ((i · 𝑥) · i) = ((i · i) · 𝑥))
95 ixi 10910 . . . . . . . . . . . . . . . . 17 (i · i) = -1
9695oveq1i 6852 . . . . . . . . . . . . . . . 16 ((i · i) · 𝑥) = (-1 · 𝑥)
9712mulm1d 10736 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥𝑆) → (-1 · 𝑥) = -𝑥)
9896, 97syl5eq 2811 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥𝑆) → ((i · i) · 𝑥) = -𝑥)
9994, 98eqtrd 2799 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥𝑆) → ((i · 𝑥) · i) = -𝑥)
10093, 99oveq12d 6860 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥𝑆) → ((1 · i) − ((i · 𝑥) · i)) = (i − -𝑥))
101 subneg 10584 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i − -𝑥) = (i + 𝑥))
1024, 12, 101sylancr 581 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥𝑆) → (i − -𝑥) = (i + 𝑥))
10391, 100, 1023eqtrd 2803 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((1 − (i · 𝑥)) · i) = (i + 𝑥))
104 addcom 10476 . . . . . . . . . . . . 13 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i + 𝑥) = (𝑥 + i))
1054, 12, 104sylancr 581 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → (i + 𝑥) = (𝑥 + i))
106103, 105eqtrd 2799 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((1 − (i · 𝑥)) · i) = (𝑥 + i))
107106oveq2d 6858 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → (1 / ((1 − (i · 𝑥)) · i)) = (1 / (𝑥 + i)))
10887, 89, 1073eqtr3d 2807 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → ((1 / (1 − (i · 𝑥))) · (1 / i)) = (1 / (𝑥 + i)))
10983, 108syl5eqr 2813 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → ((1 / (1 − (i · 𝑥))) · -i) = (1 / (𝑥 + i)))
110109mpteq2dva 4903 . . . . . . 7 (⊤ → (𝑥𝑆 ↦ ((1 / (1 − (i · 𝑥))) · -i)) = (𝑥𝑆 ↦ (1 / (𝑥 + i))))
11181, 110eqtrd 2799 . . . . . 6 (⊤ → (ℂ D (𝑥𝑆 ↦ (log‘(1 − (i · 𝑥))))) = (𝑥𝑆 ↦ (1 / (𝑥 + i))))
112 ovexd 6876 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (1 / (𝑥 − i)) ∈ V)
11326simp3bi 1177 . . . . . . . . 9 (𝑥𝑆 → (1 + (i · 𝑥)) ∈ 𝐷)
114113adantl 473 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (1 + (i · 𝑥)) ∈ 𝐷)
1153, 42, 19sylancr 581 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (1 + (i · 𝑥)) ∈ ℂ)
1162, 45, 46, 48, 42, 49, 55dvmptadd 24014 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 + (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ (0 + i)))
1174addid2i 10478 . . . . . . . . . . 11 (0 + i) = i
118117mpteq2i 4900 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (0 + i)) = (𝑥 ∈ ℂ ↦ i)
119116, 118syl6eq 2815 . . . . . . . . 9 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 + (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ i))
1202, 115, 49, 119, 65, 66, 60, 67dvmptres 24017 . . . . . . . 8 (⊤ → (ℂ D (𝑥𝑆 ↦ (1 + (i · 𝑥)))) = (𝑥𝑆 ↦ i))
121 fveq2 6375 . . . . . . . 8 (𝑦 = (1 + (i · 𝑥)) → (log‘𝑦) = (log‘(1 + (i · 𝑥))))
122 oveq2 6850 . . . . . . . 8 (𝑦 = (1 + (i · 𝑥)) → (1 / 𝑦) = (1 / (1 + (i · 𝑥))))
1232, 2, 114, 84, 39, 40, 120, 78, 121, 122dvmptco 24026 . . . . . . 7 (⊤ → (ℂ D (𝑥𝑆 ↦ (log‘(1 + (i · 𝑥))))) = (𝑥𝑆 ↦ ((1 / (1 + (i · 𝑥))) · i)))
12490, 20, 84, 21, 86divdiv2d 11087 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (1 / ((1 + (i · 𝑥)) / i)) = ((1 · i) / (1 + (i · 𝑥))))
12590, 14, 84, 86divdird 11093 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((1 + (i · 𝑥)) / i) = ((1 / i) + ((i · 𝑥) / i)))
12682a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → (1 / i) = -i)
12712, 84, 86divcan3d 11060 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((i · 𝑥) / i) = 𝑥)
128126, 127oveq12d 6860 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((1 / i) + ((i · 𝑥) / i)) = (-i + 𝑥))
129 negicn 10536 . . . . . . . . . . . . 13 -i ∈ ℂ
130 addcom 10476 . . . . . . . . . . . . 13 ((-i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (-i + 𝑥) = (𝑥 + -i))
131129, 12, 130sylancr 581 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → (-i + 𝑥) = (𝑥 + -i))
132 negsub 10583 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → (𝑥 + -i) = (𝑥 − i))
13312, 4, 132sylancl 580 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → (𝑥 + -i) = (𝑥 − i))
134131, 133eqtrd 2799 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → (-i + 𝑥) = (𝑥 − i))
135125, 128, 1343eqtrd 2803 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((1 + (i · 𝑥)) / i) = (𝑥 − i))
136135oveq2d 6858 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (1 / ((1 + (i · 𝑥)) / i)) = (1 / (𝑥 − i)))
13790, 84, 20, 21div23d 11092 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → ((1 · i) / (1 + (i · 𝑥))) = ((1 / (1 + (i · 𝑥))) · i))
138124, 136, 1373eqtr3rd 2808 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → ((1 / (1 + (i · 𝑥))) · i) = (1 / (𝑥 − i)))
139138mpteq2dva 4903 . . . . . . 7 (⊤ → (𝑥𝑆 ↦ ((1 / (1 + (i · 𝑥))) · i)) = (𝑥𝑆 ↦ (1 / (𝑥 − i))))
140123, 139eqtrd 2799 . . . . . 6 (⊤ → (ℂ D (𝑥𝑆 ↦ (log‘(1 + (i · 𝑥))))) = (𝑥𝑆 ↦ (1 / (𝑥 − i))))
1412, 18, 25, 111, 22, 112, 140dvmptsub 24021 . . . . 5 (⊤ → (ℂ D (𝑥𝑆 ↦ ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) = (𝑥𝑆 ↦ ((1 / (𝑥 + i)) − (1 / (𝑥 − i)))))
142 subcl 10534 . . . . . . . . 9 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → (𝑥 − i) ∈ ℂ)
14312, 4, 142sylancl 580 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (𝑥 − i) ∈ ℂ)
144 addcl 10271 . . . . . . . . 9 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → (𝑥 + i) ∈ ℂ)
14512, 4, 144sylancl 580 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (𝑥 + i) ∈ ℂ)
14612sqcld 13213 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (𝑥↑2) ∈ ℂ)
147 addcl 10271 . . . . . . . . 9 ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 + (𝑥↑2)) ∈ ℂ)
1483, 146, 147sylancr 581 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (1 + (𝑥↑2)) ∈ ℂ)
149 atandm4 24897 . . . . . . . . . 10 (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ (1 + (𝑥↑2)) ≠ 0))
150149simprbi 490 . . . . . . . . 9 (𝑥 ∈ dom arctan → (1 + (𝑥↑2)) ≠ 0)
1519, 150syl 17 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → (1 + (𝑥↑2)) ≠ 0)
152143, 145, 148, 151divsubdird 11094 . . . . . . 7 ((⊤ ∧ 𝑥𝑆) → (((𝑥 − i) − (𝑥 + i)) / (1 + (𝑥↑2))) = (((𝑥 − i) / (1 + (𝑥↑2))) − ((𝑥 + i) / (1 + (𝑥↑2)))))
153133oveq1d 6857 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((𝑥 + -i) − (𝑥 + i)) = ((𝑥 − i) − (𝑥 + i)))
154129a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → -i ∈ ℂ)
15512, 154, 84pnpcand 10683 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((𝑥 + -i) − (𝑥 + i)) = (-i − i))
156153, 155eqtr3d 2801 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) − (𝑥 + i)) = (-i − i))
157 2cn 11347 . . . . . . . . . . . 12 2 ∈ ℂ
158157, 4, 85divreci 11024 . . . . . . . . . . 11 (2 / i) = (2 · (1 / i))
15982oveq2i 6853 . . . . . . . . . . 11 (2 · (1 / i)) = (2 · -i)
160158, 159eqtri 2787 . . . . . . . . . 10 (2 / i) = (2 · -i)
1611292timesi 11417 . . . . . . . . . 10 (2 · -i) = (-i + -i)
162129, 4negsubi 10613 . . . . . . . . . 10 (-i + -i) = (-i − i)
163160, 161, 1623eqtri 2791 . . . . . . . . 9 (2 / i) = (-i − i)
164156, 163syl6eqr 2817 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) − (𝑥 + i)) = (2 / i))
165164oveq1d 6857 . . . . . . 7 ((⊤ ∧ 𝑥𝑆) → (((𝑥 − i) − (𝑥 + i)) / (1 + (𝑥↑2))) = ((2 / i) / (1 + (𝑥↑2))))
166143mulid1d 10311 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) · 1) = (𝑥 − i))
167143, 145mulcomd 10315 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) · (𝑥 + i)) = ((𝑥 + i) · (𝑥 − i)))
168 i2 13172 . . . . . . . . . . . . . 14 (i↑2) = -1
169168oveq2i 6853 . . . . . . . . . . . . 13 ((𝑥↑2) − (i↑2)) = ((𝑥↑2) − -1)
170 subneg 10584 . . . . . . . . . . . . . 14 (((𝑥↑2) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) − -1) = ((𝑥↑2) + 1))
171146, 3, 170sylancl 580 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥𝑆) → ((𝑥↑2) − -1) = ((𝑥↑2) + 1))
172169, 171syl5eq 2811 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((𝑥↑2) − (i↑2)) = ((𝑥↑2) + 1))
173 subsq 13179 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → ((𝑥↑2) − (i↑2)) = ((𝑥 + i) · (𝑥 − i)))
17412, 4, 173sylancl 580 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((𝑥↑2) − (i↑2)) = ((𝑥 + i) · (𝑥 − i)))
175 addcom 10476 . . . . . . . . . . . . 13 (((𝑥↑2) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) + 1) = (1 + (𝑥↑2)))
176146, 3, 175sylancl 580 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((𝑥↑2) + 1) = (1 + (𝑥↑2)))
177172, 174, 1763eqtr3d 2807 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((𝑥 + i) · (𝑥 − i)) = (1 + (𝑥↑2)))
178167, 177eqtrd 2799 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) · (𝑥 + i)) = (1 + (𝑥↑2)))
179166, 178oveq12d 6860 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (((𝑥 − i) · 1) / ((𝑥 − i) · (𝑥 + i))) = ((𝑥 − i) / (1 + (𝑥↑2))))
180 subneg 10584 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → (𝑥 − -i) = (𝑥 + i))
18112, 4, 180sylancl 580 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → (𝑥 − -i) = (𝑥 + i))
182 atandm 24894 . . . . . . . . . . . . . 14 (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ -i ∧ 𝑥 ≠ i))
1839, 182sylib 209 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥𝑆) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ -i ∧ 𝑥 ≠ i))
184183simp2d 1173 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → 𝑥 ≠ -i)
185 subeq0 10561 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ -i ∈ ℂ) → ((𝑥 − -i) = 0 ↔ 𝑥 = -i))
186185necon3bid 2981 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ -i ∈ ℂ) → ((𝑥 − -i) ≠ 0 ↔ 𝑥 ≠ -i))
18712, 129, 186sylancl 580 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − -i) ≠ 0 ↔ 𝑥 ≠ -i))
188184, 187mpbird 248 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → (𝑥 − -i) ≠ 0)
189181, 188eqnetrrd 3005 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → (𝑥 + i) ≠ 0)
190183simp3d 1174 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → 𝑥 ≠ i)
191 subeq0 10561 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → ((𝑥 − i) = 0 ↔ 𝑥 = i))
192191necon3bid 2981 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ i ∈ ℂ) → ((𝑥 − i) ≠ 0 ↔ 𝑥 ≠ i))
19312, 4, 192sylancl 580 . . . . . . . . . . 11 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) ≠ 0 ↔ 𝑥 ≠ i))
194190, 193mpbird 248 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → (𝑥 − i) ≠ 0)
19590, 145, 143, 189, 194divcan5d 11081 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (((𝑥 − i) · 1) / ((𝑥 − i) · (𝑥 + i))) = (1 / (𝑥 + i)))
196179, 195eqtr3d 2801 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → ((𝑥 − i) / (1 + (𝑥↑2))) = (1 / (𝑥 + i)))
197145mulid1d 10311 . . . . . . . . . 10 ((⊤ ∧ 𝑥𝑆) → ((𝑥 + i) · 1) = (𝑥 + i))
198197, 177oveq12d 6860 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (((𝑥 + i) · 1) / ((𝑥 + i) · (𝑥 − i))) = ((𝑥 + i) / (1 + (𝑥↑2))))
19990, 143, 145, 194, 189divcan5d 11081 . . . . . . . . 9 ((⊤ ∧ 𝑥𝑆) → (((𝑥 + i) · 1) / ((𝑥 + i) · (𝑥 − i))) = (1 / (𝑥 − i)))
200198, 199eqtr3d 2801 . . . . . . . 8 ((⊤ ∧ 𝑥𝑆) → ((𝑥 + i) / (1 + (𝑥↑2))) = (1 / (𝑥 − i)))
201196, 200oveq12d 6860 . . . . . . 7 ((⊤ ∧ 𝑥𝑆) → (((𝑥 − i) / (1 + (𝑥↑2))) − ((𝑥 + i) / (1 + (𝑥↑2)))) = ((1 / (𝑥 + i)) − (1 / (𝑥 − i))))
202152, 165, 2013eqtr3rd 2808 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → ((1 / (𝑥 + i)) − (1 / (𝑥 − i))) = ((2 / i) / (1 + (𝑥↑2))))
203202mpteq2dva 4903 . . . . 5 (⊤ → (𝑥𝑆 ↦ ((1 / (𝑥 + i)) − (1 / (𝑥 − i)))) = (𝑥𝑆 ↦ ((2 / i) / (1 + (𝑥↑2)))))
204141, 203eqtrd 2799 . . . 4 (⊤ → (ℂ D (𝑥𝑆 ↦ ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) = (𝑥𝑆 ↦ ((2 / i) / (1 + (𝑥↑2)))))
205 halfcl 11503 . . . . 5 (i ∈ ℂ → (i / 2) ∈ ℂ)
2064, 205mp1i 13 . . . 4 (⊤ → (i / 2) ∈ ℂ)
2072, 23, 24, 204, 206dvmptcmul 24018 . . 3 (⊤ → (ℂ D (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))) = (𝑥𝑆 ↦ ((i / 2) · ((2 / i) / (1 + (𝑥↑2))))))
208 df-atan 24885 . . . . . . 7 arctan = (𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))
209208reseq1i 5561 . . . . . 6 (arctan ↾ 𝑆) = ((𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) ↾ 𝑆)
210 atanf 24898 . . . . . . . . 9 arctan:(ℂ ∖ {-i, i})⟶ℂ
211210fdmi 6233 . . . . . . . 8 dom arctan = (ℂ ∖ {-i, i})
2127, 211sseqtri 3797 . . . . . . 7 𝑆 ⊆ (ℂ ∖ {-i, i})
213 resmpt 5626 . . . . . . 7 (𝑆 ⊆ (ℂ ∖ {-i, i}) → ((𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) ↾ 𝑆) = (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))))
214212, 213ax-mp 5 . . . . . 6 ((𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))) ↾ 𝑆) = (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))
215209, 214eqtri 2787 . . . . 5 (arctan ↾ 𝑆) = (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))
216215a1i 11 . . . 4 (⊤ → (arctan ↾ 𝑆) = (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))))))
217216oveq2d 6858 . . 3 (⊤ → (ℂ D (arctan ↾ 𝑆)) = (ℂ D (𝑥𝑆 ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))))
218 2ne0 11383 . . . . . . 7 2 ≠ 0
219 divcan6 10986 . . . . . . 7 (((i ∈ ℂ ∧ i ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((i / 2) · (2 / i)) = 1)
2204, 85, 157, 218, 219mp4an 684 . . . . . 6 ((i / 2) · (2 / i)) = 1
221220oveq1i 6852 . . . . 5 (((i / 2) · (2 / i)) / (1 + (𝑥↑2))) = (1 / (1 + (𝑥↑2)))
2224, 205mp1i 13 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (i / 2) ∈ ℂ)
223157, 4, 85divcli 11021 . . . . . . 7 (2 / i) ∈ ℂ
224223a1i 11 . . . . . 6 ((⊤ ∧ 𝑥𝑆) → (2 / i) ∈ ℂ)
225222, 224, 148, 151divassd 11090 . . . . 5 ((⊤ ∧ 𝑥𝑆) → (((i / 2) · (2 / i)) / (1 + (𝑥↑2))) = ((i / 2) · ((2 / i) / (1 + (𝑥↑2)))))
226221, 225syl5eqr 2813 . . . 4 ((⊤ ∧ 𝑥𝑆) → (1 / (1 + (𝑥↑2))) = ((i / 2) · ((2 / i) / (1 + (𝑥↑2)))))
227226mpteq2dva 4903 . . 3 (⊤ → (𝑥𝑆 ↦ (1 / (1 + (𝑥↑2)))) = (𝑥𝑆 ↦ ((i / 2) · ((2 / i) / (1 + (𝑥↑2))))))
228207, 217, 2273eqtr4d 2809 . 2 (⊤ → (ℂ D (arctan ↾ 𝑆)) = (𝑥𝑆 ↦ (1 / (1 + (𝑥↑2)))))
229228mptru 1660 1 (ℂ D (arctan ↾ 𝑆)) = (𝑥𝑆 ↦ (1 / (1 + (𝑥↑2))))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1107   = wceq 1652  wtru 1653  wcel 2155  wne 2937  {crab 3059  Vcvv 3350  cdif 3729  wss 3732  {csn 4334  {cpr 4336  cmpt 4888  dom cdm 5277  ran crn 5278  cres 5279  wf 6064  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190  ici 10191   + caddc 10192   · cmul 10194  -∞cmnf 10326  cmin 10520  -cneg 10521   / cdiv 10938  2c2 11327  (,]cioc 12378  cexp 13067  TopOpenctopn 16348  fldccnfld 20019  TopOnctopon 20994   D cdv 23918  logclog 24592  arctancatan 24882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14092  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-limsup 14487  df-clim 14504  df-rlim 14505  df-sum 14702  df-ef 15080  df-sin 15082  df-cos 15083  df-tan 15084  df-pi 15085  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-hom 16238  df-cco 16239  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-pt 16371  df-prds 16374  df-xrs 16428  df-qtop 16433  df-imas 16434  df-xps 16436  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-mulg 17808  df-cntz 18013  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-cmp 21470  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922  df-log 24594  df-atan 24885
This theorem is referenced by:  atancn  24954
  Copyright terms: Public domain W3C validator