Step | Hyp | Ref
| Expression |
1 | | df-asin 26015 |
. . . . 5
⊢ arcsin =
(𝑥 ∈ ℂ ↦
(-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
2 | 1 | reseq1i 5887 |
. . . 4
⊢ (arcsin
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) |
3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
4 | | difss 4066 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
5 | 3, 4 | eqsstri 3955 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
6 | | resmpt 5945 |
. . . . 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 2766 |
. . 3
⊢ (arcsin
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
9 | 8 | oveq2i 7286 |
. 2
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) |
10 | | cnelprrecn 10964 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
12 | 5 | sseli 3917 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
13 | | ax-icn 10930 |
. . . . . . . . 9
⊢ i ∈
ℂ |
14 | | mulcl 10955 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
15 | 13, 14 | mpan 687 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (i
· 𝑥) ∈
ℂ) |
16 | | ax-1cn 10929 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
17 | | sqcl 13838 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
18 | | subcl 11220 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
19 | 16, 17, 18 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
20 | 19 | sqrtcld 15149 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
21 | 15, 20 | addcld 10994 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
22 | 12, 21 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
ℂ) |
23 | | asinlem 26018 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) |
24 | 12, 23 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠
0) |
25 | 22, 24 | logcld 25726 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) |
26 | 25 | adantl 482 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2))))) ∈ ℂ) |
27 | | ovexd 7310 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i /
(√‘(1 − (𝑥↑2)))) ∈ V) |
28 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) |
29 | | asinlem3 26021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) |
30 | | rere 14833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ →
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))) |
31 | 30 | breq2d 5086 |
. . . . . . . . . . . . . . . . . 18
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
32 | 31 | biimpac 479 |
. . . . . . . . . . . . . . . . 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 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) |
35 | 28, 33, 34 | ne0gt0d 11112 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) |
36 | | 0re 10977 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
37 | | ltnle 11054 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
→ (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
38 | 36, 37 | mpan 687 |
. . . . . . . . . . . . . . . 16
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 <
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
40 | 35, 39 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) |
41 | 40 | ex 413 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
42 | 12, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ
→ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
43 | | imor 850 |
. . . . . . . . . . . 12
⊢ ((((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
44 | 42, 43 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
45 | 44 | orcomd 868 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
46 | 45 | olcd 871 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ∨
(¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) |
47 | | 3ianor 1106 |
. . . . . . . . . . 11
⊢ (¬
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0)
↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨
¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
48 | | 3orrot 1091 |
. . . . . . . . . . 11
⊢ ((¬
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
49 | | 3orass 1089 |
. . . . . . . . . . 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 11032 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
52 | | elioc2 13142 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0))) |
53 | 51, 36, 52 | mp2an 689 |
. . . . . . . . . 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 217 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
(-∞(,]0)) |
56 | 22, 55 | eldifd 3898 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ
∖ (-∞(,]0))) |
57 | 56 | adantl 482 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖
(-∞(,]0))) |
58 | | ovexd 7310 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))) ∈
V) |
59 | | eldifi 4061 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
60 | | eldifn 4062 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
61 | | 0xr 11022 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
62 | | mnflt0 12861 |
. . . . . . . . . . . 12
⊢ -∞
< 0 |
63 | | ubioc1 13132 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) |
64 | 51, 61, 62, 63 | mp3an 1460 |
. . . . . . . . . . 11
⊢ 0 ∈
(-∞(,]0) |
65 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
66 | 64, 65 | mpbiri 257 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
67 | 66 | necon3bi 2970 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
68 | 60, 67 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
69 | 59, 68 | logcld 25726 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) |
70 | 69 | adantl 482 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
71 | | ovexd 7310 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
72 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ) |
73 | 72, 12 | mulcld 10995 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ) |
74 | 73 | adantl 482 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i
· 𝑥) ∈
ℂ) |
75 | 13 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → i ∈
ℂ) |
76 | 12 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) |
77 | | 1cnd 10970 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 1 ∈
ℂ) |
78 | | simpr 485 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
79 | | 1cnd 10970 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
80 | 11 | dvmptid 25121 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
81 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
82 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
83 | 82 | cnfldtopon 23946 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
84 | 83 | toponrestid 22070 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
85 | 82 | recld2 23977 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
86 | | neg1rr 12088 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℝ |
87 | | iocmnfcld 23932 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
89 | | 1re 10975 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
90 | | icopnfcld 23931 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
92 | | uncld 22192 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧
(1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) →
((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran
(,)))) |
93 | 88, 91, 92 | mp2an 689 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(topGen‘ran (,))) |
94 | 82 | tgioo2 23966 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
95 | 94 | fveq2i 6777 |
. . . . . . . . . . . . . . . 16
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
96 | 93, 95 | eleqtri 2837 |
. . . . . . . . . . . . . . 15
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
97 | | restcldr 22325 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
98 | 85, 96, 97 | mp2an 689 |
. . . . . . . . . . . . . 14
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
99 | 83 | toponunii 22065 |
. . . . . . . . . . . . . . 15
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
100 | 99 | cldopn 22182 |
. . . . . . . . . . . . . 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 2835 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
103 | 102 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
104 | 11, 78, 79, 80, 81, 84, 82, 103 | dvmptres 25127 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1)) |
105 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ i ∈ ℂ) |
106 | 11, 76, 77, 104, 105 | dvmptcmul 25128 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1))) |
107 | 13 | mulid1i 10979 |
. . . . . . . . . 10
⊢ (i
· 1) = i |
108 | 107 | mpteq2i 5179 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i) |
109 | 106, 108 | eqtrdi 2794 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i)) |
110 | 12 | sqcld 13862 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
111 | 16, 110, 18 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
112 | 111 | sqrtcld 15149 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
113 | 112 | adantl 482 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
114 | | ovexd 7310 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (-𝑥 / (√‘(1 −
(𝑥↑2)))) ∈
V) |
115 | | elin 3903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ)) |
116 | 3 | asindmre 35860 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |
117 | 116 | eqimssi 3979 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∩ ℝ) ⊆
(-1(,)1) |
118 | 117 | sseli 3917 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1)) |
119 | 115, 118 | sylbir 234 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1)) |
120 | | incom 4135 |
. . . . . . . . . . . . . . . 16
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩
(0(,)+∞)) |
121 | | pnfxr 11029 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* |
122 | | df-ioc 13084 |
. . . . . . . . . . . . . . . . . 18
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
123 | | df-ioo 13083 |
. . . . . . . . . . . . . . . . . 18
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
124 | | xrltnle 11042 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) |
125 | 122, 123,
124 | ixxdisj 13094 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩
(0(,)+∞)) = ∅) |
126 | 51, 61, 121, 125 | mp3an 1460 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
127 | 120, 126 | eqtri 2766 |
. . . . . . . . . . . . . . 15
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ |
128 | | elioore 13109 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈
ℝ) |
129 | 128 | resqcld 13965 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈
ℝ) |
130 | | resubcl 11285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 −
(𝑥↑2)) ∈
ℝ) |
131 | 89, 129, 130 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ) |
132 | 86 | rexri 11033 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ* |
133 | | 1xr 11034 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
134 | | elioo2 13120 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1))) |
135 | 132, 133,
134 | mp2an 689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1)) |
136 | | recn 10961 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
137 | 136 | abscld 15148 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
138 | 136 | absge0d 15156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 0 ≤
(abs‘𝑥)) |
139 | | 0le1 11498 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ≤
1 |
140 | | lt2sq 13852 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1))
→ ((abs‘𝑥) <
1 ↔ ((abs‘𝑥)↑2) < (1↑2))) |
141 | 89, 139, 140 | mpanr12 702 |
. . . . . . . . . . . . . . . . . . . . . 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 15026 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1))) |
144 | 89, 143 | mpan2 688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ (-1 < 𝑥 ∧
𝑥 <
1))) |
145 | | absresq 15014 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥)↑2) =
(𝑥↑2)) |
146 | | sq1 13912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1↑2) = 1 |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
(1↑2) = 1) |
148 | 145, 147 | breq12d 5087 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ (𝑥↑2) < 1)) |
149 | | resqcl 13844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈
ℝ) |
150 | | posdif 11468 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 −
(𝑥↑2)))) |
151 | 149, 89, 150 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1
− (𝑥↑2)))) |
152 | 148, 151 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ 0 < (1 − (𝑥↑2)))) |
153 | 142, 144,
152 | 3bitr3d 309 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2)))) |
154 | 153 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))) |
155 | 154 | 3impib 1115 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))) |
156 | 135, 155 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → 0 <
(1 − (𝑥↑2))) |
157 | 131, 156 | elrpd 12769 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ+) |
158 | | ioorp 13157 |
. . . . . . . . . . . . . . . 16
⊢
(0(,)+∞) = ℝ+ |
159 | 157, 158 | eleqtrrdi 2850 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
(0(,)+∞)) |
160 | | disjel 4390 |
. . . . . . . . . . . . . . 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 13142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0))) |
164 | 51, 36, 163 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
165 | 164 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
166 | 165 | simp1d 1141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ) |
167 | | resubcl 11285 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 −
(1 − (𝑥↑2)))
∈ ℝ) |
168 | 89, 166, 167 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ) |
169 | | nncan 11250 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1
− (𝑥↑2))) =
(𝑥↑2)) |
170 | 16, 169 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥↑2) ∈ ℂ →
(1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
171 | 170 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥↑2) ∈ ℂ →
((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈
ℝ)) |
172 | 171 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈
ℝ) |
173 | 168, 172 | sylan2 593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (𝑥↑2) ∈ ℝ) |
174 | 166 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ) |
175 | 165 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ≤ 0) |
176 | 175 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0) |
177 | | letr 11069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1
− (𝑥↑2)) ∈
ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 −
(𝑥↑2)) ≤ 0 ∧ 0
≤ 1) → (1 − (𝑥↑2)) ≤ 1)) |
178 | 36, 89, 177 | mp3an23 1452 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1
− (𝑥↑2)) ≤
1)) |
179 | 139, 178 | mpan2i 694 |
. . . . . . . . . . . . . . . . . . . . . 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 11488 |
. . . . . . . . . . . . . . . . . . . . . 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 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2)))) |
184 | 170 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
185 | 183, 184 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (𝑥↑2)) |
186 | 173, 185 | resqrtcld 15129 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
187 | 17, 186 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
188 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
(√‘(𝑥↑2))
∈ ℝ)) |
189 | 187, 188 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
190 | 187 | renegcld 11402 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ) |
191 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
-(√‘(𝑥↑2))
∈ ℝ)) |
192 | 190, 191 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
-(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
193 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑2) = (𝑥↑2) |
194 | | eqsqrtor 15078 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) →
((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
195 | 17, 194 | mpdan 684 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
196 | 193, 195 | mpbii 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))) |
197 | 196 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
∨ 𝑥 =
-(√‘(𝑥↑2)))) |
198 | 189, 192,
197 | mpjaod 857 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → 𝑥
∈ ℝ) |
199 | 198 | stoic1a 1775 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ¬
𝑥 ∈ ℝ) →
¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
200 | 12, 199 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) |
201 | 162, 200 | pm2.61dan 810 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
202 | 111, 201 | eldifd 3898 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖
(-∞(,]0))) |
203 | 202 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 −
(𝑥↑2)) ∈ (ℂ
∖ (-∞(,]0))) |
204 | | 2cnd 12051 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 2 ∈
ℂ) |
205 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
206 | 204, 205 | mulcld 10995 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
207 | 206 | negcld 11319 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → -(2
· 𝑥) ∈
ℂ) |
208 | 207 | adantl 482 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(2 · 𝑥) ∈ ℂ) |
209 | 12, 208 | sylan2 593 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → -(2
· 𝑥) ∈
ℂ) |
210 | 59 | sqrtcld 15149 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (√‘𝑦) ∈ ℂ) |
211 | 210 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈
ℂ) |
212 | | ovexd 7310 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 ·
(√‘𝑦))) ∈
V) |
213 | 19 | adantl 482 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ) |
214 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ ℝ) |
215 | | 1cnd 10970 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 1 ∈ ℂ) |
216 | 11, 215 | dvmptc 25122 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 1)) = (𝑥
∈ ℂ ↦ 0)) |
217 | 17 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
218 | | 2cn 12048 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
219 | | mulcl 10955 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
220 | 218, 219 | mpan 687 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
221 | 220 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
222 | | 2nn 12046 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
223 | | dvexp 25117 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
224 | 222, 223 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) |
225 | | 2m1e1 12099 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
226 | 225 | oveq2i 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
227 | | exp1 13788 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
228 | 226, 227 | eqtrid 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥) |
229 | 228 | oveq2d 7291 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (2
· (𝑥↑(2 −
1))) = (2 · 𝑥)) |
230 | 229 | mpteq2ia 5177 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) = (𝑥 ∈ ℂ
↦ (2 · 𝑥)) |
231 | 224, 230 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· 𝑥)) |
232 | 231 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) |
233 | 11, 79, 214, 216, 217, 221, 232 | dvmptsub 25131 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2
· 𝑥)))) |
234 | | df-neg 11208 |
. . . . . . . . . . . . 13
⊢ -(2
· 𝑥) = (0 − (2
· 𝑥)) |
235 | 234 | mpteq2i 5179 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ -(2
· 𝑥)) = (𝑥 ∈ ℂ ↦ (0
− (2 · 𝑥))) |
236 | 233, 235 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥))) |
237 | 11, 213, 208, 236, 81, 84, 82, 103 | dvmptres 25127 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥))) |
238 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
239 | 238 | dvcnsqrt 25897 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦)))) |
240 | 239 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦))))) |
241 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) →
(√‘𝑦) =
(√‘(1 − (𝑥↑2)))) |
242 | 241 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 − (𝑥↑2)) → (2 ·
(√‘𝑦)) = (2
· (√‘(1 − (𝑥↑2))))) |
243 | 242 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2
· (√‘𝑦))) = (1 / (2 · (√‘(1
− (𝑥↑2)))))) |
244 | 11, 11, 203, 209, 211, 212, 237, 240, 241, 243 | dvmptco 25136 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))) |
245 | | mulneg2 11412 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥)) |
246 | 218, 12, 245 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥)) |
247 | 246 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-(2
· 𝑥) / (2 ·
(√‘(1 − (𝑥↑2)))))) |
248 | 12 | negcld 11319 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ) |
249 | | eldifn 4062 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
250 | 249, 3 | eleq2s 2857 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
251 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = -1 → 𝑥 = -1) |
252 | | mnflt 12859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-1
∈ ℝ → -∞ < -1) |
253 | 86, 252 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
< -1 |
254 | | ubioc1 13132 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
255 | 51, 132, 253, 254 | mp3an 1460 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
(-∞(,]-1) |
256 | 251, 255 | eqeltrdi 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
257 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → 𝑥 = 1) |
258 | | ltpnf 12856 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
259 | 89, 258 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
260 | | lbico1 13133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
261 | 133, 121,
259, 260 | mp3an 1460 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
(1[,)+∞) |
262 | 257, 261 | eqeltrdi 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
263 | 256, 262 | orim12i 906 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
264 | 263 | orcoms 869 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
265 | | elun 4083 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
266 | 264, 265 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
267 | 250, 266 | nsyl 140 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
268 | | 1cnd 10970 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
269 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
270 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
271 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
272 | 270, 271 | sqr00d 15153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
273 | 268, 269,
272 | subeq0d 11340 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
274 | 146, 273 | eqtr2id 2791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
275 | 274 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
276 | | sqeqor 13932 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
277 | 16, 276 | mpan2 688 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
278 | 275, 277 | sylibd 238 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) |
279 | 278 | necon3bd 2957 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) |
280 | 12, 267, 279 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) |
281 | | 2cnne0 12183 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
282 | | divcan5 11677 |
. . . . . . . . . . . . 13
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
283 | 281, 282 | mp3an3 1449 |
. . . . . . . . . . . 12
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 ·
-𝑥) / (2 ·
(√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2))))) |
284 | 248, 112,
280, 283 | syl12anc 834 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
285 | 218, 12, 219 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ) |
286 | 285 | negcld 11319 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ) |
287 | | mulcl 10955 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
288 | 218, 112,
287 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2))))
∈ ℂ) |
289 | | mulne0 11617 |
. . . . . . . . . . . . . 14
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) |
290 | 281, 289 | mpan 687 |
. . . . . . . . . . . . 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 11755 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = ((1 / (2
· (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) |
293 | 247, 284,
292 | 3eqtr3rd 2787 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)) =
(-𝑥 / (√‘(1
− (𝑥↑2))))) |
294 | 293 | mpteq2ia 5177 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))
= (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))) |
295 | 244, 294 | eqtrdi 2794 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))) |
296 | 11, 74, 75, 109, 113, 114, 295 | dvmptadd 25124 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))) |
297 | | mulcl 10955 |
. . . . . . . . . . . 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 11789 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) =
(((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 −
(𝑥↑2)))) + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
301 | | ixi 11604 |
. . . . . . . . . . . . . . . 16
⊢ (i
· i) = -1 |
302 | 301 | eqcomi 2747 |
. . . . . . . . . . . . . . 15
⊢ -1 = (i
· i) |
303 | 302 | oveq1i 7285 |
. . . . . . . . . . . . . 14
⊢ (-1
· 𝑥) = ((i ·
i) · 𝑥) |
304 | | mulm1 11416 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (-1
· 𝑥) = -𝑥) |
305 | | mulass 10959 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i)
· 𝑥) = (i ·
(i · 𝑥))) |
306 | 13, 13, 305 | mp3an12 1450 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((i
· i) · 𝑥) =
(i · (i · 𝑥))) |
307 | 303, 304,
306 | 3eqtr3a 2802 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥))) |
308 | 307 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1
− (𝑥↑2))))) =
((i · (i · 𝑥)) + (i · (√‘(1 −
(𝑥↑2)))))) |
309 | | negcl 11221 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) |
310 | 298, 309 | addcomd 11177 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 −
(𝑥↑2)))))) |
311 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → i ∈
ℂ) |
312 | 311, 15, 20 | adddid 10999 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i ·
(√‘(1 − (𝑥↑2)))))) |
313 | 308, 310,
312 | 3eqtr4d 2788 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))))) |
314 | 12, 313 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) = (i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
315 | 314 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) = ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
316 | 72, 112, 280 | divcan4d 11757 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) = i) |
317 | 316 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
318 | 300, 315,
317 | 3eqtr3rd 2787 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
319 | 318 | mpteq2ia 5177 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2))))) |
320 | 296, 319 | eqtrdi 2794 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2)))))) |
321 | | logf1o 25720 |
. . . . . . . . . 10
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
322 | | f1of 6716 |
. . . . . . . . . 10
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
323 | 321, 322 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
324 | | snssi 4741 |
. . . . . . . . . . 11
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) |
325 | 64, 324 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ (-∞(,]0) |
326 | | sscon 4073 |
. . . . . . . . . 10
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
327 | 325, 326 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
328 | 323, 327 | feqresmpt 6838 |
. . . . . . . 8
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
329 | 328 | oveq2d 7291 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) |
330 | 238 | dvlog 25806 |
. . . . . . 7
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
331 | 329, 330 | eqtr3di 2793 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
332 | | fveq2 6774 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) →
(log‘𝑦) =
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))) |
333 | | oveq2 7283 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) → (1 /
𝑦) = (1 / ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) |
334 | 11, 11, 57, 58, 70, 71, 320, 331, 332, 333 | dvmptco 25136 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))))) |
335 | 22, 24 | reccld 11744 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) |
336 | | mulcl 10955 |
. . . . . . . . . 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 11786 |
. . . . . . 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 11755 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
341 | 72, 22, 24 | divcan4d 11757 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = i) |
342 | 340, 341 | eqtr3d 2780 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) = i) |
343 | 342 | oveq1d 7290 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = (i /
(√‘(1 − (𝑥↑2))))) |
344 | 339, 343 | eqtr3d 2780 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) = (i /
(√‘(1 − (𝑥↑2))))) |
345 | 344 | mpteq2ia 5177 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2))))) |
346 | 334, 345 | eqtrdi 2794 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2)))))) |
347 | | negicn 11222 |
. . . . 5
⊢ -i ∈
ℂ |
348 | 347 | a1i 11 |
. . . 4
⊢ (⊤
→ -i ∈ ℂ) |
349 | 11, 26, 27, 346, 348 | dvmptcmul 25128 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2))))))) |
350 | 349 | mptru 1546 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) |
351 | | divass 11651 |
. . . . . 6
⊢ ((-i
∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) |
352 | 347, 13, 351 | mp3an12 1450 |
. . . . 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 11421 |
. . . . . 6
⊢ (-i
· i) = -(i · i) |
355 | 301 | negeqi 11214 |
. . . . . 6
⊢ -(i
· i) = --1 |
356 | | negneg1e1 12091 |
. . . . . 6
⊢ --1 =
1 |
357 | 354, 355,
356 | 3eqtri 2770 |
. . . . 5
⊢ (-i
· i) = 1 |
358 | 357 | oveq1i 7285 |
. . . 4
⊢ ((-i
· i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 −
(𝑥↑2)))) |
359 | 353, 358 | eqtr3di 2793 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1
− (𝑥↑2))))) = (1
/ (√‘(1 − (𝑥↑2))))) |
360 | 359 | mpteq2ia 5177 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
361 | 9, 350, 360 | 3eqtri 2770 |
1
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |