Proof of Theorem dvatan
| Step | Hyp | Ref
| Expression |
| 1 | | cnelprrecn 11248 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
| 3 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 4 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 5 | | atansopn.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (ℂ ∖
(-∞(,]0)) |
| 6 | | atansopn.s |
. . . . . . . . . . . 12
⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷} |
| 7 | 5, 6 | atansssdm 26976 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆ dom
arctan |
| 8 | | simpr 484 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 9 | 7, 8 | sselid 3981 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 𝑥 ∈ dom
arctan) |
| 10 | | atandm2 26920 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ (1 −
(i · 𝑥)) ≠ 0
∧ (1 + (i · 𝑥))
≠ 0)) |
| 11 | 9, 10 | sylib 218 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 ∈ ℂ ∧ (1 −
(i · 𝑥)) ≠ 0
∧ (1 + (i · 𝑥))
≠ 0)) |
| 12 | 11 | simp1d 1143 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 𝑥 ∈
ℂ) |
| 13 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
| 14 | 4, 12, 13 | sylancr 587 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (i
· 𝑥) ∈
ℂ) |
| 15 | | subcl 11507 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · 𝑥) ∈ ℂ) → (1 − (i
· 𝑥)) ∈
ℂ) |
| 16 | 3, 14, 15 | sylancr 587 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 −
(i · 𝑥)) ∈
ℂ) |
| 17 | 11 | simp2d 1144 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 −
(i · 𝑥)) ≠
0) |
| 18 | 16, 17 | logcld 26612 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝑆) →
(log‘(1 − (i · 𝑥))) ∈ ℂ) |
| 19 | | addcl 11237 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (i · 𝑥) ∈ ℂ) → (1 + (i ·
𝑥)) ∈
ℂ) |
| 20 | 3, 14, 19 | sylancr 587 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 + (i
· 𝑥)) ∈
ℂ) |
| 21 | 11 | simp3d 1145 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 + (i
· 𝑥)) ≠
0) |
| 22 | 20, 21 | logcld 26612 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝑆) →
(log‘(1 + (i · 𝑥))) ∈ ℂ) |
| 23 | 18, 22 | subcld 11620 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝑆) →
((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥)))) ∈
ℂ) |
| 24 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((2 / i) /
(1 + (𝑥↑2))) ∈
V) |
| 25 | | ovexd 7466 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 /
(𝑥 + i)) ∈
V) |
| 26 | 5, 6 | atans2 26974 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ ℂ ∧ (1 − (i ·
𝑥)) ∈ 𝐷 ∧ (1 + (i · 𝑥)) ∈ 𝐷)) |
| 27 | 26 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → (1 − (i · 𝑥)) ∈ 𝐷) |
| 28 | 27 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 −
(i · 𝑥)) ∈
𝐷) |
| 29 | | negex 11506 |
. . . . . . . . 9
⊢ -i ∈
V |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → -i ∈
V) |
| 31 | 5 | logdmss 26684 |
. . . . . . . . . 10
⊢ 𝐷 ⊆ (ℂ ∖
{0}) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ 𝐷) → 𝑦 ∈ 𝐷) |
| 33 | 31, 32 | sselid 3981 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑦
∈ 𝐷) → 𝑦 ∈ (ℂ ∖
{0})) |
| 34 | | logf1o 26606 |
. . . . . . . . . . 11
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
| 35 | | f1of 6848 |
. . . . . . . . . . 11
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
⊢
log:(ℂ ∖ {0})⟶ran log |
| 37 | 36 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (log‘𝑦) ∈
ran log) |
| 38 | | logrncn 26604 |
. . . . . . . . 9
⊢
((log‘𝑦)
∈ ran log → (log‘𝑦) ∈ ℂ) |
| 39 | 33, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ 𝐷) →
(log‘𝑦) ∈
ℂ) |
| 40 | | ovexd 7466 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑦
∈ 𝐷) → (1 / 𝑦) ∈ V) |
| 41 | 4 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ i ∈ ℂ) |
| 42 | 41, 13 | sylan 580 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
| 43 | 3, 42, 15 | sylancr 587 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 − (i · 𝑥)) ∈ ℂ) |
| 44 | 29 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -i ∈ V) |
| 45 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
| 46 | | 0cnd 11254 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ ℂ) |
| 47 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (⊤
→ 1 ∈ ℂ) |
| 48 | 2, 47 | dvmptc 25996 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 1)) = (𝑥
∈ ℂ ↦ 0)) |
| 49 | 4 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → i ∈ ℂ) |
| 50 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
| 51 | 2 | dvmptid 25995 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
| 52 | 2, 50, 45, 51, 41 | dvmptcmul 26002 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i ·
1))) |
| 53 | 4 | mulridi 11265 |
. . . . . . . . . . . . 13
⊢ (i
· 1) = i |
| 54 | 53 | mpteq2i 5247 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ (i
· 1)) = (𝑥 ∈
ℂ ↦ i) |
| 55 | 52, 54 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i)) |
| 56 | 2, 45, 46, 48, 42, 49, 55 | dvmptsub 26005 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ (0 −
i))) |
| 57 | | df-neg 11495 |
. . . . . . . . . . 11
⊢ -i = (0
− i) |
| 58 | 57 | mpteq2i 5247 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦ -i) =
(𝑥 ∈ ℂ ↦
(0 − i)) |
| 59 | 56, 58 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ -i)) |
| 60 | 6 | ssrab3 4082 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
ℂ |
| 61 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 𝑆 ⊆
ℂ) |
| 62 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 63 | 62 | cnfldtopon 24803 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 64 | 63 | toponrestid 22927 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 65 | 5, 6 | atansopn 26975 |
. . . . . . . . . 10
⊢ 𝑆 ∈
(TopOpen‘ℂfld) |
| 66 | 65 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 𝑆 ∈
(TopOpen‘ℂfld)) |
| 67 | 2, 43, 44, 59, 61, 64, 62, 66 | dvmptres 26001 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (1 − (i
· 𝑥)))) = (𝑥 ∈ 𝑆 ↦ -i)) |
| 68 | | fssres 6774 |
. . . . . . . . . . . . . 14
⊢
((log:(ℂ ∖ {0})⟶ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log
↾ 𝐷):𝐷⟶ran
log) |
| 69 | 36, 31, 68 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (log
↾ 𝐷):𝐷⟶ran log |
| 70 | 69 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ (log ↾ 𝐷):𝐷⟶ran log) |
| 71 | 70 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ (⊤
→ (log ↾ 𝐷) =
(𝑦 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑦))) |
| 72 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐷 → ((log ↾ 𝐷)‘𝑦) = (log‘𝑦)) |
| 73 | 72 | mpteq2ia 5245 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐷 ↦ ((log ↾ 𝐷)‘𝑦)) = (𝑦 ∈ 𝐷 ↦ (log‘𝑦)) |
| 74 | 71, 73 | eqtr2di 2794 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑦 ∈ 𝐷 ↦ (log‘𝑦)) = (log ↾ 𝐷)) |
| 75 | 74 | oveq2d 7447 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑦 ∈
𝐷 ↦ (log‘𝑦))) = (ℂ D (log ↾
𝐷))) |
| 76 | 5 | dvlog 26693 |
. . . . . . . . 9
⊢ (ℂ
D (log ↾ 𝐷)) = (𝑦 ∈ 𝐷 ↦ (1 / 𝑦)) |
| 77 | 75, 76 | eqtrdi 2793 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑦 ∈
𝐷 ↦ (log‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (1 / 𝑦))) |
| 78 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = (1 − (i · 𝑥)) → (log‘𝑦) = (log‘(1 − (i
· 𝑥)))) |
| 79 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = (1 − (i · 𝑥)) → (1 / 𝑦) = (1 / (1 − (i ·
𝑥)))) |
| 80 | 2, 2, 28, 30, 39, 40, 67, 77, 78, 79 | dvmptco 26010 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (log‘(1
− (i · 𝑥)))))
= (𝑥 ∈ 𝑆 ↦ ((1 / (1 − (i
· 𝑥))) ·
-i))) |
| 81 | | irec 14240 |
. . . . . . . . . 10
⊢ (1 / i) =
-i |
| 82 | 81 | oveq2i 7442 |
. . . . . . . . 9
⊢ ((1 / (1
− (i · 𝑥)))
· (1 / i)) = ((1 / (1 − (i · 𝑥))) · -i) |
| 83 | 4 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → i ∈
ℂ) |
| 84 | | ine0 11698 |
. . . . . . . . . . . 12
⊢ i ≠
0 |
| 85 | 84 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → i ≠
0) |
| 86 | 16, 83, 17, 85 | recdiv2d 12061 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / (1
− (i · 𝑥))) /
i) = (1 / ((1 − (i · 𝑥)) · i))) |
| 87 | 16, 17 | reccld 12036 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / (1
− (i · 𝑥)))
∈ ℂ) |
| 88 | 87, 83, 85 | divrecd 12046 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / (1
− (i · 𝑥))) /
i) = ((1 / (1 − (i · 𝑥))) · (1 / i))) |
| 89 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 1 ∈
ℂ) |
| 90 | 89, 14, 83 | subdird 11720 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1
− (i · 𝑥))
· i) = ((1 · i) − ((i · 𝑥) · i))) |
| 91 | 4 | mullidi 11266 |
. . . . . . . . . . . . . . 15
⊢ (1
· i) = i |
| 92 | 91 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1
· i) = i) |
| 93 | 83, 12, 83 | mul32d 11471 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((i
· 𝑥) · i) =
((i · i) · 𝑥)) |
| 94 | | ixi 11892 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· i) = -1 |
| 95 | 94 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢ ((i
· i) · 𝑥) =
(-1 · 𝑥) |
| 96 | 12 | mulm1d 11715 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (-1
· 𝑥) = -𝑥) |
| 97 | 95, 96 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((i
· i) · 𝑥) =
-𝑥) |
| 98 | 93, 97 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((i
· 𝑥) · i) =
-𝑥) |
| 99 | 92, 98 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1
· i) − ((i · 𝑥) · i)) = (i − -𝑥)) |
| 100 | | subneg 11558 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i − -𝑥) = (i + 𝑥)) |
| 101 | 4, 12, 100 | sylancr 587 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (i −
-𝑥) = (i + 𝑥)) |
| 102 | 90, 99, 101 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1
− (i · 𝑥))
· i) = (i + 𝑥)) |
| 103 | 83, 12, 102 | comraddd 11475 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1
− (i · 𝑥))
· i) = (𝑥 +
i)) |
| 104 | 103 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / ((1
− (i · 𝑥))
· i)) = (1 / (𝑥 +
i))) |
| 105 | 86, 88, 104 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / (1
− (i · 𝑥)))
· (1 / i)) = (1 / (𝑥
+ i))) |
| 106 | 82, 105 | eqtr3id 2791 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / (1
− (i · 𝑥)))
· -i) = (1 / (𝑥 +
i))) |
| 107 | 106 | mpteq2dva 5242 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ 𝑆 ↦ ((1 / (1 − (i
· 𝑥))) · -i))
= (𝑥 ∈ 𝑆 ↦ (1 / (𝑥 + i)))) |
| 108 | 80, 107 | eqtrd 2777 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (log‘(1
− (i · 𝑥)))))
= (𝑥 ∈ 𝑆 ↦ (1 / (𝑥 + i)))) |
| 109 | | ovexd 7466 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 /
(𝑥 − i)) ∈
V) |
| 110 | 26 | simp3bi 1148 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → (1 + (i · 𝑥)) ∈ 𝐷) |
| 111 | 110 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 + (i
· 𝑥)) ∈ 𝐷) |
| 112 | 3, 42, 19 | sylancr 587 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 + (i · 𝑥)) ∈ ℂ) |
| 113 | 2, 45, 46, 48, 42, 49, 55 | dvmptadd 25998 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 + (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ (0 +
i))) |
| 114 | 4 | addlidi 11449 |
. . . . . . . . . . 11
⊢ (0 + i) =
i |
| 115 | 114 | mpteq2i 5247 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ ↦ (0 + i))
= (𝑥 ∈ ℂ ↦
i) |
| 116 | 113, 115 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 + (i · 𝑥)))) = (𝑥 ∈ ℂ ↦ i)) |
| 117 | 2, 112, 49, 116, 61, 64, 62, 66 | dvmptres 26001 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (1 + (i ·
𝑥)))) = (𝑥 ∈ 𝑆 ↦ i)) |
| 118 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑦 = (1 + (i · 𝑥)) → (log‘𝑦) = (log‘(1 + (i ·
𝑥)))) |
| 119 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = (1 + (i · 𝑥)) → (1 / 𝑦) = (1 / (1 + (i · 𝑥)))) |
| 120 | 2, 2, 111, 83, 39, 40, 117, 77, 118, 119 | dvmptco 26010 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (log‘(1 +
(i · 𝑥))))) = (𝑥 ∈ 𝑆 ↦ ((1 / (1 + (i · 𝑥))) ·
i))) |
| 121 | 89, 20, 83, 21, 85 | divdiv2d 12075 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / ((1 +
(i · 𝑥)) / i)) = ((1
· i) / (1 + (i · 𝑥)))) |
| 122 | 89, 14, 83, 85 | divdird 12081 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 + (i
· 𝑥)) / i) = ((1 /
i) + ((i · 𝑥) /
i))) |
| 123 | 81 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / i) =
-i) |
| 124 | 12, 83, 85 | divcan3d 12048 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((i
· 𝑥) / i) = 𝑥) |
| 125 | 123, 124 | oveq12d 7449 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / i) +
((i · 𝑥) / i)) = (-i
+ 𝑥)) |
| 126 | | negicn 11509 |
. . . . . . . . . . . . 13
⊢ -i ∈
ℂ |
| 127 | | addcom 11447 |
. . . . . . . . . . . . 13
⊢ ((-i
∈ ℂ ∧ 𝑥
∈ ℂ) → (-i + 𝑥) = (𝑥 + -i)) |
| 128 | 126, 12, 127 | sylancr 587 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (-i +
𝑥) = (𝑥 + -i)) |
| 129 | | negsub 11557 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → (𝑥 + -i) =
(𝑥 −
i)) |
| 130 | 12, 4, 129 | sylancl 586 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 + -i) = (𝑥 − i)) |
| 131 | 128, 130 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (-i +
𝑥) = (𝑥 − i)) |
| 132 | 122, 125,
131 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 + (i
· 𝑥)) / i) = (𝑥 − i)) |
| 133 | 132 | oveq2d 7447 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / ((1 +
(i · 𝑥)) / i)) = (1
/ (𝑥 −
i))) |
| 134 | 89, 83, 20, 21 | div23d 12080 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1
· i) / (1 + (i · 𝑥))) = ((1 / (1 + (i · 𝑥))) ·
i)) |
| 135 | 121, 133,
134 | 3eqtr3rd 2786 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 / (1 +
(i · 𝑥))) ·
i) = (1 / (𝑥 −
i))) |
| 136 | 135 | mpteq2dva 5242 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈ 𝑆 ↦ ((1 / (1 + (i ·
𝑥))) · i)) = (𝑥 ∈ 𝑆 ↦ (1 / (𝑥 − i)))) |
| 137 | 120, 136 | eqtrd 2777 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ (log‘(1 +
(i · 𝑥))))) = (𝑥 ∈ 𝑆 ↦ (1 / (𝑥 − i)))) |
| 138 | 2, 18, 25, 108, 22, 109, 137 | dvmptsub 26005 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥)))))) = (𝑥 ∈ 𝑆 ↦ ((1 / (𝑥 + i)) − (1 / (𝑥 − i))))) |
| 139 | | subcl 11507 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → (𝑥 −
i) ∈ ℂ) |
| 140 | 12, 4, 139 | sylancl 586 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 − i) ∈
ℂ) |
| 141 | | addcl 11237 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → (𝑥 + i)
∈ ℂ) |
| 142 | 12, 4, 141 | sylancl 586 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 + i) ∈
ℂ) |
| 143 | 12 | sqcld 14184 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥↑2) ∈
ℂ) |
| 144 | | addcl 11237 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 + (𝑥↑2)) ∈
ℂ) |
| 145 | 3, 143, 144 | sylancr 587 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 +
(𝑥↑2)) ∈
ℂ) |
| 146 | | atandm4 26922 |
. . . . . . . . . 10
⊢ (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ (1 +
(𝑥↑2)) ≠
0)) |
| 147 | 146 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom arctan → (1 +
(𝑥↑2)) ≠
0) |
| 148 | 9, 147 | syl 17 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 +
(𝑥↑2)) ≠
0) |
| 149 | 140, 142,
145, 148 | divsubdird 12082 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 − i) − (𝑥 + i)) / (1 + (𝑥↑2))) = (((𝑥 − i) / (1 + (𝑥↑2))) − ((𝑥 + i) / (1 + (𝑥↑2))))) |
| 150 | 130 | oveq1d 7446 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 + -i) − (𝑥 + i)) = ((𝑥 − i) − (𝑥 + i))) |
| 151 | 126 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → -i ∈
ℂ) |
| 152 | 12, 151, 83 | pnpcand 11657 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 + -i) − (𝑥 + i)) = (-i −
i)) |
| 153 | 150, 152 | eqtr3d 2779 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) − (𝑥 + i)) = (-i −
i)) |
| 154 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 155 | 154, 4, 84 | divreci 12012 |
. . . . . . . . . . 11
⊢ (2 / i) =
(2 · (1 / i)) |
| 156 | 81 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (2
· (1 / i)) = (2 · -i) |
| 157 | 155, 156 | eqtri 2765 |
. . . . . . . . . 10
⊢ (2 / i) =
(2 · -i) |
| 158 | 126 | 2timesi 12404 |
. . . . . . . . . 10
⊢ (2
· -i) = (-i + -i) |
| 159 | 126, 4 | negsubi 11587 |
. . . . . . . . . 10
⊢ (-i + -i)
= (-i − i) |
| 160 | 157, 158,
159 | 3eqtri 2769 |
. . . . . . . . 9
⊢ (2 / i) =
(-i − i) |
| 161 | 153, 160 | eqtr4di 2795 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) − (𝑥 + i)) = (2 /
i)) |
| 162 | 161 | oveq1d 7446 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 − i) − (𝑥 + i)) / (1 + (𝑥↑2))) = ((2 / i) / (1 +
(𝑥↑2)))) |
| 163 | 140 | mulridd 11278 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) · 1) = (𝑥 − i)) |
| 164 | 140, 142 | mulcomd 11282 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) · (𝑥 + i)) = ((𝑥 + i) · (𝑥 − i))) |
| 165 | | i2 14241 |
. . . . . . . . . . . . . 14
⊢
(i↑2) = -1 |
| 166 | 165 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢ ((𝑥↑2) − (i↑2)) =
((𝑥↑2) −
-1) |
| 167 | | subneg 11558 |
. . . . . . . . . . . . . 14
⊢ (((𝑥↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝑥↑2) − -1) = ((𝑥↑2) + 1)) |
| 168 | 143, 3, 167 | sylancl 586 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥↑2) − -1) = ((𝑥↑2) + 1)) |
| 169 | 166, 168 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥↑2) − (i↑2)) =
((𝑥↑2) +
1)) |
| 170 | | subsq 14249 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → ((𝑥↑2)
− (i↑2)) = ((𝑥 +
i) · (𝑥 −
i))) |
| 171 | 12, 4, 170 | sylancl 586 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥↑2) − (i↑2)) =
((𝑥 + i) · (𝑥 − i))) |
| 172 | | addcom 11447 |
. . . . . . . . . . . . 13
⊢ (((𝑥↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝑥↑2) + 1) = (1 + (𝑥↑2))) |
| 173 | 143, 3, 172 | sylancl 586 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥↑2) + 1) = (1 + (𝑥↑2))) |
| 174 | 169, 171,
173 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 + i) · (𝑥 − i)) = (1 + (𝑥↑2))) |
| 175 | 164, 174 | eqtrd 2777 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) · (𝑥 + i)) = (1 + (𝑥↑2))) |
| 176 | 163, 175 | oveq12d 7449 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 − i) · 1) /
((𝑥 − i) ·
(𝑥 + i))) = ((𝑥 − i) / (1 + (𝑥↑2)))) |
| 177 | | subneg 11558 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → (𝑥 −
-i) = (𝑥 +
i)) |
| 178 | 12, 4, 177 | sylancl 586 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 − -i) = (𝑥 + i)) |
| 179 | | atandm 26919 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ dom arctan ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ -i ∧ 𝑥 ≠ i)) |
| 180 | 9, 179 | sylib 218 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ -i ∧ 𝑥 ≠ i)) |
| 181 | 180 | simp2d 1144 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 𝑥 ≠ -i) |
| 182 | | subeq0 11535 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ -i ∈
ℂ) → ((𝑥 −
-i) = 0 ↔ 𝑥 =
-i)) |
| 183 | 182 | necon3bid 2985 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ -i ∈
ℂ) → ((𝑥 −
-i) ≠ 0 ↔ 𝑥 ≠
-i)) |
| 184 | 12, 126, 183 | sylancl 586 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − -i) ≠ 0 ↔ 𝑥 ≠ -i)) |
| 185 | 181, 184 | mpbird 257 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 − -i) ≠
0) |
| 186 | 178, 185 | eqnetrrd 3009 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 + i) ≠ 0) |
| 187 | 180 | simp3d 1145 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → 𝑥 ≠ i) |
| 188 | | subeq0 11535 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → ((𝑥 −
i) = 0 ↔ 𝑥 =
i)) |
| 189 | 188 | necon3bid 2985 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ i ∈
ℂ) → ((𝑥 −
i) ≠ 0 ↔ 𝑥 ≠
i)) |
| 190 | 12, 4, 189 | sylancl 586 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) ≠ 0 ↔ 𝑥 ≠ i)) |
| 191 | 187, 190 | mpbird 257 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (𝑥 − i) ≠
0) |
| 192 | 89, 142, 140, 186, 191 | divcan5d 12069 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 − i) · 1) /
((𝑥 − i) ·
(𝑥 + i))) = (1 / (𝑥 + i))) |
| 193 | 176, 192 | eqtr3d 2779 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 − i) / (1 + (𝑥↑2))) = (1 / (𝑥 + i))) |
| 194 | 142 | mulridd 11278 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 + i) · 1) = (𝑥 + i)) |
| 195 | 194, 174 | oveq12d 7449 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 + i) · 1) / ((𝑥 + i) · (𝑥 − i))) = ((𝑥 + i) / (1 + (𝑥↑2)))) |
| 196 | 89, 140, 142, 191, 186 | divcan5d 12069 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 + i) · 1) / ((𝑥 + i) · (𝑥 − i))) = (1 / (𝑥 − i))) |
| 197 | 195, 196 | eqtr3d 2779 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((𝑥 + i) / (1 + (𝑥↑2))) = (1 / (𝑥 − i))) |
| 198 | 193, 197 | oveq12d 7449 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((𝑥 − i) / (1 + (𝑥↑2))) − ((𝑥 + i) / (1 + (𝑥↑2)))) = ((1 / (𝑥 + i)) − (1 / (𝑥 − i)))) |
| 199 | 149, 162,
198 | 3eqtr3rd 2786 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → ((1 /
(𝑥 + i)) − (1 /
(𝑥 − i))) = ((2 / i)
/ (1 + (𝑥↑2)))) |
| 200 | 199 | mpteq2dva 5242 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ 𝑆 ↦ ((1 / (𝑥 + i)) − (1 / (𝑥 − i)))) = (𝑥 ∈ 𝑆 ↦ ((2 / i) / (1 + (𝑥↑2))))) |
| 201 | 138, 200 | eqtrd 2777 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥)))))) = (𝑥 ∈ 𝑆 ↦ ((2 / i) / (1 + (𝑥↑2))))) |
| 202 | | halfcl 12491 |
. . . . 5
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
| 203 | 4, 202 | mp1i 13 |
. . . 4
⊢ (⊤
→ (i / 2) ∈ ℂ) |
| 204 | 2, 23, 24, 201, 203 | dvmptcmul 26002 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝑆 ↦ ((i / 2) ·
((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))) = (𝑥 ∈ 𝑆 ↦ ((i / 2) · ((2 / i) / (1 +
(𝑥↑2)))))) |
| 205 | | df-atan 26910 |
. . . . . . 7
⊢ arctan =
(𝑥 ∈ (ℂ ∖
{-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i
· 𝑥)))))) |
| 206 | 205 | reseq1i 5993 |
. . . . . 6
⊢ (arctan
↾ 𝑆) = ((𝑥 ∈ (ℂ ∖ {-i,
i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i
· 𝑥)))))) ↾
𝑆) |
| 207 | | atanf 26923 |
. . . . . . . . 9
⊢
arctan:(ℂ ∖ {-i, i})⟶ℂ |
| 208 | 207 | fdmi 6747 |
. . . . . . . 8
⊢ dom
arctan = (ℂ ∖ {-i, i}) |
| 209 | 7, 208 | sseqtri 4032 |
. . . . . . 7
⊢ 𝑆 ⊆ (ℂ ∖ {-i,
i}) |
| 210 | | resmpt 6055 |
. . . . . . 7
⊢ (𝑆 ⊆ (ℂ ∖ {-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 5 |
. . . . . 6
⊢ ((𝑥 ∈ (ℂ ∖ {-i,
i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i
· 𝑥)))))) ↾
𝑆) = (𝑥 ∈ 𝑆 ↦ ((i / 2) · ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥)))))) |
| 212 | 206, 211 | eqtri 2765 |
. . . . 5
⊢ (arctan
↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ ((i / 2) · ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥)))))) |
| 213 | 212 | a1i 11 |
. . . 4
⊢ (⊤
→ (arctan ↾ 𝑆) =
(𝑥 ∈ 𝑆 ↦ ((i / 2) · ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥))))))) |
| 214 | 213 | oveq2d 7447 |
. . 3
⊢ (⊤
→ (ℂ D (arctan ↾ 𝑆)) = (ℂ D (𝑥 ∈ 𝑆 ↦ ((i / 2) · ((log‘(1
− (i · 𝑥)))
− (log‘(1 + (i · 𝑥)))))))) |
| 215 | | 2ne0 12370 |
. . . . . . 7
⊢ 2 ≠
0 |
| 216 | | divcan6 11974 |
. . . . . . 7
⊢ (((i
∈ ℂ ∧ i ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((i / 2) · (2 / i)) = 1) |
| 217 | 4, 84, 154, 215, 216 | mp4an 693 |
. . . . . 6
⊢ ((i / 2)
· (2 / i)) = 1 |
| 218 | 217 | oveq1i 7441 |
. . . . 5
⊢ (((i / 2)
· (2 / i)) / (1 + (𝑥↑2))) = (1 / (1 + (𝑥↑2))) |
| 219 | 4, 202 | mp1i 13 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (i / 2)
∈ ℂ) |
| 220 | 154, 4, 84 | divcli 12009 |
. . . . . . 7
⊢ (2 / i)
∈ ℂ |
| 221 | 220 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (2 / i)
∈ ℂ) |
| 222 | 219, 221,
145, 148 | divassd 12078 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (((i / 2)
· (2 / i)) / (1 + (𝑥↑2))) = ((i / 2) · ((2 / i) / (1
+ (𝑥↑2))))) |
| 223 | 218, 222 | eqtr3id 2791 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝑆) → (1 / (1 +
(𝑥↑2))) = ((i / 2)
· ((2 / i) / (1 + (𝑥↑2))))) |
| 224 | 223 | mpteq2dva 5242 |
. . 3
⊢ (⊤
→ (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2)))) = (𝑥 ∈ 𝑆 ↦ ((i / 2) · ((2 / i) / (1 +
(𝑥↑2)))))) |
| 225 | 204, 214,
224 | 3eqtr4d 2787 |
. 2
⊢ (⊤
→ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2))))) |
| 226 | 225 | mptru 1547 |
1
⊢ (ℂ
D (arctan ↾ 𝑆)) =
(𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2)))) |