Step | Hyp | Ref
| Expression |
1 | | df-asin 24392 |
. . . . 5
⊢ arcsin =
(𝑥 ∈ ℂ ↦
(-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
2 | 1 | reseq1i 5313 |
. . . 4
⊢ (arcsin
↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i
· (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) |
3 | | dvasin.d |
. . . . . 6
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
4 | | difss 3699 |
. . . . . 6
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆
ℂ |
5 | 3, 4 | eqsstri 3598 |
. . . . 5
⊢ 𝐷 ⊆
ℂ |
6 | | resmpt 5369 |
. . . . 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 2632 |
. . 3
⊢ (arcsin
↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
9 | 8 | oveq2i 6560 |
. 2
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(ℂ D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) |
10 | | cnelprrecn 9908 |
. . . . 5
⊢ ℂ
∈ {ℝ, ℂ} |
11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂ ∈ {ℝ, ℂ}) |
12 | 5 | sseli 3564 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ) |
13 | | ax-icn 9874 |
. . . . . . . . 9
⊢ i ∈
ℂ |
14 | | mulcl 9899 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑥
∈ ℂ) → (i · 𝑥) ∈ ℂ) |
15 | 13, 14 | mpan 702 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (i
· 𝑥) ∈
ℂ) |
16 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
17 | | sqcl 12787 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈
ℂ) |
18 | | subcl 10159 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 −
(𝑥↑2)) ∈
ℂ) |
19 | 16, 17, 18 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (1
− (𝑥↑2)) ∈
ℂ) |
20 | 19 | sqrtcld 14024 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
21 | 15, 20 | addcld 9938 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
22 | 12, 21 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
ℂ) |
23 | | asinlem 24395 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) |
24 | 12, 23 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠
0) |
25 | 22, 24 | logcld 24121 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) |
26 | 25 | adantl 481 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2))))) ∈ ℂ) |
27 | | ovex 6577 |
. . . . 5
⊢ (i /
(√‘(1 − (𝑥↑2)))) ∈ V |
28 | 27 | a1i 11 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i /
(√‘(1 − (𝑥↑2)))) ∈ V) |
29 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) |
30 | | asinlem3 24398 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) |
31 | | rere 13710 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ →
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))) |
32 | 31 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
33 | 32 | biimpac 502 |
. . . . . . . . . . . . . . . . 17
⊢ ((0 ≤
(ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) |
34 | 30, 33 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) |
35 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≠ 0) |
36 | 29, 34, 35 | ne0gt0d 10053 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) |
37 | | 0re 9919 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
38 | | ltnle 9996 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
→ (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
39 | 37, 38 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 <
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
41 | 36, 40 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) |
42 | 41 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
43 | 12, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ
→ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
44 | | imor 427 |
. . . . . . . . . . . 12
⊢ ((((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
45 | 43, 44 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤
0)) |
46 | 45 | orcomd 402 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
47 | 46 | olcd 407 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ∨
(¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) |
48 | | 3ianor 1048 |
. . . . . . . . . . 11
⊢ (¬
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0)
↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨
¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0)) |
49 | | 3orrot 1037 |
. . . . . . . . . . 11
⊢ ((¬
((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤ 0 ∨
¬ ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ)) |
50 | | 3orass 1034 |
. . . . . . . . . . 11
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ))) |
51 | 48, 49, 50 | 3bitrri 286 |
. . . . . . . . . 10
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))) ≤
0)) |
52 | | mnfxr 9975 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
53 | | elioc2 12107 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) →
(((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0))) |
54 | 52, 37, 53 | mp2an 704 |
. . . . . . . . . 10
⊢ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞
< ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ≤
0)) |
55 | 51, 54 | xchbinxr 324 |
. . . . . . . . 9
⊢ ((¬
-∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i ·
𝑥) + (√‘(1
− (𝑥↑2))))
∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈
(-∞(,]0)) |
56 | 47, 55 | sylib 207 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) ∈
(-∞(,]0)) |
57 | 22, 56 | eldifd 3551 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ
∖ (-∞(,]0))) |
58 | 57 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖
(-∞(,]0))) |
59 | | ovex 6577 |
. . . . . . 7
⊢ ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))) ∈
V |
60 | 59 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))) ∈
V) |
61 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
∈ ℂ) |
62 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0)) |
63 | | 0xr 9965 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
64 | | mnflt0 11835 |
. . . . . . . . . . . 12
⊢ -∞
< 0 |
65 | | ubioc1 12098 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ -∞ < 0) → 0 ∈ (-∞(,]0)) |
66 | 52, 63, 64, 65 | mp3an 1416 |
. . . . . . . . . . 11
⊢ 0 ∈
(-∞(,]0) |
67 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈
(-∞(,]0))) |
68 | 66, 67 | mpbiri 247 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0)) |
69 | 68 | necon3bi 2808 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ (-∞(,]0)
→ 𝑦 ≠
0) |
70 | 62, 69 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → 𝑦
≠ 0) |
71 | 61, 70 | logcld 24121 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (log‘𝑦) ∈ ℂ) |
72 | 71 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ) |
73 | | ovex 6577 |
. . . . . . 7
⊢ (1 /
𝑦) ∈
V |
74 | 73 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V) |
75 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ) |
76 | 75, 12 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ) |
77 | 76 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (i
· 𝑥) ∈
ℂ) |
78 | 13 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → i ∈
ℂ) |
79 | 12 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 𝑥 ∈
ℂ) |
80 | | 1cnd 9935 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → 1 ∈
ℂ) |
81 | | simpr 476 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 𝑥
∈ ℂ) |
82 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 1 ∈ ℂ) |
83 | 11 | dvmptid 23526 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 𝑥)) =
(𝑥 ∈ ℂ ↦
1)) |
84 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ⊆
ℂ) |
85 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
86 | 85 | cnfldtopon 22396 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
87 | 86 | toponunii 20547 |
. . . . . . . . . . . . . 14
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
88 | 87 | restid 15917 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
89 | 86, 88 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
90 | 89 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
91 | 85 | recld2 22425 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) |
92 | | neg1rr 11002 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℝ |
93 | | iocmnfcld 22382 |
. . . . . . . . . . . . . . . . . 18
⊢ (-1
∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,)))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞(,]-1) ∈ (Clsd‘(topGen‘ran
(,))) |
95 | | 1re 9918 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
96 | | icopnfcld 22381 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,)))) |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(1[,)+∞) ∈ (Clsd‘(topGen‘ran
(,))) |
98 | | uncld 20655 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧
(1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) →
((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran
(,)))) |
99 | 94, 97, 98 | mp2an 704 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(topGen‘ran (,))) |
100 | 85 | tgioo2 22414 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
101 | 100 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(Clsd‘(topGen‘ran (,))) =
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
102 | 99, 101 | eleqtri 2686 |
. . . . . . . . . . . . . . 15
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ)) |
103 | | restcldr 20788 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ (Clsd‘(TopOpen‘ℂfld)) ∧
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘((TopOpen‘ℂfld) ↾t
ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld))) |
104 | 91, 102, 103 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢
((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) |
105 | 87 | cldopn 20645 |
. . . . . . . . . . . . . 14
⊢
(((-∞(,]-1) ∪ (1[,)+∞)) ∈
(Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld)) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈
(TopOpen‘ℂfld) |
107 | 3, 106 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐷 ∈
(TopOpen‘ℂfld) |
108 | 107 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐷 ∈
(TopOpen‘ℂfld)) |
109 | 11, 81, 82, 83, 84, 90, 85, 108 | dvmptres 23532 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1)) |
110 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ i ∈ ℂ) |
111 | 11, 79, 80, 109, 110 | dvmptcmul 23533 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1))) |
112 | 13 | mulid1i 9921 |
. . . . . . . . . 10
⊢ (i
· 1) = i |
113 | 112 | mpteq2i 4669 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i) |
114 | 111, 113 | syl6eq 2660 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i)) |
115 | 12 | sqcld 12868 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ) |
116 | 16, 115, 18 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ) |
117 | 116 | sqrtcld 14024 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈
ℂ) |
118 | 117 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) →
(√‘(1 − (𝑥↑2))) ∈ ℂ) |
119 | | ovex 6577 |
. . . . . . . . 9
⊢ (-𝑥 / (√‘(1 −
(𝑥↑2)))) ∈
V |
120 | 119 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (-𝑥 / (√‘(1 −
(𝑥↑2)))) ∈
V) |
121 | | elin 3758 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ)) |
122 | 3 | asindmre 32665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |
123 | 122 | eqimssi 3622 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∩ ℝ) ⊆
(-1(,)1) |
124 | 123 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1)) |
125 | 121, 124 | sylbir 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1)) |
126 | | incom 3767 |
. . . . . . . . . . . . . . . 16
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩
(0(,)+∞)) |
127 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
∈ ℝ* |
128 | | df-ioc 12051 |
. . . . . . . . . . . . . . . . . 18
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
129 | | df-ioo 12050 |
. . . . . . . . . . . . . . . . . 18
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
130 | | xrltnle 9984 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) |
131 | 128, 129,
130 | ixxdisj 12061 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞(,]0) ∩
(0(,)+∞)) = ∅) |
132 | 52, 63, 127, 131 | mp3an 1416 |
. . . . . . . . . . . . . . . 16
⊢
((-∞(,]0) ∩ (0(,)+∞)) = ∅ |
133 | 126, 132 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢
((0(,)+∞) ∩ (-∞(,]0)) = ∅ |
134 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈
ℝ) |
135 | 134 | resqcld 12897 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈
ℝ) |
136 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 −
(𝑥↑2)) ∈
ℝ) |
137 | 95, 135, 136 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ) |
138 | 92 | rexri 9976 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℝ* |
139 | 95 | rexri 9976 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
140 | | elioo2 12087 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1))) |
141 | 138, 139,
140 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1)) |
142 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
143 | 142 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
144 | 142 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 0 ≤
(abs‘𝑥)) |
145 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ≤
1 |
146 | | lt2sq 12799 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1))
→ ((abs‘𝑥) <
1 ↔ ((abs‘𝑥)↑2) < (1↑2))) |
147 | 95, 145, 146 | mpanr12 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((abs‘𝑥)
∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) <
(1↑2))) |
148 | 143, 144,
147 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ ((abs‘𝑥)↑2) < (1↑2))) |
149 | | abslt 13902 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1))) |
150 | 95, 149 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥) < 1
↔ (-1 < 𝑥 ∧
𝑥 <
1))) |
151 | | absresq 13890 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
((abs‘𝑥)↑2) =
(𝑥↑2)) |
152 | | sq1 12820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1↑2) = 1 |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ →
(1↑2) = 1) |
154 | 151, 153 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ (𝑥↑2) < 1)) |
155 | | resqcl 12793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈
ℝ) |
156 | | posdif 10400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥↑2) ∈ ℝ ∧ 1
∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 −
(𝑥↑2)))) |
157 | 155, 95, 156 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1
− (𝑥↑2)))) |
158 | 154, 157 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ →
(((abs‘𝑥)↑2)
< (1↑2) ↔ 0 < (1 − (𝑥↑2)))) |
159 | 148, 150,
158 | 3bitr3d 297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2)))) |
160 | 159 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → ((-1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))) |
161 | 160 | 3impib 1254 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ -1 <
𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))) |
162 | 141, 161 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (-1(,)1) → 0 <
(1 − (𝑥↑2))) |
163 | 137, 162 | elrpd 11745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
ℝ+) |
164 | | ioorp 12122 |
. . . . . . . . . . . . . . . 16
⊢
(0(,)+∞) = ℝ+ |
165 | 163, 164 | syl6eleqr 2699 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (-1(,)1) → (1
− (𝑥↑2)) ∈
(0(,)+∞)) |
166 | | disjel 3975 |
. . . . . . . . . . . . . . 15
⊢
((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 −
(𝑥↑2)) ∈
(0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
167 | 133, 165,
166 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (-1(,)1) → ¬ (1
− (𝑥↑2)) ∈
(-∞(,]0)) |
168 | 125, 167 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) |
169 | | elioc2 12107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0))) |
170 | 52, 37, 169 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
171 | 170 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ <
(1 − (𝑥↑2))
∧ (1 − (𝑥↑2)) ≤ 0)) |
172 | 171 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ) |
173 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 −
(1 − (𝑥↑2)))
∈ ℝ) |
174 | 95, 172, 173 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ) |
175 | | nncan 10189 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1
− (𝑥↑2))) =
(𝑥↑2)) |
176 | 16, 175 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥↑2) ∈ ℂ →
(1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
177 | 176 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥↑2) ∈ ℂ →
((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈
ℝ)) |
178 | 177 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈
ℝ) |
179 | 174, 178 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (𝑥↑2) ∈ ℝ) |
180 | 172 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ) |
181 | 171 | simp3d 1068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
(-∞(,]0) → (1 − (𝑥↑2)) ≤ 0) |
182 | 181 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0) |
183 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((1
− (𝑥↑2)) ∈
ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 −
(𝑥↑2)) ≤ 0 ∧ 0
≤ 1) → (1 − (𝑥↑2)) ≤ 1)) |
184 | 37, 95, 183 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
− (𝑥↑2)) ∈
ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1
− (𝑥↑2)) ≤
1)) |
185 | 145, 184 | mpan2i 709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
− (𝑥↑2)) ∈
ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤
1)) |
186 | 180, 182,
185 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1) |
187 | | subge0 10420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1
− (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) |
188 | 95, 180, 187 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤
1)) |
189 | 186, 188 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2)))) |
190 | 176 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2)) |
191 | 189, 190 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → 0 ≤ (𝑥↑2)) |
192 | 179, 191 | resqrtcld 14004 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥↑2) ∈ ℂ ∧ (1
− (𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
193 | 17, 192 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ) |
194 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
(√‘(𝑥↑2))
∈ ℝ)) |
195 | 193, 194 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
196 | 193 | renegcld 10336 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ) |
197 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔
-(√‘(𝑥↑2))
∈ ℝ)) |
198 | 196, 197 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
-(√‘(𝑥↑2))
→ 𝑥 ∈
ℝ)) |
199 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑2) = (𝑥↑2) |
200 | | eqsqrtor 13954 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) →
((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
201 | 17, 200 | mpdan 699 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))) |
202 | 199, 201 | mpbii 222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))) |
203 | 202 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → (𝑥 =
(√‘(𝑥↑2))
∨ 𝑥 =
-(√‘(𝑥↑2)))) |
204 | 195, 198,
203 | mpjaod 395 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) → 𝑥
∈ ℝ) |
205 | 204 | stoic1a 1688 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ ¬
𝑥 ∈ ℝ) →
¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
206 | 12, 205 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 −
(𝑥↑2)) ∈
(-∞(,]0)) |
207 | 168, 206 | pm2.61dan 828 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈
(-∞(,]0)) |
208 | 116, 207 | eldifd 3551 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖
(-∞(,]0))) |
209 | 208 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → (1 −
(𝑥↑2)) ∈ (ℂ
∖ (-∞(,]0))) |
210 | | 2cnd 10970 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 2 ∈
ℂ) |
211 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
212 | 210, 211 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
213 | 212 | negcld 10258 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → -(2
· 𝑥) ∈
ℂ) |
214 | 213 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → -(2 · 𝑥) ∈ ℂ) |
215 | 12, 214 | sylan2 490 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ 𝐷) → -(2
· 𝑥) ∈
ℂ) |
216 | 61 | sqrtcld 14024 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℂ ∖
(-∞(,]0)) → (√‘𝑦) ∈ ℂ) |
217 | 216 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈
ℂ) |
218 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (1 / (2
· (√‘𝑦))) ∈ V |
219 | 218 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑦
∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 ·
(√‘𝑦))) ∈
V) |
220 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ) |
221 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → 0 ∈ ℝ) |
222 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 1 ∈ ℂ) |
223 | 11, 222 | dvmptc 23527 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ 1)) = (𝑥
∈ ℂ ↦ 0)) |
224 | 17 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (𝑥↑2) ∈ ℂ) |
225 | | 2cn 10968 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
226 | | mulcl 9899 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
227 | 225, 226 | mpan 702 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
228 | 227 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
229 | | 2nn 11062 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
230 | | dvexp 23522 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 −
1))))) |
231 | 229, 230 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) |
232 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
− 1) = 1 |
233 | 232 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥↑(2 − 1)) = (𝑥↑1) |
234 | | exp1 12728 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥) |
235 | 233, 234 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥) |
236 | 235 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (2
· (𝑥↑(2 −
1))) = (2 · 𝑥)) |
237 | 236 | mpteq2ia 4668 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ ↦ (2
· (𝑥↑(2 −
1)))) = (𝑥 ∈ ℂ
↦ (2 · 𝑥)) |
238 | 231, 237 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2
· 𝑥)) |
239 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))) |
240 | 11, 82, 221, 223, 224, 228, 239 | dvmptsub 23536 |
. . . . . . . . . . . 12
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2
· 𝑥)))) |
241 | | df-neg 10148 |
. . . . . . . . . . . . 13
⊢ -(2
· 𝑥) = (0 − (2
· 𝑥)) |
242 | 241 | mpteq2i 4669 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ ↦ -(2
· 𝑥)) = (𝑥 ∈ ℂ ↦ (0
− (2 · 𝑥))) |
243 | 240, 242 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℂ D (𝑥 ∈
ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥))) |
244 | 11, 220, 214, 243, 84, 90, 85, 108 | dvmptres 23532 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥))) |
245 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
246 | 245 | dvcnsqrt 24285 |
. . . . . . . . . . 11
⊢ (ℂ
D (𝑦 ∈ (ℂ
∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦)))) |
247 | 246 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / (2 · (√‘𝑦))))) |
248 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) →
(√‘𝑦) =
(√‘(1 − (𝑥↑2)))) |
249 | 248 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑦 = (1 − (𝑥↑2)) → (2 ·
(√‘𝑦)) = (2
· (√‘(1 − (𝑥↑2))))) |
250 | 249 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2
· (√‘𝑦))) = (1 / (2 · (√‘(1
− (𝑥↑2)))))) |
251 | 11, 11, 209, 215, 217, 219, 244, 247, 248, 250 | dvmptco 23541 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))) |
252 | | mulneg2 10346 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥)) |
253 | 225, 12, 252 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥)) |
254 | 253 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-(2
· 𝑥) / (2 ·
(√‘(1 − (𝑥↑2)))))) |
255 | 12 | negcld 10258 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ) |
256 | | eldifn 3695 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
257 | 256, 3 | eleq2s 2706 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
258 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = -1 → 𝑥 = -1) |
259 | | mnflt 11833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-1
∈ ℝ → -∞ < -1) |
260 | 92, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ -∞
< -1 |
261 | | ubioc1 12098 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ -∞ < -1) → -1 ∈
(-∞(,]-1)) |
262 | 52, 138, 260, 261 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
(-∞(,]-1) |
263 | 258, 262 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1)) |
264 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 1 → 𝑥 = 1) |
265 | | ltpnf 11830 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
266 | 95, 265 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
267 | | lbico1 12099 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1
< +∞) → 1 ∈ (1[,)+∞)) |
268 | 139, 127,
266, 267 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
(1[,)+∞) |
269 | 264, 268 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞)) |
270 | 263, 269 | orim12i 537 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
271 | 270 | orcoms 403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈
(1[,)+∞))) |
272 | | elun 3715 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞)) ↔ (𝑥
∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞))) |
273 | 271, 272 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪
(1[,)+∞))) |
274 | 257, 273 | nsyl 134 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1)) |
275 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 ∈
ℂ) |
276 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ) |
277 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈
ℂ) |
278 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (√‘(1
− (𝑥↑2))) =
0) |
279 | 277, 278 | sqr00d 14028 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0) |
280 | 275, 276,
279 | subeq0d 10279 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2)) |
281 | 152, 280 | syl5req 2657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2)) |
282 | 281 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2))) |
283 | | sqeqor 12840 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑥↑2)
= (1↑2) ↔ (𝑥 = 1
∨ 𝑥 =
-1))) |
284 | 16, 283 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔
(𝑥 = 1 ∨ 𝑥 = -1))) |
285 | 282, 284 | sylibd 228 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ →
((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1))) |
286 | 285 | necon3bd 2796 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (¬
(𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1
− (𝑥↑2))) ≠
0)) |
287 | 12, 274, 286 | sylc 63 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠
0) |
288 | | 2cnne0 11119 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
289 | | divcan5 10606 |
. . . . . . . . . . . . 13
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
290 | 288, 289 | mp3an3 1405 |
. . . . . . . . . . . 12
⊢ ((-𝑥 ∈ ℂ ∧
((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 ·
-𝑥) / (2 ·
(√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2))))) |
291 | 255, 117,
287, 290 | syl12anc 1316 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = (-𝑥 / (√‘(1 −
(𝑥↑2))))) |
292 | 225, 12, 226 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ) |
293 | 292 | negcld 10258 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ) |
294 | | mulcl 9899 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
295 | 225, 117,
294 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2))))
∈ ℂ) |
296 | | mulne0 10548 |
. . . . . . . . . . . . . 14
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) |
297 | 288, 296 | mpan 702 |
. . . . . . . . . . . . 13
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → (2 ·
(√‘(1 − (𝑥↑2)))) ≠ 0) |
298 | 117, 287,
297 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1
− (𝑥↑2)))) ≠
0) |
299 | 293, 295,
298 | divrec2d 10684 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 −
(𝑥↑2))))) = ((1 / (2
· (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) |
300 | 254, 291,
299 | 3eqtr3rd 2653 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)) =
(-𝑥 / (√‘(1
− (𝑥↑2))))) |
301 | 300 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1
− (𝑥↑2)))))
· -(2 · 𝑥)))
= (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))) |
302 | 251, 301 | syl6eq 2660 |
. . . . . . . 8
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (√‘(1
− (𝑥↑2))))) =
(𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))) |
303 | 11, 77, 78, 114, 118, 120, 302 | dvmptadd 23529 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))) |
304 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i ·
(√‘(1 − (𝑥↑2)))) ∈ ℂ) |
305 | 13, 20, 304 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → (i
· (√‘(1 − (𝑥↑2)))) ∈ ℂ) |
306 | 12, 305 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1
− (𝑥↑2))))
∈ ℂ) |
307 | 306, 255,
117, 287 | divdird 10718 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) =
(((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 −
(𝑥↑2)))) + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
308 | | ixi 10535 |
. . . . . . . . . . . . . . . 16
⊢ (i
· i) = -1 |
309 | 308 | eqcomi 2619 |
. . . . . . . . . . . . . . 15
⊢ -1 = (i
· i) |
310 | 309 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ (-1
· 𝑥) = ((i ·
i) · 𝑥) |
311 | | mulm1 10350 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (-1
· 𝑥) = -𝑥) |
312 | | mulass 9903 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i)
· 𝑥) = (i ·
(i · 𝑥))) |
313 | 13, 13, 312 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((i
· i) · 𝑥) =
(i · (i · 𝑥))) |
314 | 310, 311,
313 | 3eqtr3a 2668 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥))) |
315 | 314 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1
− (𝑥↑2))))) =
((i · (i · 𝑥)) + (i · (√‘(1 −
(𝑥↑2)))))) |
316 | | negcl 10160 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → -𝑥 ∈
ℂ) |
317 | 305, 316 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 −
(𝑥↑2)))))) |
318 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → i ∈
ℂ) |
319 | 318, 15, 20 | adddid 9943 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i ·
(√‘(1 − (𝑥↑2)))))) |
320 | 315, 317,
319 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → ((i
· (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))))) |
321 | 12, 320 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) = (i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2)))))) |
322 | 321 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) +
-𝑥) / (√‘(1
− (𝑥↑2)))) = ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
323 | 75, 117, 287 | divcan4d 10686 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) = i) |
324 | 323 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1
− (𝑥↑2)))) /
(√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 −
(𝑥↑2)))))) |
325 | 307, 322,
324 | 3eqtr3rd 2653 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) |
326 | 325 | mpteq2ia 4668 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2))))) |
327 | 303, 326 | syl6eq 2660 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) /
(√‘(1 − (𝑥↑2)))))) |
328 | 245 | dvlog 24197 |
. . . . . . 7
⊢ (ℂ
D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦)) |
329 | | logf1o 24115 |
. . . . . . . . . 10
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
330 | | f1of 6050 |
. . . . . . . . . 10
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
331 | 329, 330 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ log:(ℂ ∖ {0})⟶ran log) |
332 | | snssi 4280 |
. . . . . . . . . . 11
⊢ (0 ∈
(-∞(,]0) → {0} ⊆ (-∞(,]0)) |
333 | 66, 332 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ (-∞(,]0) |
334 | | sscon 3706 |
. . . . . . . . . 10
⊢ ({0}
⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ
∖ {0})) |
335 | 333, 334 | mp1i 13 |
. . . . . . . . 9
⊢ (⊤
→ (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖
{0})) |
336 | 331, 335 | feqresmpt 6160 |
. . . . . . . 8
⊢ (⊤
→ (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (log‘𝑦))) |
337 | 336 | oveq2d 6565 |
. . . . . . 7
⊢ (⊤
→ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D
(𝑦 ∈ (ℂ ∖
(-∞(,]0)) ↦ (log‘𝑦)))) |
338 | 328, 337 | syl5reqr 2659 |
. . . . . 6
⊢ (⊤
→ (ℂ D (𝑦 ∈
(ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0))
↦ (1 / 𝑦))) |
339 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) →
(log‘𝑦) =
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))) |
340 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = ((i · 𝑥) + (√‘(1 −
(𝑥↑2)))) → (1 /
𝑦) = (1 / ((i ·
𝑥) + (√‘(1
− (𝑥↑2)))))) |
341 | 11, 11, 58, 60, 72, 74, 327, 338, 339, 340 | dvmptco 23541 |
. . . . 5
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))))) |
342 | 22, 24 | reccld 10673 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) |
343 | | mulcl 9899 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
→ (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈
ℂ) |
344 | 13, 21, 343 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) ∈ ℂ) |
345 | 12, 344 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) ∈
ℂ) |
346 | 342, 345,
117, 287 | divassd 10715 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = ((1 / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) · ((i · ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) |
347 | 345, 22, 24 | divrec2d 10684 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))))) |
348 | 75, 22, 24 | divcan4d 10686 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) / ((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))) = i) |
349 | 347, 348 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) = i) |
350 | 349 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · (i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2)))))) / (√‘(1 −
(𝑥↑2)))) = (i /
(√‘(1 − (𝑥↑2))))) |
351 | 346, 350 | eqtr3d 2646 |
. . . . . 6
⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2))))) = (i /
(√‘(1 − (𝑥↑2))))) |
352 | 351 | mpteq2ia 4668 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 −
(𝑥↑2))))) · ((i
· ((i · 𝑥) +
(√‘(1 − (𝑥↑2))))) / (√‘(1 −
(𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2))))) |
353 | 341, 352 | syl6eq 2660 |
. . . 4
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (log‘((i
· 𝑥) +
(√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 −
(𝑥↑2)))))) |
354 | | negicn 10161 |
. . . . 5
⊢ -i ∈
ℂ |
355 | 354 | a1i 11 |
. . . 4
⊢ (⊤
→ -i ∈ ℂ) |
356 | 11, 26, 28, 353, 355 | dvmptcmul 23533 |
. . 3
⊢ (⊤
→ (ℂ D (𝑥 ∈
𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2))))))) |
357 | 356 | trud 1484 |
. 2
⊢ (ℂ
D (𝑥 ∈ 𝐷 ↦ (-i ·
(log‘((i · 𝑥)
+ (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) |
358 | 13, 13 | mulneg1i 10355 |
. . . . . 6
⊢ (-i
· i) = -(i · i) |
359 | 308 | negeqi 10153 |
. . . . . 6
⊢ -(i
· i) = --1 |
360 | | negneg1e1 11005 |
. . . . . 6
⊢ --1 =
1 |
361 | 358, 359,
360 | 3eqtri 2636 |
. . . . 5
⊢ (-i
· i) = 1 |
362 | 361 | oveq1i 6559 |
. . . 4
⊢ ((-i
· i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 −
(𝑥↑2)))) |
363 | | divass 10582 |
. . . . . 6
⊢ ((-i
∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) |
364 | 354, 13, 363 | mp3an12 1406 |
. . . . 5
⊢
(((√‘(1 − (𝑥↑2))) ∈ ℂ ∧
(√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) /
(√‘(1 − (𝑥↑2)))) = (-i · (i /
(√‘(1 − (𝑥↑2)))))) |
365 | 117, 287,
364 | syl2anc 691 |
. . . 4
⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1
− (𝑥↑2)))) = (-i
· (i / (√‘(1 − (𝑥↑2)))))) |
366 | 362, 365 | syl5reqr 2659 |
. . 3
⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1
− (𝑥↑2))))) = (1
/ (√‘(1 − (𝑥↑2))))) |
367 | 366 | mpteq2ia 4668 |
. 2
⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1
− (𝑥↑2)))))) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |
368 | 9, 357, 367 | 3eqtri 2636 |
1
⊢ (ℂ
D (arcsin ↾ 𝐷)) =
(𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 −
(𝑥↑2))))) |