| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-asin 26908 | . . . . 5
⊢ arcsin =
(𝑥 ∈ ℂ ↦
(-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) | 
| 2 | 1 | reseq1i 5993 | . . . 4
⊢ (arcsin
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) | 
| 3 |  | dvasin.d | . . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) | 
| 4 |  | difss 4136 | . . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ | 
| 5 | 3, 4 | eqsstri 4030 | . . . . 5
⊢ 𝐷 ⊆
ℂ | 
| 6 |  | resmpt 6055 | . . . . 5
⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))))) | 
| 7 | 5, 6 | ax-mp 5 | . . . 4
⊢ ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) | 
| 8 | 2, 7 | eqtri 2765 | . . 3
⊢ (arcsin
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) | 
| 9 | 8 | oveq2i 7442 | . 2
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) | 
| 10 |  | cnelprrecn 11248 | . . . . 5
⊢ ℂ
∈ {ℝ, ℂ} | 
| 11 | 10 | a1i 11 | . . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) | 
| 12 | 5 | sseli 3979 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) | 
| 13 |  | ax-icn 11214 | . . . . . . . . 9
⊢ i ∈
ℂ | 
| 14 |  | mulcl 11239 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) | 
| 15 | 13, 14 | mpan 690 | . . . . . . . 8
⊢ (𝑥 ∈ ℂ → (i
· 𝑥) ∈
ℂ) | 
| 16 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 17 |  | sqcl 14158 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) | 
| 18 |  | subcl 11507 | . . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) | 
| 19 | 16, 17, 18 | sylancr 587 | . . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) | 
| 20 | 19 | sqrtcld 15476 | . . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(√‘(1 − (𝑥↑2))) ∈ ℂ) | 
| 21 | 15, 20 | addcld 11280 | . . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℂ) | 
| 22 | 12, 21 | syl 17 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
ℂ) | 
| 23 |  | asinlem 26911 | . . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) | 
| 24 | 12, 23 | syl 17 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠
0) | 
| 25 | 22, 24 | logcld 26612 | . . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) | 
| 26 | 25 | adantl 481 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2))))) ∈ ℂ) | 
| 27 |  | ovexd 7466 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i /
(√‘(1 − (𝑥↑2)))) ∈ V) | 
| 28 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) | 
| 29 |  | asinlem3 26914 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) | 
| 30 |  | rere 15161 | . . . . . . . . . . . . . . . . . . 19
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ →
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))) | 
| 31 | 30 | breq2d 5155 | . . . . . . . . . . . . . . . . . 18
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) | 
| 32 | 31 | biimpac 478 | . . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) | 
| 33 | 29, 32 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) | 
| 34 | 23 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) | 
| 35 | 28, 33, 34 | ne0gt0d 11398 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) | 
| 36 |  | 0re 11263 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ | 
| 37 |  | ltnle 11340 | . . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
→ (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) | 
| 38 | 36, 37 | mpan 690 | . . . . . . . . . . . . . . . 16
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) | 
| 39 | 38 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 <
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) | 
| 40 | 35, 39 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) | 
| 41 | 40 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) | 
| 42 | 12, 41 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ
→ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) | 
| 43 |  | imor 854 | . . . . . . . . . . . 12
⊢ ((((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) | 
| 44 | 42, 43 | sylib 218 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) | 
| 45 | 44 | orcomd 872 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) | 
| 46 | 45 | olcd 875 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ∨
(¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) | 
| 47 |  | 3ianor 1107 | . . . . . . . . . . 11
⊢ (¬
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0)
↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨
¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) | 
| 48 |  | 3orrot 1092 | . . . . . . . . . . 11
⊢ ((¬
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) | 
| 49 |  | 3orass 1090 | . . . . . . . . . . 11
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) | 
| 50 | 47, 48, 49 | 3bitrri 298 | . . . . . . . . . 10
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ≤
0)) | 
| 51 |  | mnfxr 11318 | . . . . . . . . . . 11
⊢ -∞
∈ ℝ* | 
| 52 |  | elioc2 13450 | . . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0))) | 
| 53 | 51, 36, 52 | mp2an 692 | . . . . . . . . . 10
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) | 
| 54 | 50, 53 | xchbinxr 335 | . . . . . . . . 9
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
(-∞(,]0)) | 
| 55 | 46, 54 | sylib 218 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
(-∞(,]0)) | 
| 56 | 22, 55 | eldifd 3962 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ
∖ (-∞(,]0))) | 
| 57 | 56 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖
(-∞(,]0))) | 
| 58 |  | ovexd 7466 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))) ∈
V) | 
| 59 |  | eldifi 4131 | . . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) | 
| 60 |  | eldifn 4132 | . . . . . . . . 9
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) | 
| 61 |  | 0xr 11308 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ* | 
| 62 |  | mnflt0 13167 | . . . . . . . . . . . 12
⊢ -∞
< 0 | 
| 63 |  | ubioc1 13440 | . . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) | 
| 64 | 51, 61, 62, 63 | mp3an 1463 | . . . . . . . . . . 11
⊢ 0 ∈
(-∞(,]0) | 
| 65 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) | 
| 66 | 64, 65 | mpbiri 258 | . . . . . . . . . 10
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) | 
| 67 | 66 | necon3bi 2967 | . . . . . . . . 9
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) | 
| 68 | 60, 67 | syl 17 | . . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) | 
| 69 | 59, 68 | logcld 26612 | . . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) | 
| 70 | 69 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) | 
| 71 |  | ovexd 7466 | . . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) | 
| 72 | 13 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ) | 
| 73 | 72, 12 | mulcld 11281 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ) | 
| 74 | 73 | adantl 481 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i
· 𝑥) ∈
ℂ) | 
| 75 | 13 | a1i 11 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → i ∈
ℂ) | 
| 76 | 12 | adantl 481 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) | 
| 77 |  | 1cnd 11256 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 1 ∈
ℂ) | 
| 78 |  | simpr 484 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) | 
| 79 |  | 1cnd 11256 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) | 
| 80 | 11 | dvmptid 25995 | . . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) | 
| 81 | 5 | a1i 11 | . . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ⊆
ℂ) | 
| 82 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 83 | 82 | cnfldtopon 24803 | . . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 84 | 83 | toponrestid 22927 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 85 | 82 | recld2 24836 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) | 
| 86 |  | neg1rr 12381 | . . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℝ | 
| 87 |  | iocmnfcld 24789 | . . . . . . . . . . . . . . . . . 18
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) | 
| 88 | 86, 87 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) | 
| 89 |  | 1re 11261 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ | 
| 90 |  | icopnfcld 24788 | . . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) | 
| 91 | 89, 90 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) | 
| 92 |  | uncld 23049 | . . . . . . . . . . . . . . . . 17
⊢
(((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧
(1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) →
((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran
(,)))) | 
| 93 | 88, 91, 92 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(topGen‘ran (,))) | 
| 94 |  | tgioo4 24826 | . . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 95 | 94 | fveq2i 6909 | . . . . . . . . . . . . . . . 16
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 96 | 93, 95 | eleqtri 2839 | . . . . . . . . . . . . . . 15
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 97 |  | restcldr 23182 | . . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) | 
| 98 | 85, 96, 97 | mp2an 692 | . . . . . . . . . . . . . 14
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) | 
| 99 | 83 | toponunii 22922 | . . . . . . . . . . . . . . 15
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 100 | 99 | cldopn 23039 | . . . . . . . . . . . . . 14
⊢
(((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld)) | 
| 101 | 98, 100 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld) | 
| 102 | 3, 101 | eqeltri 2837 | . . . . . . . . . . . 12
⊢ 𝐷 ∈
(TopOpen‘ℂfld) | 
| 103 | 102 | a1i 11 | . . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) | 
| 104 | 11, 78, 79, 80, 81, 84, 82, 103 | dvmptres 26001 | . . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1)) | 
| 105 | 13 | a1i 11 | . . . . . . . . . 10
⊢ (⊤
→ i ∈ ℂ) | 
| 106 | 11, 76, 77, 104, 105 | dvmptcmul 26002 | . . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1))) | 
| 107 | 13 | mulridi 11265 | . . . . . . . . . 10
⊢ (i
· 1) = i | 
| 108 | 107 | mpteq2i 5247 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i) | 
| 109 | 106, 108 | eqtrdi 2793 | . . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i)) | 
| 110 | 12 | sqcld 14184 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) | 
| 111 | 16, 110, 18 | sylancr 587 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) | 
| 112 | 111 | sqrtcld 15476 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) | 
| 113 | 112 | adantl 481 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(√‘(1 − (𝑥↑2))) ∈ ℂ) | 
| 114 |  | ovexd 7466 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (-𝑥 / (√‘(1 −
(𝑥↑2)))) ∈
V) | 
| 115 |  | elin 3967 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ)) | 
| 116 | 3 | asindmre 37710 | . . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) | 
| 117 | 116 | eqimssi 4044 | . . . . . . . . . . . . . . . 16
⊢ (𝐷 ∩ ℝ) ⊆
(-1(,)1) | 
| 118 | 117 | sseli 3979 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1)) | 
| 119 | 115, 118 | sylbir 235 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1)) | 
| 120 |  | incom 4209 | . . . . . . . . . . . . . . . 16
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩
(0(,)+∞)) | 
| 121 |  | pnfxr 11315 | . . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* | 
| 122 |  | df-ioc 13392 | . . . . . . . . . . . . . . . . . 18
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) | 
| 123 |  | df-ioo 13391 | . . . . . . . . . . . . . . . . . 18
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | 
| 124 |  | xrltnle 11328 | . . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) | 
| 125 | 122, 123,
124 | ixxdisj 13402 | . . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩
(0(,)+∞)) = ∅) | 
| 126 | 51, 61, 121, 125 | mp3an 1463 | . . . . . . . . . . . . . . . 16
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ | 
| 127 | 120, 126 | eqtri 2765 | . . . . . . . . . . . . . . 15
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ | 
| 128 |  | elioore 13417 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈
ℝ) | 
| 129 | 128 | resqcld 14165 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈
ℝ) | 
| 130 |  | resubcl 11573 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 −
(𝑥↑2)) ∈
ℝ) | 
| 131 | 89, 129, 130 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ) | 
| 132 | 86 | rexri 11319 | . . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ* | 
| 133 |  | 1xr 11320 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* | 
| 134 |  | elioo2 13428 | . . . . . . . . . . . . . . . . . . 19
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1))) | 
| 135 | 132, 133,
134 | mp2an 692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1)) | 
| 136 |  | recn 11245 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) | 
| 137 | 136 | abscld 15475 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) | 
| 138 | 136 | absge0d 15483 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 0 ≤
(abs‘𝑥)) | 
| 139 |  | 0le1 11786 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ≤
1 | 
| 140 |  | lt2sq 14173 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1))
→ ((abs‘𝑥) <
1 ↔ ((abs‘𝑥)↑2) < (1↑2))) | 
| 141 | 89, 139, 140 | mpanr12 705 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) <
(1↑2))) | 
| 142 | 137, 138,
141 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ ((abs‘𝑥)↑2) < (1↑2))) | 
| 143 |  | abslt 15353 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1))) | 
| 144 | 89, 143 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ (-1 < 𝑥 ∧
𝑥 <
1))) | 
| 145 |  | absresq 15341 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥)↑2) =
(𝑥↑2)) | 
| 146 |  | sq1 14234 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1↑2) = 1 | 
| 147 | 146 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
(1↑2) = 1) | 
| 148 | 145, 147 | breq12d 5156 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ (𝑥↑2) < 1)) | 
| 149 |  | resqcl 14164 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈
ℝ) | 
| 150 |  | posdif 11756 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 −
(𝑥↑2)))) | 
| 151 | 149, 89, 150 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1
− (𝑥↑2)))) | 
| 152 | 148, 151 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ 0 < (1 − (𝑥↑2)))) | 
| 153 | 142, 144,
152 | 3bitr3d 309 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2)))) | 
| 154 | 153 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))) | 
| 155 | 154 | 3impib 1117 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))) | 
| 156 | 135, 155 | sylbi 217 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → 0 <
(1 − (𝑥↑2))) | 
| 157 | 131, 156 | elrpd 13074 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ+) | 
| 158 |  | ioorp 13465 | . . . . . . . . . . . . . . . 16
⊢
(0(,)+∞) = ℝ+ | 
| 159 | 157, 158 | eleqtrrdi 2852 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
(0(,)+∞)) | 
| 160 |  | disjel 4457 | . . . . . . . . . . . . . . 15
⊢
((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 −
(𝑥↑2)) ∈
(0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) | 
| 161 | 127, 159,
160 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (-1(,)1) → ¬ (1
− (𝑥↑2)) ∈
(-∞(,]0)) | 
| 162 | 119, 161 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) | 
| 163 |  | elioc2 13450 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0))) | 
| 164 | 51, 36, 163 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) | 
| 165 | 164 | biimpi 216 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) | 
| 166 | 165 | simp1d 1143 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ) | 
| 167 |  | resubcl 11573 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 −
(1 − (𝑥↑2)))
∈ ℝ) | 
| 168 | 89, 166, 167 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ) | 
| 169 |  | nncan 11538 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1
− (𝑥↑2))) =
(𝑥↑2)) | 
| 170 | 16, 169 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥↑2) ∈ ℂ →
(1 − (1 − (𝑥↑2))) = (𝑥↑2)) | 
| 171 | 170 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥↑2) ∈ ℂ →
((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈
ℝ)) | 
| 172 | 171 | biimpa 476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈
ℝ) | 
| 173 | 168, 172 | sylan2 593 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (𝑥↑2) ∈ ℝ) | 
| 174 | 166 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ) | 
| 175 | 165 | simp3d 1145 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ≤ 0) | 
| 176 | 175 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0) | 
| 177 |  | letr 11355 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1
− (𝑥↑2)) ∈
ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 −
(𝑥↑2)) ≤ 0 ∧ 0
≤ 1) → (1 − (𝑥↑2)) ≤ 1)) | 
| 178 | 36, 89, 177 | mp3an23 1455 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1
− (𝑥↑2)) ≤
1)) | 
| 179 | 139, 178 | mpan2i 697 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤
1)) | 
| 180 | 174, 176,
179 | sylc 65 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1) | 
| 181 |  | subge0 11776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1
− (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) | 
| 182 | 89, 174, 181 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) | 
| 183 | 180, 182 | mpbird 257 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2)))) | 
| 184 | 170 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2)) | 
| 185 | 183, 184 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (𝑥↑2)) | 
| 186 | 173, 185 | resqrtcld 15456 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) | 
| 187 | 17, 186 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) | 
| 188 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
(√‘(𝑥↑2))
∈ ℝ)) | 
| 189 | 187, 188 | syl5ibrcom 247 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) | 
| 190 | 187 | renegcld 11690 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ) | 
| 191 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
-(√‘(𝑥↑2))
∈ ℝ)) | 
| 192 | 190, 191 | syl5ibrcom 247 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
-(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) | 
| 193 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑2) = (𝑥↑2) | 
| 194 |  | eqsqrtor 15405 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) →
((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) | 
| 195 | 17, 194 | mpdan 687 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) | 
| 196 | 193, 195 | mpbii 233 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))) | 
| 197 | 196 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
∨ 𝑥 =
-(√‘(𝑥↑2)))) | 
| 198 | 189, 192,
197 | mpjaod 861 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → 𝑥
∈ ℝ) | 
| 199 | 198 | stoic1a 1772 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ¬
𝑥 ∈ ℝ) →
¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) | 
| 200 | 12, 199 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) | 
| 201 | 162, 200 | pm2.61dan 813 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) | 
| 202 | 111, 201 | eldifd 3962 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖
(-∞(,]0))) | 
| 203 | 202 | adantl 481 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 −
(𝑥↑2)) ∈ (ℂ
∖ (-∞(,]0))) | 
| 204 |  | 2cnd 12344 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 2 ∈
ℂ) | 
| 205 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) | 
| 206 | 204, 205 | mulcld 11281 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) | 
| 207 | 206 | negcld 11607 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → -(2
· 𝑥) ∈
ℂ) | 
| 208 | 207 | adantl 481 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(2 · 𝑥) ∈ ℂ) | 
| 209 | 12, 208 | sylan2 593 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → -(2
· 𝑥) ∈
ℂ) | 
| 210 | 59 | sqrtcld 15476 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (√‘𝑦) ∈ ℂ) | 
| 211 | 210 | adantl 481 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈
ℂ) | 
| 212 |  | ovexd 7466 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 ·
(√‘𝑦))) ∈
V) | 
| 213 | 19 | adantl 481 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ) | 
| 214 | 36 | a1i 11 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ ℝ) | 
| 215 |  | 1cnd 11256 | . . . . . . . . . . . . . 14
⊢ (⊤
→ 1 ∈ ℂ) | 
| 216 | 11, 215 | dvmptc 25996 | . . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 1)) = (𝑥
∈ ℂ ↦ 0)) | 
| 217 | 17 | adantl 481 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) | 
| 218 |  | 2cn 12341 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ | 
| 219 |  | mulcl 11239 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) | 
| 220 | 218, 219 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) | 
| 221 | 220 | adantl 481 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) | 
| 222 |  | 2nn 12339 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ | 
| 223 |  | dvexp 25991 | . . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) | 
| 224 | 222, 223 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) | 
| 225 |  | 2m1e1 12392 | . . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 | 
| 226 | 225 | oveq2i 7442 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) | 
| 227 |  | exp1 14108 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) | 
| 228 | 226, 227 | eqtrid 2789 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥) | 
| 229 | 228 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (2
· (𝑥↑(2 −
1))) = (2 · 𝑥)) | 
| 230 | 229 | mpteq2ia 5245 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) = (𝑥 ∈ ℂ
↦ (2 · 𝑥)) | 
| 231 | 224, 230 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· 𝑥)) | 
| 232 | 231 | a1i 11 | . . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) | 
| 233 | 11, 79, 214, 216, 217, 221, 232 | dvmptsub 26005 | . . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2
· 𝑥)))) | 
| 234 |  | df-neg 11495 | . . . . . . . . . . . . 13
⊢ -(2
· 𝑥) = (0 − (2
· 𝑥)) | 
| 235 | 234 | mpteq2i 5247 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ -(2
· 𝑥)) = (𝑥 ∈ ℂ ↦ (0
− (2 · 𝑥))) | 
| 236 | 233, 235 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥))) | 
| 237 | 11, 213, 208, 236, 81, 84, 82, 103 | dvmptres 26001 | . . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥))) | 
| 238 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) | 
| 239 | 238 | dvcnsqrt 26786 | . . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦)))) | 
| 240 | 239 | a1i 11 | . . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦))))) | 
| 241 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) →
(√‘𝑦) =
(√‘(1 − (𝑥↑2)))) | 
| 242 | 241 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑦 = (1 − (𝑥↑2)) → (2 ·
(√‘𝑦)) = (2
· (√‘(1 − (𝑥↑2))))) | 
| 243 | 242 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2
· (√‘𝑦))) = (1 / (2 · (√‘(1
− (𝑥↑2)))))) | 
| 244 | 11, 11, 203, 209, 211, 212, 237, 240, 241, 243 | dvmptco 26010 | . . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))) | 
| 245 |  | mulneg2 11700 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥)) | 
| 246 | 218, 12, 245 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥)) | 
| 247 | 246 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-(2
· 𝑥) / (2 ·
(√‘(1 − (𝑥↑2)))))) | 
| 248 | 12 | negcld 11607 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ) | 
| 249 |  | eldifn 4132 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) | 
| 250 | 249, 3 | eleq2s 2859 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) | 
| 251 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = -1 → 𝑥 = -1) | 
| 252 |  | mnflt 13165 | . . . . . . . . . . . . . . . . . . . 20
⊢ (-1
∈ ℝ → -∞ < -1) | 
| 253 | 86, 252 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ -∞
< -1 | 
| 254 |  | ubioc1 13440 | . . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) | 
| 255 | 51, 132, 253, 254 | mp3an 1463 | . . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
(-∞(,]-1) | 
| 256 | 251, 255 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) | 
| 257 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → 𝑥 = 1) | 
| 258 |  | ltpnf 13162 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) | 
| 259 | 89, 258 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ | 
| 260 |  | lbico1 13441 | . . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) | 
| 261 | 133, 121,
259, 260 | mp3an 1463 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
(1[,)+∞) | 
| 262 | 257, 261 | eqeltrdi 2849 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) | 
| 263 | 256, 262 | orim12i 909 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) | 
| 264 | 263 | orcoms 873 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) | 
| 265 |  | elun 4153 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) | 
| 266 | 264, 265 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) | 
| 267 | 250, 266 | nsyl 140 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) | 
| 268 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) | 
| 269 | 17 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) | 
| 270 | 19 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) | 
| 271 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) | 
| 272 | 270, 271 | sqr00d 15480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) | 
| 273 | 268, 269,
272 | subeq0d 11628 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) | 
| 274 | 146, 273 | eqtr2id 2790 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) | 
| 275 | 274 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) | 
| 276 |  | sqeqor 14255 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) | 
| 277 | 16, 276 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) | 
| 278 | 275, 277 | sylibd 239 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) | 
| 279 | 278 | necon3bd 2954 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) | 
| 280 | 12, 267, 279 | sylc 65 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) | 
| 281 |  | 2cnne0 12476 | . . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 282 |  | divcan5 11969 | . . . . . . . . . . . . 13
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) | 
| 283 | 281, 282 | mp3an3 1452 | . . . . . . . . . . . 12
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 ·
-𝑥) / (2 ·
(√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2))))) | 
| 284 | 248, 112,
280, 283 | syl12anc 837 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) | 
| 285 | 218, 12, 219 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ) | 
| 286 | 285 | negcld 11607 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ) | 
| 287 |  | mulcl 11239 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) | 
| 288 | 218, 112,
287 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2))))
∈ ℂ) | 
| 289 |  | mulne0 11905 | . . . . . . . . . . . . . 14
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) | 
| 290 | 281, 289 | mpan 690 | . . . . . . . . . . . . 13
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) | 
| 291 | 112, 280,
290 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2)))) ≠
0) | 
| 292 | 286, 288,
291 | divrec2d 12047 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = ((1 / (2
· (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) | 
| 293 | 247, 284,
292 | 3eqtr3rd 2786 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)) =
(-𝑥 / (√‘(1
− (𝑥↑2))))) | 
| 294 | 293 | mpteq2ia 5245 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))
= (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))) | 
| 295 | 244, 294 | eqtrdi 2793 | . . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))) | 
| 296 | 11, 74, 75, 109, 113, 114, 295 | dvmptadd 25998 | . . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))) | 
| 297 |  | mulcl 11239 | . . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) | 
| 298 | 13, 20, 297 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → (i
· (√‘(1 − (𝑥↑2)))) ∈ ℂ) | 
| 299 | 12, 298 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1
− (𝑥↑2))))
∈ ℂ) | 
| 300 | 299, 248,
112, 280 | divdird 12081 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) =
(((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 −
(𝑥↑2)))) + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) | 
| 301 |  | ixi 11892 | . . . . . . . . . . . . . . . 16
⊢ (i
· i) = -1 | 
| 302 | 301 | eqcomi 2746 | . . . . . . . . . . . . . . 15
⊢ -1 = (i
· i) | 
| 303 | 302 | oveq1i 7441 | . . . . . . . . . . . . . 14
⊢ (-1
· 𝑥) = ((i ·
i) · 𝑥) | 
| 304 |  | mulm1 11704 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (-1
· 𝑥) = -𝑥) | 
| 305 |  | mulass 11243 | . . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i)
· 𝑥) = (i ·
(i · 𝑥))) | 
| 306 | 13, 13, 305 | mp3an12 1453 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((i
· i) · 𝑥) =
(i · (i · 𝑥))) | 
| 307 | 303, 304,
306 | 3eqtr3a 2801 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥))) | 
| 308 | 307 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1
− (𝑥↑2))))) =
((i · (i · 𝑥)) + (i · (√‘(1 −
(𝑥↑2)))))) | 
| 309 |  | negcl 11508 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) | 
| 310 | 298, 309 | addcomd 11463 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 −
(𝑥↑2)))))) | 
| 311 | 13 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → i ∈
ℂ) | 
| 312 | 311, 15, 20 | adddid 11285 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i ·
(√‘(1 − (𝑥↑2)))))) | 
| 313 | 308, 310,
312 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))))) | 
| 314 | 12, 313 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) = (i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) | 
| 315 | 314 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) = ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) | 
| 316 | 72, 112, 280 | divcan4d 12049 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) = i) | 
| 317 | 316 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) | 
| 318 | 300, 315,
317 | 3eqtr3rd 2786 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) | 
| 319 | 318 | mpteq2ia 5245 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2))))) | 
| 320 | 296, 319 | eqtrdi 2793 | . . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2)))))) | 
| 321 |  | logf1o 26606 | . . . . . . . . . 10
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log | 
| 322 |  | f1of 6848 | . . . . . . . . . 10
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) | 
| 323 | 321, 322 | mp1i 13 | . . . . . . . . 9
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) | 
| 324 |  | snssi 4808 | . . . . . . . . . . 11
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) | 
| 325 | 64, 324 | ax-mp 5 | . . . . . . . . . 10
⊢ {0}
⊆ (-∞(,]0) | 
| 326 |  | sscon 4143 | . . . . . . . . . 10
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) | 
| 327 | 325, 326 | mp1i 13 | . . . . . . . . 9
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) | 
| 328 | 323, 327 | feqresmpt 6978 | . . . . . . . 8
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) | 
| 329 | 328 | oveq2d 7447 | . . . . . . 7
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) | 
| 330 | 238 | dvlog 26693 | . . . . . . 7
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) | 
| 331 | 329, 330 | eqtr3di 2792 | . . . . . 6
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) | 
| 332 |  | fveq2 6906 | . . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) →
(log‘𝑦) =
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))) | 
| 333 |  | oveq2 7439 | . . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) → (1 /
𝑦) = (1 / ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) | 
| 334 | 11, 11, 57, 58, 70, 71, 320, 331, 332, 333 | dvmptco 26010 | . . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))))) | 
| 335 | 22, 24 | reccld 12036 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) | 
| 336 |  | mulcl 11239 | . . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
→ (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) | 
| 337 | 13, 21, 336 | sylancr 587 | . . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) ∈ ℂ) | 
| 338 | 12, 337 | syl 17 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) | 
| 339 | 335, 338,
112, 280 | divassd 12078 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = ((1 / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) · ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) | 
| 340 | 338, 22, 24 | divrec2d 12047 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))))) | 
| 341 | 72, 22, 24 | divcan4d 12049 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = i) | 
| 342 | 340, 341 | eqtr3d 2779 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) = i) | 
| 343 | 342 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = (i /
(√‘(1 − (𝑥↑2))))) | 
| 344 | 339, 343 | eqtr3d 2779 | . . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) = (i /
(√‘(1 − (𝑥↑2))))) | 
| 345 | 344 | mpteq2ia 5245 | . . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2))))) | 
| 346 | 334, 345 | eqtrdi 2793 | . . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2)))))) | 
| 347 |  | negicn 11509 | . . . . 5
⊢ -i ∈
ℂ | 
| 348 | 347 | a1i 11 | . . . 4
⊢ (⊤
→ -i ∈ ℂ) | 
| 349 | 11, 26, 27, 346, 348 | dvmptcmul 26002 | . . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2))))))) | 
| 350 | 349 | mptru 1547 | . 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) | 
| 351 |  | divass 11940 | . . . . . 6
⊢ ((-i
∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) | 
| 352 | 347, 13, 351 | mp3an12 1453 | . . . . 5
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) | 
| 353 | 112, 280,
352 | syl2anc 584 | . . . 4
⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1
− (𝑥↑2)))) = (-i
· (i / (√‘(1 − (𝑥↑2)))))) | 
| 354 | 13, 13 | mulneg1i 11709 | . . . . . 6
⊢ (-i
· i) = -(i · i) | 
| 355 | 301 | negeqi 11501 | . . . . . 6
⊢ -(i
· i) = --1 | 
| 356 |  | negneg1e1 12384 | . . . . . 6
⊢ --1 =
1 | 
| 357 | 354, 355,
356 | 3eqtri 2769 | . . . . 5
⊢ (-i
· i) = 1 | 
| 358 | 357 | oveq1i 7441 | . . . 4
⊢ ((-i
· i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 −
(𝑥↑2)))) | 
| 359 | 353, 358 | eqtr3di 2792 | . . 3
⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1
− (𝑥↑2))))) = (1
/ (√‘(1 − (𝑥↑2))))) | 
| 360 | 359 | mpteq2ia 5245 | . 2
⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) | 
| 361 | 9, 350, 360 | 3eqtri 2769 | 1
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |