Step | Hyp | Ref
| Expression |
1 | | df-asin 24637 |
. . . . 5
⊢ arcsin =
(𝑥 ∈ ℂ ↦
(-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
2 | 1 | reseq1i 5424 |
. . . 4
⊢ (arcsin
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) |
3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
4 | | difss 3770 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
5 | 3, 4 | eqsstri 3668 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
6 | | resmpt 5484 |
. . . . 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 2673 |
. . 3
⊢ (arcsin
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
9 | 8 | oveq2i 6701 |
. 2
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) |
10 | | cnelprrecn 10067 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
12 | 5 | sseli 3632 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
13 | | ax-icn 10033 |
. . . . . . . . 9
⊢ i ∈
ℂ |
14 | | mulcl 10058 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
15 | 13, 14 | mpan 706 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (i
· 𝑥) ∈
ℂ) |
16 | | ax-1cn 10032 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
17 | | sqcl 12965 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
18 | | subcl 10318 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
19 | 16, 17, 18 | sylancr 696 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
20 | 19 | sqrtcld 14220 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
21 | 15, 20 | addcld 10097 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
22 | 12, 21 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
ℂ) |
23 | | asinlem 24640 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) |
24 | 12, 23 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠
0) |
25 | 22, 24 | logcld 24362 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) |
26 | 25 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2))))) ∈ ℂ) |
27 | | ovexd 6720 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i /
(√‘(1 − (𝑥↑2)))) ∈ V) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) |
29 | | asinlem3 24643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) |
30 | | rere 13906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ →
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))) |
31 | 30 | breq2d 4697 |
. . . . . . . . . . . . . . . . . 18
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
32 | 31 | biimpac 502 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) |
33 | 29, 32 | sylan 487 |
. . . . . . . . . . . . . . . 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 10212 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) |
36 | | 0re 10078 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
37 | | ltnle 10155 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
→ (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
38 | 36, 37 | mpan 706 |
. . . . . . . . . . . . . . . 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 222 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) |
41 | 40 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
42 | 12, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ
→ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
43 | | imor 427 |
. . . . . . . . . . . 12
⊢ ((((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
44 | 42, 43 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
45 | 44 | orcomd 402 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
46 | 45 | olcd 407 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ∨
(¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) |
47 | | 3ianor 1074 |
. . . . . . . . . . 11
⊢ (¬
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0)
↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨
¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
48 | | 3orrot 1061 |
. . . . . . . . . . 11
⊢ ((¬
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
49 | | 3orass 1057 |
. . . . . . . . . . 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 287 |
. . . . . . . . . 10
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ≤
0)) |
51 | | mnfxr 10134 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
52 | | elioc2 12274 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0))) |
53 | 51, 36, 52 | mp2an 708 |
. . . . . . . . . 10
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
54 | 50, 53 | xchbinxr 324 |
. . . . . . . . 9
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
(-∞(,]0)) |
55 | 46, 54 | sylib 208 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
(-∞(,]0)) |
56 | 22, 55 | eldifd 3618 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ
∖ (-∞(,]0))) |
57 | 56 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖
(-∞(,]0))) |
58 | | ovexd 6720 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))) ∈
V) |
59 | | eldifi 3765 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
60 | | eldifn 3766 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
61 | | 0xr 10124 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
62 | | mnflt0 11997 |
. . . . . . . . . . . 12
⊢ -∞
< 0 |
63 | | ubioc1 12265 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) |
64 | 51, 61, 62, 63 | mp3an 1464 |
. . . . . . . . . . 11
⊢ 0 ∈
(-∞(,]0) |
65 | | eleq1 2718 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
66 | 64, 65 | mpbiri 248 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
67 | 66 | necon3bi 2849 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
68 | 60, 67 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
69 | 59, 68 | logcld 24362 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) |
70 | 69 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
71 | | ovexd 6720 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
72 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ) |
73 | 72, 12 | mulcld 10098 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ) |
74 | 73 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i
· 𝑥) ∈
ℂ) |
75 | 13 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → i ∈
ℂ) |
76 | 12 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) |
77 | | 1cnd 10094 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 1 ∈
ℂ) |
78 | | simpr 476 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
79 | | 1cnd 10094 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
80 | 11 | dvmptid 23765 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
81 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
82 | | eqid 2651 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
83 | 82 | cnfldtopon 22633 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
84 | 83 | toponunii 20769 |
. . . . . . . . . . . . . 14
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
85 | 84 | restid 16141 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
86 | 83, 85 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
87 | 86 | eqcomi 2660 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
88 | 82 | recld2 22664 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
89 | | neg1rr 11163 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℝ |
90 | | iocmnfcld 22619 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
92 | | 1re 10077 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
93 | | icopnfcld 22618 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
95 | | uncld 20893 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧
(1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) →
((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran
(,)))) |
96 | 91, 94, 95 | mp2an 708 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(topGen‘ran (,))) |
97 | 82 | tgioo2 22653 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
98 | 97 | fveq2i 6232 |
. . . . . . . . . . . . . . . 16
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
99 | 96, 98 | eleqtri 2728 |
. . . . . . . . . . . . . . 15
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
100 | | restcldr 21026 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
101 | 88, 99, 100 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
102 | 84 | cldopn 20883 |
. . . . . . . . . . . . . 14
⊢
(((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld)) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld) |
104 | 3, 103 | eqeltri 2726 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
106 | 11, 78, 79, 80, 81, 87, 82, 105 | dvmptres 23771 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1)) |
107 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ i ∈ ℂ) |
108 | 11, 76, 77, 106, 107 | dvmptcmul 23772 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1))) |
109 | 13 | mulid1i 10080 |
. . . . . . . . . 10
⊢ (i
· 1) = i |
110 | 109 | mpteq2i 4774 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i) |
111 | 108, 110 | syl6eq 2701 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i)) |
112 | 12 | sqcld 13046 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
113 | 16, 112, 18 | sylancr 696 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
114 | 113 | sqrtcld 14220 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
115 | 114 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
116 | | ovexd 6720 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (-𝑥 / (√‘(1 −
(𝑥↑2)))) ∈
V) |
117 | | elin 3829 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ)) |
118 | 3 | asindmre 33625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |
119 | 118 | eqimssi 3692 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∩ ℝ) ⊆
(-1(,)1) |
120 | 119 | sseli 3632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1)) |
121 | 117, 120 | sylbir 225 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1)) |
122 | | incom 3838 |
. . . . . . . . . . . . . . . 16
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩
(0(,)+∞)) |
123 | | pnfxr 10130 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* |
124 | | df-ioc 12218 |
. . . . . . . . . . . . . . . . . 18
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
125 | | df-ioo 12217 |
. . . . . . . . . . . . . . . . . 18
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
126 | | xrltnle 10143 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) |
127 | 124, 125,
126 | ixxdisj 12228 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩
(0(,)+∞)) = ∅) |
128 | 51, 61, 123, 127 | mp3an 1464 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
129 | 122, 128 | eqtri 2673 |
. . . . . . . . . . . . . . 15
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ |
130 | | elioore 12243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈
ℝ) |
131 | 130 | resqcld 13075 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈
ℝ) |
132 | | resubcl 10383 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 −
(𝑥↑2)) ∈
ℝ) |
133 | 92, 131, 132 | sylancr 696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ) |
134 | 89 | rexri 10135 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ* |
135 | 92 | rexri 10135 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
136 | | elioo2 12254 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1))) |
137 | 134, 135,
136 | mp2an 708 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1)) |
138 | | recn 10064 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
139 | 138 | abscld 14219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
140 | 138 | absge0d 14227 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 0 ≤
(abs‘𝑥)) |
141 | | 0le1 10589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ≤
1 |
142 | | lt2sq 12977 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1))
→ ((abs‘𝑥) <
1 ↔ ((abs‘𝑥)↑2) < (1↑2))) |
143 | 92, 141, 142 | mpanr12 721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) <
(1↑2))) |
144 | 139, 140,
143 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ ((abs‘𝑥)↑2) < (1↑2))) |
145 | | abslt 14098 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1))) |
146 | 92, 145 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ (-1 < 𝑥 ∧
𝑥 <
1))) |
147 | | absresq 14086 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥)↑2) =
(𝑥↑2)) |
148 | | sq1 12998 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1↑2) = 1 |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
(1↑2) = 1) |
150 | 147, 149 | breq12d 4698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ (𝑥↑2) < 1)) |
151 | | resqcl 12971 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈
ℝ) |
152 | | posdif 10559 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 −
(𝑥↑2)))) |
153 | 151, 92, 152 | sylancl 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1
− (𝑥↑2)))) |
154 | 150, 153 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ 0 < (1 − (𝑥↑2)))) |
155 | 144, 146,
154 | 3bitr3d 298 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2)))) |
156 | 155 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))) |
157 | 156 | 3impib 1281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))) |
158 | 137, 157 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → 0 <
(1 − (𝑥↑2))) |
159 | 133, 158 | elrpd 11907 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ+) |
160 | | ioorp 12289 |
. . . . . . . . . . . . . . . 16
⊢
(0(,)+∞) = ℝ+ |
161 | 159, 160 | syl6eleqr 2741 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
(0(,)+∞)) |
162 | | disjel 4056 |
. . . . . . . . . . . . . . 15
⊢
((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 −
(𝑥↑2)) ∈
(0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
163 | 129, 161,
162 | sylancr 696 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (-1(,)1) → ¬ (1
− (𝑥↑2)) ∈
(-∞(,]0)) |
164 | 121, 163 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) |
165 | | elioc2 12274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0))) |
166 | 51, 36, 165 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
167 | 166 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
168 | 167 | simp1d 1093 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ) |
169 | | resubcl 10383 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 −
(1 − (𝑥↑2)))
∈ ℝ) |
170 | 92, 168, 169 | sylancr 696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ) |
171 | | nncan 10348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1
− (𝑥↑2))) =
(𝑥↑2)) |
172 | 16, 171 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥↑2) ∈ ℂ →
(1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
173 | 172 | eleq1d 2715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥↑2) ∈ ℂ →
((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈
ℝ)) |
174 | 173 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈
ℝ) |
175 | 170, 174 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (𝑥↑2) ∈ ℝ) |
176 | 168 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ) |
177 | 167 | simp3d 1095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ≤ 0) |
178 | 177 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0) |
179 | | letr 10169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1
− (𝑥↑2)) ∈
ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 −
(𝑥↑2)) ≤ 0 ∧ 0
≤ 1) → (1 − (𝑥↑2)) ≤ 1)) |
180 | 36, 92, 179 | mp3an23 1456 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1
− (𝑥↑2)) ≤
1)) |
181 | 141, 180 | mpan2i 713 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤
1)) |
182 | 176, 178,
181 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1) |
183 | | subge0 10579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1
− (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) |
184 | 92, 176, 183 | sylancr 696 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) |
185 | 182, 184 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2)))) |
186 | 172 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
187 | 185, 186 | breqtrd 4711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (𝑥↑2)) |
188 | 175, 187 | resqrtcld 14200 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
189 | 17, 188 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
190 | | eleq1 2718 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
(√‘(𝑥↑2))
∈ ℝ)) |
191 | 189, 190 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
192 | 189 | renegcld 10495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ) |
193 | | eleq1 2718 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
-(√‘(𝑥↑2))
∈ ℝ)) |
194 | 192, 193 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
-(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
195 | | eqid 2651 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑2) = (𝑥↑2) |
196 | | eqsqrtor 14150 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) →
((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
197 | 17, 196 | mpdan 703 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
198 | 195, 197 | mpbii 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))) |
199 | 198 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
∨ 𝑥 =
-(√‘(𝑥↑2)))) |
200 | 191, 194,
199 | mpjaod 395 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → 𝑥
∈ ℝ) |
201 | 200 | stoic1a 1737 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ¬
𝑥 ∈ ℝ) →
¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
202 | 12, 201 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) |
203 | 164, 202 | pm2.61dan 849 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
204 | 113, 203 | eldifd 3618 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖
(-∞(,]0))) |
205 | 204 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 −
(𝑥↑2)) ∈ (ℂ
∖ (-∞(,]0))) |
206 | | 2cnd 11131 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 2 ∈
ℂ) |
207 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
208 | 206, 207 | mulcld 10098 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
209 | 208 | negcld 10417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → -(2
· 𝑥) ∈
ℂ) |
210 | 209 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(2 · 𝑥) ∈ ℂ) |
211 | 12, 210 | sylan2 490 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → -(2
· 𝑥) ∈
ℂ) |
212 | 59 | sqrtcld 14220 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (√‘𝑦) ∈ ℂ) |
213 | 212 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈
ℂ) |
214 | | ovexd 6720 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 ·
(√‘𝑦))) ∈
V) |
215 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ) |
216 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ ℝ) |
217 | | 1cnd 10094 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 1 ∈ ℂ) |
218 | 11, 217 | dvmptc 23766 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 1)) = (𝑥
∈ ℂ ↦ 0)) |
219 | 17 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
220 | | 2cn 11129 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
221 | | mulcl 10058 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
222 | 220, 221 | mpan 706 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
223 | 222 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
224 | | 2nn 11223 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
225 | | dvexp 23761 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
226 | 224, 225 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) |
227 | | 2m1e1 11173 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
228 | 227 | oveq2i 6701 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
229 | | exp1 12906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
230 | 228, 229 | syl5eq 2697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥) |
231 | 230 | oveq2d 6706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (2
· (𝑥↑(2 −
1))) = (2 · 𝑥)) |
232 | 231 | mpteq2ia 4773 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) = (𝑥 ∈ ℂ
↦ (2 · 𝑥)) |
233 | 226, 232 | eqtri 2673 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· 𝑥)) |
234 | 233 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) |
235 | 11, 79, 216, 218, 219, 223, 234 | dvmptsub 23775 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2
· 𝑥)))) |
236 | | df-neg 10307 |
. . . . . . . . . . . . 13
⊢ -(2
· 𝑥) = (0 − (2
· 𝑥)) |
237 | 236 | mpteq2i 4774 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ -(2
· 𝑥)) = (𝑥 ∈ ℂ ↦ (0
− (2 · 𝑥))) |
238 | 235, 237 | syl6eqr 2703 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥))) |
239 | 11, 215, 210, 238, 81, 87, 82, 105 | dvmptres 23771 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥))) |
240 | | eqid 2651 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
241 | 240 | dvcnsqrt 24530 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦)))) |
242 | 241 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦))))) |
243 | | fveq2 6229 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) →
(√‘𝑦) =
(√‘(1 − (𝑥↑2)))) |
244 | 243 | oveq2d 6706 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 − (𝑥↑2)) → (2 ·
(√‘𝑦)) = (2
· (√‘(1 − (𝑥↑2))))) |
245 | 244 | oveq2d 6706 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2
· (√‘𝑦))) = (1 / (2 · (√‘(1
− (𝑥↑2)))))) |
246 | 11, 11, 205, 211, 213, 214, 239, 242, 243, 245 | dvmptco 23780 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))) |
247 | | mulneg2 10505 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥)) |
248 | 220, 12, 247 | sylancr 696 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥)) |
249 | 248 | oveq1d 6705 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-(2
· 𝑥) / (2 ·
(√‘(1 − (𝑥↑2)))))) |
250 | 12 | negcld 10417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ) |
251 | | eldifn 3766 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
252 | 251, 3 | eleq2s 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
253 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = -1 → 𝑥 = -1) |
254 | | mnflt 11995 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-1
∈ ℝ → -∞ < -1) |
255 | 89, 254 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
< -1 |
256 | | ubioc1 12265 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
257 | 51, 134, 255, 256 | mp3an 1464 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
(-∞(,]-1) |
258 | 253, 257 | syl6eqel 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
259 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → 𝑥 = 1) |
260 | | ltpnf 11992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
261 | 92, 260 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
262 | | lbico1 12266 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
263 | 135, 123,
261, 262 | mp3an 1464 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
(1[,)+∞) |
264 | 259, 263 | syl6eqel 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
265 | 258, 264 | orim12i 537 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
266 | 265 | orcoms 403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
267 | | elun 3786 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
268 | 266, 267 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
269 | 252, 268 | nsyl 135 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
270 | | 1cnd 10094 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
271 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
272 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
273 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
274 | 272, 273 | sqr00d 14224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
275 | 270, 271,
274 | subeq0d 10438 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
276 | 148, 275 | syl5req 2698 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
277 | 276 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
278 | | sqeqor 13018 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
279 | 16, 278 | mpan2 707 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
280 | 277, 279 | sylibd 229 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) |
281 | 280 | necon3bd 2837 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) |
282 | 12, 269, 281 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) |
283 | | 2cnne0 11280 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
284 | | divcan5 10765 |
. . . . . . . . . . . . 13
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
285 | 283, 284 | mp3an3 1453 |
. . . . . . . . . . . 12
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 ·
-𝑥) / (2 ·
(√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2))))) |
286 | 250, 114,
282, 285 | syl12anc 1364 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
287 | 220, 12, 221 | sylancr 696 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ) |
288 | 287 | negcld 10417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ) |
289 | | mulcl 10058 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
290 | 220, 114,
289 | sylancr 696 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2))))
∈ ℂ) |
291 | | mulne0 10707 |
. . . . . . . . . . . . . 14
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) |
292 | 283, 291 | mpan 706 |
. . . . . . . . . . . . 13
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) |
293 | 114, 282,
292 | syl2anc 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2)))) ≠
0) |
294 | 288, 290,
293 | divrec2d 10843 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = ((1 / (2
· (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) |
295 | 249, 286,
294 | 3eqtr3rd 2694 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)) =
(-𝑥 / (√‘(1
− (𝑥↑2))))) |
296 | 295 | mpteq2ia 4773 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))
= (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))) |
297 | 246, 296 | syl6eq 2701 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))) |
298 | 11, 74, 75, 111, 115, 116, 297 | dvmptadd 23768 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))) |
299 | | mulcl 10058 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
300 | 13, 20, 299 | sylancr 696 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → (i
· (√‘(1 − (𝑥↑2)))) ∈ ℂ) |
301 | 12, 300 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1
− (𝑥↑2))))
∈ ℂ) |
302 | 301, 250,
114, 282 | divdird 10877 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) =
(((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 −
(𝑥↑2)))) + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
303 | | ixi 10694 |
. . . . . . . . . . . . . . . 16
⊢ (i
· i) = -1 |
304 | 303 | eqcomi 2660 |
. . . . . . . . . . . . . . 15
⊢ -1 = (i
· i) |
305 | 304 | oveq1i 6700 |
. . . . . . . . . . . . . 14
⊢ (-1
· 𝑥) = ((i ·
i) · 𝑥) |
306 | | mulm1 10509 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (-1
· 𝑥) = -𝑥) |
307 | | mulass 10062 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i)
· 𝑥) = (i ·
(i · 𝑥))) |
308 | 13, 13, 307 | mp3an12 1454 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((i
· i) · 𝑥) =
(i · (i · 𝑥))) |
309 | 305, 306,
308 | 3eqtr3a 2709 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥))) |
310 | 309 | oveq1d 6705 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1
− (𝑥↑2))))) =
((i · (i · 𝑥)) + (i · (√‘(1 −
(𝑥↑2)))))) |
311 | | negcl 10319 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) |
312 | 300, 311 | addcomd 10276 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 −
(𝑥↑2)))))) |
313 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → i ∈
ℂ) |
314 | 313, 15, 20 | adddid 10102 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i ·
(√‘(1 − (𝑥↑2)))))) |
315 | 310, 312,
314 | 3eqtr4d 2695 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))))) |
316 | 12, 315 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) = (i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
317 | 316 | oveq1d 6705 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) = ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
318 | 72, 114, 282 | divcan4d 10845 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) = i) |
319 | 318 | oveq1d 6705 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
320 | 302, 317,
319 | 3eqtr3rd 2694 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
321 | 320 | mpteq2ia 4773 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2))))) |
322 | 298, 321 | syl6eq 2701 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2)))))) |
323 | 240 | dvlog 24442 |
. . . . . . 7
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
324 | | logf1o 24356 |
. . . . . . . . . 10
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
325 | | f1of 6175 |
. . . . . . . . . 10
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
326 | 324, 325 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
327 | | snssi 4371 |
. . . . . . . . . . 11
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) |
328 | 64, 327 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ (-∞(,]0) |
329 | | sscon 3777 |
. . . . . . . . . 10
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
330 | 328, 329 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
331 | 326, 330 | feqresmpt 6289 |
. . . . . . . 8
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
332 | 331 | oveq2d 6706 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) |
333 | 323, 332 | syl5reqr 2700 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
334 | | fveq2 6229 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) →
(log‘𝑦) =
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))) |
335 | | oveq2 6698 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) → (1 /
𝑦) = (1 / ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) |
336 | 11, 11, 57, 58, 70, 71, 322, 333, 334, 335 | dvmptco 23780 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))))) |
337 | 22, 24 | reccld 10832 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) |
338 | | mulcl 10058 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
→ (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) |
339 | 13, 21, 338 | sylancr 696 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) ∈ ℂ) |
340 | 12, 339 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) |
341 | 337, 340,
114, 282 | divassd 10874 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = ((1 / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) · ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) |
342 | 340, 22, 24 | divrec2d 10843 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
343 | 72, 22, 24 | divcan4d 10845 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = i) |
344 | 342, 343 | eqtr3d 2687 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) = i) |
345 | 344 | oveq1d 6705 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = (i /
(√‘(1 − (𝑥↑2))))) |
346 | 341, 345 | eqtr3d 2687 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) = (i /
(√‘(1 − (𝑥↑2))))) |
347 | 346 | mpteq2ia 4773 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2))))) |
348 | 336, 347 | syl6eq 2701 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2)))))) |
349 | | negicn 10320 |
. . . . 5
⊢ -i ∈
ℂ |
350 | 349 | a1i 11 |
. . . 4
⊢ (⊤
→ -i ∈ ℂ) |
351 | 11, 26, 27, 348, 350 | dvmptcmul 23772 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2))))))) |
352 | 351 | trud 1533 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) |
353 | 13, 13 | mulneg1i 10514 |
. . . . . 6
⊢ (-i
· i) = -(i · i) |
354 | 303 | negeqi 10312 |
. . . . . 6
⊢ -(i
· i) = --1 |
355 | | negneg1e1 11166 |
. . . . . 6
⊢ --1 =
1 |
356 | 353, 354,
355 | 3eqtri 2677 |
. . . . 5
⊢ (-i
· i) = 1 |
357 | 356 | oveq1i 6700 |
. . . 4
⊢ ((-i
· i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 −
(𝑥↑2)))) |
358 | | divass 10741 |
. . . . . 6
⊢ ((-i
∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) |
359 | 349, 13, 358 | mp3an12 1454 |
. . . . 5
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) |
360 | 114, 282,
359 | syl2anc 694 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1
− (𝑥↑2)))) = (-i
· (i / (√‘(1 − (𝑥↑2)))))) |
361 | 357, 360 | syl5reqr 2700 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1
− (𝑥↑2))))) = (1
/ (√‘(1 − (𝑥↑2))))) |
362 | 361 | mpteq2ia 4773 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
363 | 9, 352, 362 | 3eqtri 2677 |
1
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |