| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvasin.d |
⊢ 𝐷 = ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) |
| 2 |
|
df-asin |
⊢ arcsin = ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 3 |
2
|
reseq1i |
⊢ ( arcsin ↾ 𝐷 ) = ( ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ↾ 𝐷 ) |
| 4 |
|
difss |
⊢ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ⊆ ℂ |
| 5 |
1 4
|
eqsstri |
⊢ 𝐷 ⊆ ℂ |
| 6 |
|
resmpt |
⊢ ( 𝐷 ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ) |
| 7 |
5 6
|
ax-mp |
⊢ ( ( 𝑥 ∈ ℂ ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 8 |
3 7
|
eqtri |
⊢ ( arcsin ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 9 |
8
|
oveq2i |
⊢ ( ℂ D ( arcsin ↾ 𝐷 ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ) |
| 10 |
|
cnelprrecn |
⊢ ℂ ∈ { ℝ , ℂ } |
| 11 |
10
|
a1i |
⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } ) |
| 12 |
5
|
sseli |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ ) |
| 13 |
|
ax-icn |
⊢ i ∈ ℂ |
| 14 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ ) |
| 15 |
13 14
|
mpan |
⊢ ( 𝑥 ∈ ℂ → ( i · 𝑥 ) ∈ ℂ ) |
| 16 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 17 |
|
sqcl |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
| 18 |
|
subcl |
⊢ ( ( 1 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ ) |
| 19 |
16 17 18
|
sylancr |
⊢ ( 𝑥 ∈ ℂ → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ ) |
| 20 |
19
|
sqrtcld |
⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ) |
| 21 |
15 20
|
addcld |
⊢ ( 𝑥 ∈ ℂ → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 22 |
12 21
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 23 |
|
asinlem |
⊢ ( 𝑥 ∈ ℂ → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 24 |
12 23
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 25 |
22 24
|
logcld |
⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 26 |
25
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 27 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ V ) |
| 28 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) |
| 29 |
|
asinlem3 |
⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( ℜ ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 30 |
|
rere |
⊢ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ( ℜ ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 31 |
30
|
breq2d |
⊢ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ( 0 ≤ ( ℜ ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ↔ 0 ≤ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 32 |
31
|
biimpac |
⊢ ( ( 0 ≤ ( ℜ ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → 0 ≤ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 33 |
29 32
|
sylan |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → 0 ≤ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 34 |
23
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 35 |
28 33 34
|
ne0gt0d |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → 0 < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 36 |
|
0re |
⊢ 0 ∈ ℝ |
| 37 |
|
ltnle |
⊢ ( ( 0 ∈ ℝ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → ( 0 < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ↔ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 38 |
36 37
|
mpan |
⊢ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ( 0 < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ↔ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 39 |
38
|
adantl |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → ( 0 < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ↔ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 40 |
35 39
|
mpbid |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) → ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) |
| 41 |
40
|
ex |
⊢ ( 𝑥 ∈ ℂ → ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 42 |
12 41
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 43 |
|
imor |
⊢ ( ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ → ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ↔ ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 44 |
42 43
|
sylib |
⊢ ( 𝑥 ∈ 𝐷 → ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 45 |
44
|
orcomd |
⊢ ( 𝑥 ∈ 𝐷 → ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) ) |
| 46 |
45
|
olcd |
⊢ ( 𝑥 ∈ 𝐷 → ( ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) ) ) |
| 47 |
|
3ianor |
⊢ ( ¬ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ↔ ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∨ ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 48 |
|
3orrot |
⊢ ( ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∨ ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ↔ ( ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) ) |
| 49 |
|
3orass |
⊢ ( ( ¬ -∞ < ( ( 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 |
⊢ ( ( ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) ) ↔ ¬ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 51 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
| 52 |
|
elioc2 |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) ) |
| 53 |
51 36 52
|
mp2an |
⊢ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ) ) |
| 54 |
50 53
|
xchbinxr |
⊢ ( ( ¬ -∞ < ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∨ ( ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≤ 0 ∨ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℝ ) ) ↔ ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ) |
| 55 |
46 54
|
sylib |
⊢ ( 𝑥 ∈ 𝐷 → ¬ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ) |
| 56 |
22 55
|
eldifd |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 57 |
56
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 58 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ V ) |
| 59 |
|
eldifi |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ∈ ℂ ) |
| 60 |
|
eldifn |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ¬ 𝑦 ∈ ( -∞ (,] 0 ) ) |
| 61 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 62 |
|
mnflt0 |
⊢ -∞ < 0 |
| 63 |
|
ubioc1 |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0 ) → 0 ∈ ( -∞ (,] 0 ) ) |
| 64 |
51 61 62 63
|
mp3an |
⊢ 0 ∈ ( -∞ (,] 0 ) |
| 65 |
|
eleq1 |
⊢ ( 𝑦 = 0 → ( 𝑦 ∈ ( -∞ (,] 0 ) ↔ 0 ∈ ( -∞ (,] 0 ) ) ) |
| 66 |
64 65
|
mpbiri |
⊢ ( 𝑦 = 0 → 𝑦 ∈ ( -∞ (,] 0 ) ) |
| 67 |
66
|
necon3bi |
⊢ ( ¬ 𝑦 ∈ ( -∞ (,] 0 ) → 𝑦 ≠ 0 ) |
| 68 |
60 67
|
syl |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ≠ 0 ) |
| 69 |
59 68
|
logcld |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
| 70 |
69
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( log ‘ 𝑦 ) ∈ ℂ ) |
| 71 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 1 / 𝑦 ) ∈ V ) |
| 72 |
13
|
a1i |
⊢ ( 𝑥 ∈ 𝐷 → i ∈ ℂ ) |
| 73 |
72 12
|
mulcld |
⊢ ( 𝑥 ∈ 𝐷 → ( i · 𝑥 ) ∈ ℂ ) |
| 74 |
73
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( i · 𝑥 ) ∈ ℂ ) |
| 75 |
13
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → i ∈ ℂ ) |
| 76 |
12
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ ) |
| 77 |
|
1cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 1 ∈ ℂ ) |
| 78 |
|
simpr |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ ) |
| 79 |
|
1cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ ) |
| 80 |
11
|
dvmptid |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) ) |
| 81 |
5
|
a1i |
⊢ ( ⊤ → 𝐷 ⊆ ℂ ) |
| 82 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
| 83 |
82
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
| 84 |
83
|
toponrestid |
⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) |
| 85 |
82
|
recld2 |
⊢ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) |
| 86 |
|
neg1rr |
⊢ - 1 ∈ ℝ |
| 87 |
|
iocmnfcld |
⊢ ( - 1 ∈ ℝ → ( -∞ (,] - 1 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
| 88 |
86 87
|
ax-mp |
⊢ ( -∞ (,] - 1 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) |
| 89 |
|
1re |
⊢ 1 ∈ ℝ |
| 90 |
|
icopnfcld |
⊢ ( 1 ∈ ℝ → ( 1 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
| 91 |
89 90
|
ax-mp |
⊢ ( 1 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) |
| 92 |
|
uncld |
⊢ ( ( ( -∞ (,] - 1 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ∧ ( 1 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) → ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ) |
| 93 |
88 91 92
|
mp2an |
⊢ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) |
| 94 |
|
tgioo4 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
| 95 |
94
|
fveq2i |
⊢ ( Clsd ‘ ( topGen ‘ ran (,) ) ) = ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
| 96 |
93 95
|
eleqtri |
⊢ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) |
| 97 |
|
restcldr |
⊢ ( ( ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) → ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) |
| 98 |
85 96 97
|
mp2an |
⊢ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) |
| 99 |
83
|
toponunii |
⊢ ℂ = ∪ ( TopOpen ‘ ℂfld ) |
| 100 |
99
|
cldopn |
⊢ ( ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) → ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ∈ ( TopOpen ‘ ℂfld ) ) |
| 101 |
98 100
|
ax-mp |
⊢ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ∈ ( TopOpen ‘ ℂfld ) |
| 102 |
1 101
|
eqeltri |
⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld ) |
| 103 |
102
|
a1i |
⊢ ( ⊤ → 𝐷 ∈ ( TopOpen ‘ ℂfld ) ) |
| 104 |
11 78 79 80 81 84 82 103
|
dvmptres |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ 1 ) ) |
| 105 |
13
|
a1i |
⊢ ( ⊤ → i ∈ ℂ ) |
| 106 |
11 76 77 104 105
|
dvmptcmul |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( i · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( i · 1 ) ) ) |
| 107 |
13
|
mulridi |
⊢ ( i · 1 ) = i |
| 108 |
107
|
mpteq2i |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( i · 1 ) ) = ( 𝑥 ∈ 𝐷 ↦ i ) |
| 109 |
106 108
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( i · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ i ) ) |
| 110 |
12
|
sqcld |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
| 111 |
16 110 18
|
sylancr |
⊢ ( 𝑥 ∈ 𝐷 → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ ) |
| 112 |
111
|
sqrtcld |
⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ) |
| 113 |
112
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ) |
| 114 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ V ) |
| 115 |
|
elin |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ ℝ ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) ) |
| 116 |
1
|
asindmre |
⊢ ( 𝐷 ∩ ℝ ) = ( - 1 (,) 1 ) |
| 117 |
116
|
eqimssi |
⊢ ( 𝐷 ∩ ℝ ) ⊆ ( - 1 (,) 1 ) |
| 118 |
117
|
sseli |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ ℝ ) → 𝑥 ∈ ( - 1 (,) 1 ) ) |
| 119 |
115 118
|
sylbir |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ( - 1 (,) 1 ) ) |
| 120 |
|
incom |
⊢ ( ( 0 (,) +∞ ) ∩ ( -∞ (,] 0 ) ) = ( ( -∞ (,] 0 ) ∩ ( 0 (,) +∞ ) ) |
| 121 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
| 122 |
|
df-ioc |
⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ) |
| 123 |
|
df-ioo |
⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } ) |
| 124 |
|
xrltnle |
⊢ ( ( 0 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 0 < 𝑤 ↔ ¬ 𝑤 ≤ 0 ) ) |
| 125 |
122 123 124
|
ixxdisj |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ (,] 0 ) ∩ ( 0 (,) +∞ ) ) = ∅ ) |
| 126 |
51 61 121 125
|
mp3an |
⊢ ( ( -∞ (,] 0 ) ∩ ( 0 (,) +∞ ) ) = ∅ |
| 127 |
120 126
|
eqtri |
⊢ ( ( 0 (,) +∞ ) ∩ ( -∞ (,] 0 ) ) = ∅ |
| 128 |
|
elioore |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → 𝑥 ∈ ℝ ) |
| 129 |
128
|
resqcld |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → ( 𝑥 ↑ 2 ) ∈ ℝ ) |
| 130 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 131 |
89 129 130
|
sylancr |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 132 |
86
|
rexri |
⊢ - 1 ∈ ℝ* |
| 133 |
|
1xr |
⊢ 1 ∈ ℝ* |
| 134 |
|
elioo2 |
⊢ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑥 ∈ ( - 1 (,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ - 1 < 𝑥 ∧ 𝑥 < 1 ) ) ) |
| 135 |
132 133 134
|
mp2an |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) ↔ ( 𝑥 ∈ ℝ ∧ - 1 < 𝑥 ∧ 𝑥 < 1 ) ) |
| 136 |
|
recn |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ ) |
| 137 |
136
|
abscld |
⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ ) |
| 138 |
136
|
absge0d |
⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( abs ‘ 𝑥 ) ) |
| 139 |
|
0le1 |
⊢ 0 ≤ 1 |
| 140 |
|
lt2sq |
⊢ ( ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( abs ‘ 𝑥 ) < 1 ↔ ( ( abs ‘ 𝑥 ) ↑ 2 ) < ( 1 ↑ 2 ) ) ) |
| 141 |
89 139 140
|
mpanr12 |
⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑥 ) ) → ( ( abs ‘ 𝑥 ) < 1 ↔ ( ( abs ‘ 𝑥 ) ↑ 2 ) < ( 1 ↑ 2 ) ) ) |
| 142 |
137 138 141
|
syl2anc |
⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ 𝑥 ) < 1 ↔ ( ( abs ‘ 𝑥 ) ↑ 2 ) < ( 1 ↑ 2 ) ) ) |
| 143 |
|
abslt |
⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑥 ) < 1 ↔ ( - 1 < 𝑥 ∧ 𝑥 < 1 ) ) ) |
| 144 |
89 143
|
mpan2 |
⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ 𝑥 ) < 1 ↔ ( - 1 < 𝑥 ∧ 𝑥 < 1 ) ) ) |
| 145 |
|
absresq |
⊢ ( 𝑥 ∈ ℝ → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) ) |
| 146 |
|
sq1 |
⊢ ( 1 ↑ 2 ) = 1 |
| 147 |
146
|
a1i |
⊢ ( 𝑥 ∈ ℝ → ( 1 ↑ 2 ) = 1 ) |
| 148 |
145 147
|
breq12d |
⊢ ( 𝑥 ∈ ℝ → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) < ( 1 ↑ 2 ) ↔ ( 𝑥 ↑ 2 ) < 1 ) ) |
| 149 |
|
resqcl |
⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ↑ 2 ) ∈ ℝ ) |
| 150 |
|
posdif |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑥 ↑ 2 ) < 1 ↔ 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 151 |
149 89 150
|
sylancl |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ↑ 2 ) < 1 ↔ 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 152 |
148 151
|
bitrd |
⊢ ( 𝑥 ∈ ℝ → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) < ( 1 ↑ 2 ) ↔ 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 153 |
142 144 152
|
3bitr3d |
⊢ ( 𝑥 ∈ ℝ → ( ( - 1 < 𝑥 ∧ 𝑥 < 1 ) ↔ 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 154 |
153
|
biimpd |
⊢ ( 𝑥 ∈ ℝ → ( ( - 1 < 𝑥 ∧ 𝑥 < 1 ) → 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 155 |
154
|
3impib |
⊢ ( ( 𝑥 ∈ ℝ ∧ - 1 < 𝑥 ∧ 𝑥 < 1 ) → 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) |
| 156 |
135 155
|
sylbi |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → 0 < ( 1 − ( 𝑥 ↑ 2 ) ) ) |
| 157 |
131 156
|
elrpd |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ+ ) |
| 158 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
| 159 |
157 158
|
eleqtrrdi |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( 0 (,) +∞ ) ) |
| 160 |
|
disjel |
⊢ ( ( ( ( 0 (,) +∞ ) ∩ ( -∞ (,] 0 ) ) = ∅ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( 0 (,) +∞ ) ) → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 161 |
127 159 160
|
sylancr |
⊢ ( 𝑥 ∈ ( - 1 (,) 1 ) → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 162 |
119 161
|
syl |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ ) → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 163 |
|
elioc2 |
⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( 𝑥 ↑ 2 ) ) ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ) ) ) |
| 164 |
51 36 163
|
mp2an |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( 𝑥 ↑ 2 ) ) ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ) ) |
| 165 |
164
|
biimpi |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) → ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( 𝑥 ↑ 2 ) ) ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ) ) |
| 166 |
165
|
simp1d |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 167 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) → ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℝ ) |
| 168 |
89 166 167
|
sylancr |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) → ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℝ ) |
| 169 |
|
nncan |
⊢ ( ( 1 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ↑ 2 ) ) |
| 170 |
16 169
|
mpan |
⊢ ( ( 𝑥 ↑ 2 ) ∈ ℂ → ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ↑ 2 ) ) |
| 171 |
170
|
eleq1d |
⊢ ( ( 𝑥 ↑ 2 ) ∈ ℂ → ( ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℝ ↔ ( 𝑥 ↑ 2 ) ∈ ℝ ) ) |
| 172 |
171
|
biimpa |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℝ ) → ( 𝑥 ↑ 2 ) ∈ ℝ ) |
| 173 |
168 172
|
sylan2 |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ ) |
| 174 |
166
|
adantl |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 175 |
165
|
simp3d |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ) |
| 176 |
175
|
adantl |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ) |
| 177 |
|
letr |
⊢ ( ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ 1 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) ) |
| 178 |
36 89 177
|
mp3an23 |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ → ( ( ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ 1 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) ) |
| 179 |
139 178
|
mpan2i |
⊢ ( ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ → ( ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 0 → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) ) |
| 180 |
174 176 179
|
sylc |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) |
| 181 |
|
subge0 |
⊢ ( ( 1 ∈ ℝ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ↔ ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) ) |
| 182 |
89 174 181
|
sylancr |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 0 ≤ ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ↔ ( 1 − ( 𝑥 ↑ 2 ) ) ≤ 1 ) ) |
| 183 |
180 182
|
mpbird |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ≤ ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 184 |
170
|
adantr |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( 1 − ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ↑ 2 ) ) |
| 185 |
183 184
|
breqtrd |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ≤ ( 𝑥 ↑ 2 ) ) |
| 186 |
173 185
|
resqrtcld |
⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 187 |
17 186
|
sylan |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 188 |
|
eleq1 |
⊢ ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) → ( 𝑥 ∈ ℝ ↔ ( √ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℝ ) ) |
| 189 |
187 188
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) → 𝑥 ∈ ℝ ) ) |
| 190 |
187
|
renegcld |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → - ( √ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℝ ) |
| 191 |
|
eleq1 |
⊢ ( 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) → ( 𝑥 ∈ ℝ ↔ - ( √ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℝ ) ) |
| 192 |
190 191
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) → 𝑥 ∈ ℝ ) ) |
| 193 |
|
eqid |
⊢ ( 𝑥 ↑ 2 ) = ( 𝑥 ↑ 2 ) |
| 194 |
|
eqsqrtor |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) = ( 𝑥 ↑ 2 ) ↔ ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) ∨ 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) ) ) ) |
| 195 |
17 194
|
mpdan |
⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) = ( 𝑥 ↑ 2 ) ↔ ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) ∨ 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) ) ) ) |
| 196 |
193 195
|
mpbii |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) ∨ 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) ) ) |
| 197 |
196
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝑥 = ( √ ‘ ( 𝑥 ↑ 2 ) ) ∨ 𝑥 = - ( √ ‘ ( 𝑥 ↑ 2 ) ) ) ) |
| 198 |
189 192 197
|
mpjaod |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 𝑥 ∈ ℝ ) |
| 199 |
198
|
stoic1a |
⊢ ( ( 𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ ) → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 200 |
12 199
|
sylan |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ ) → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 201 |
162 200
|
pm2.61dan |
⊢ ( 𝑥 ∈ 𝐷 → ¬ ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) |
| 202 |
111 201
|
eldifd |
⊢ ( 𝑥 ∈ 𝐷 → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 203 |
202
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) |
| 204 |
|
2cnd |
⊢ ( 𝑥 ∈ ℂ → 2 ∈ ℂ ) |
| 205 |
|
id |
⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ ) |
| 206 |
204 205
|
mulcld |
⊢ ( 𝑥 ∈ ℂ → ( 2 · 𝑥 ) ∈ ℂ ) |
| 207 |
206
|
negcld |
⊢ ( 𝑥 ∈ ℂ → - ( 2 · 𝑥 ) ∈ ℂ ) |
| 208 |
207
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( 2 · 𝑥 ) ∈ ℂ ) |
| 209 |
12 208
|
sylan2 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → - ( 2 · 𝑥 ) ∈ ℂ ) |
| 210 |
59
|
sqrtcld |
⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( √ ‘ 𝑦 ) ∈ ℂ ) |
| 211 |
210
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( √ ‘ 𝑦 ) ∈ ℂ ) |
| 212 |
|
ovexd |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 1 / ( 2 · ( √ ‘ 𝑦 ) ) ) ∈ V ) |
| 213 |
19
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ ) |
| 214 |
36
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℝ ) |
| 215 |
|
1cnd |
⊢ ( ⊤ → 1 ∈ ℂ ) |
| 216 |
11 215
|
dvmptc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) ) |
| 217 |
17
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
| 218 |
|
2cn |
⊢ 2 ∈ ℂ |
| 219 |
|
mulcl |
⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ ) |
| 220 |
218 219
|
mpan |
⊢ ( 𝑥 ∈ ℂ → ( 2 · 𝑥 ) ∈ ℂ ) |
| 221 |
220
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ ) |
| 222 |
|
2nn |
⊢ 2 ∈ ℕ |
| 223 |
|
dvexp |
⊢ ( 2 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) ) |
| 224 |
222 223
|
ax-mp |
⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) |
| 225 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
| 226 |
225
|
oveq2i |
⊢ ( 𝑥 ↑ ( 2 − 1 ) ) = ( 𝑥 ↑ 1 ) |
| 227 |
|
exp1 |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 1 ) = 𝑥 ) |
| 228 |
226 227
|
eqtrid |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ ( 2 − 1 ) ) = 𝑥 ) |
| 229 |
228
|
oveq2d |
⊢ ( 𝑥 ∈ ℂ → ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) = ( 2 · 𝑥 ) ) |
| 230 |
229
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) |
| 231 |
224 230
|
eqtri |
⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) |
| 232 |
231
|
a1i |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) ) |
| 233 |
11 79 214 216 217 221 232
|
dvmptsub |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 0 − ( 2 · 𝑥 ) ) ) ) |
| 234 |
|
df-neg |
⊢ - ( 2 · 𝑥 ) = ( 0 − ( 2 · 𝑥 ) ) |
| 235 |
234
|
mpteq2i |
⊢ ( 𝑥 ∈ ℂ ↦ - ( 2 · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( 0 − ( 2 · 𝑥 ) ) ) |
| 236 |
233 235
|
eqtr4di |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( 2 · 𝑥 ) ) ) |
| 237 |
11 213 208 236 81 84 82 103
|
dvmptres |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ - ( 2 · 𝑥 ) ) ) |
| 238 |
|
eqid |
⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) ) |
| 239 |
238
|
dvcnsqrt |
⊢ ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( √ ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / ( 2 · ( √ ‘ 𝑦 ) ) ) ) |
| 240 |
239
|
a1i |
⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( √ ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / ( 2 · ( √ ‘ 𝑦 ) ) ) ) ) |
| 241 |
|
fveq2 |
⊢ ( 𝑦 = ( 1 − ( 𝑥 ↑ 2 ) ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 242 |
241
|
oveq2d |
⊢ ( 𝑦 = ( 1 − ( 𝑥 ↑ 2 ) ) → ( 2 · ( √ ‘ 𝑦 ) ) = ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 243 |
242
|
oveq2d |
⊢ ( 𝑦 = ( 1 − ( 𝑥 ↑ 2 ) ) → ( 1 / ( 2 · ( √ ‘ 𝑦 ) ) ) = ( 1 / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 244 |
11 11 203 209 211 212 237 240 241 243
|
dvmptco |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · - ( 2 · 𝑥 ) ) ) ) |
| 245 |
|
mulneg2 |
⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · - 𝑥 ) = - ( 2 · 𝑥 ) ) |
| 246 |
218 12 245
|
sylancr |
⊢ ( 𝑥 ∈ 𝐷 → ( 2 · - 𝑥 ) = - ( 2 · 𝑥 ) ) |
| 247 |
246
|
oveq1d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 2 · - 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( - ( 2 · 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 248 |
12
|
negcld |
⊢ ( 𝑥 ∈ 𝐷 → - 𝑥 ∈ ℂ ) |
| 249 |
|
eldifn |
⊢ ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) → ¬ 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) |
| 250 |
249 1
|
eleq2s |
⊢ ( 𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) |
| 251 |
|
id |
⊢ ( 𝑥 = - 1 → 𝑥 = - 1 ) |
| 252 |
|
mnflt |
⊢ ( - 1 ∈ ℝ → -∞ < - 1 ) |
| 253 |
86 252
|
ax-mp |
⊢ -∞ < - 1 |
| 254 |
|
ubioc1 |
⊢ ( ( -∞ ∈ ℝ* ∧ - 1 ∈ ℝ* ∧ -∞ < - 1 ) → - 1 ∈ ( -∞ (,] - 1 ) ) |
| 255 |
51 132 253 254
|
mp3an |
⊢ - 1 ∈ ( -∞ (,] - 1 ) |
| 256 |
251 255
|
eqeltrdi |
⊢ ( 𝑥 = - 1 → 𝑥 ∈ ( -∞ (,] - 1 ) ) |
| 257 |
|
id |
⊢ ( 𝑥 = 1 → 𝑥 = 1 ) |
| 258 |
|
ltpnf |
⊢ ( 1 ∈ ℝ → 1 < +∞ ) |
| 259 |
89 258
|
ax-mp |
⊢ 1 < +∞ |
| 260 |
|
lbico1 |
⊢ ( ( 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 1 < +∞ ) → 1 ∈ ( 1 [,) +∞ ) ) |
| 261 |
133 121 259 260
|
mp3an |
⊢ 1 ∈ ( 1 [,) +∞ ) |
| 262 |
257 261
|
eqeltrdi |
⊢ ( 𝑥 = 1 → 𝑥 ∈ ( 1 [,) +∞ ) ) |
| 263 |
256 262
|
orim12i |
⊢ ( ( 𝑥 = - 1 ∨ 𝑥 = 1 ) → ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) ) |
| 264 |
263
|
orcoms |
⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) ) |
| 265 |
|
elun |
⊢ ( 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ↔ ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) ) |
| 266 |
264 265
|
sylibr |
⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) |
| 267 |
250 266
|
nsyl |
⊢ ( 𝑥 ∈ 𝐷 → ¬ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) |
| 268 |
|
1cnd |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → 1 ∈ ℂ ) |
| 269 |
17
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 𝑥 ↑ 2 ) ∈ ℂ ) |
| 270 |
19
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ ) |
| 271 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) |
| 272 |
270 271
|
sqr00d |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) = 0 ) |
| 273 |
268 269 272
|
subeq0d |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → 1 = ( 𝑥 ↑ 2 ) ) |
| 274 |
146 273
|
eqtr2id |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ) |
| 275 |
274
|
ex |
⊢ ( 𝑥 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 → ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ) ) |
| 276 |
|
sqeqor |
⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) ) |
| 277 |
16 276
|
mpan2 |
⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) ) |
| 278 |
275 277
|
sylibd |
⊢ ( 𝑥 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 → ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) ) |
| 279 |
278
|
necon3bd |
⊢ ( 𝑥 ∈ ℂ → ( ¬ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) ) |
| 280 |
12 267 279
|
sylc |
⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) |
| 281 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
| 282 |
|
divcan5 |
⊢ ( ( - 𝑥 ∈ ℂ ∧ ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · - 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 283 |
281 282
|
mp3an3 |
⊢ ( ( - 𝑥 ∈ ℂ ∧ ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) ) → ( ( 2 · - 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 284 |
248 112 280 283
|
syl12anc |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 2 · - 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 285 |
218 12 219
|
sylancr |
⊢ ( 𝑥 ∈ 𝐷 → ( 2 · 𝑥 ) ∈ ℂ ) |
| 286 |
285
|
negcld |
⊢ ( 𝑥 ∈ 𝐷 → - ( 2 · 𝑥 ) ∈ ℂ ) |
| 287 |
|
mulcl |
⊢ ( ( 2 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ) → ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 288 |
218 112 287
|
sylancr |
⊢ ( 𝑥 ∈ 𝐷 → ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 289 |
|
mulne0 |
⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) ) → ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 290 |
281 289
|
mpan |
⊢ ( ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) → ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 291 |
112 280 290
|
syl2anc |
⊢ ( 𝑥 ∈ 𝐷 → ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ≠ 0 ) |
| 292 |
286 288 291
|
divrec2d |
⊢ ( 𝑥 ∈ 𝐷 → ( - ( 2 · 𝑥 ) / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( 1 / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · - ( 2 · 𝑥 ) ) ) |
| 293 |
247 284 292
|
3eqtr3rd |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · - ( 2 · 𝑥 ) ) = ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 294 |
293
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( 2 · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · - ( 2 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 295 |
244 294
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 296 |
11 74 75 109 113 114 295
|
dvmptadd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( i + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 297 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ) → ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 298 |
13 20 297
|
sylancr |
⊢ ( 𝑥 ∈ ℂ → ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 299 |
12 298
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) |
| 300 |
299 248 112 280
|
divdird |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + - 𝑥 ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 301 |
|
ixi |
⊢ ( i · i ) = - 1 |
| 302 |
301
|
eqcomi |
⊢ - 1 = ( i · i ) |
| 303 |
302
|
oveq1i |
⊢ ( - 1 · 𝑥 ) = ( ( i · i ) · 𝑥 ) |
| 304 |
|
mulm1 |
⊢ ( 𝑥 ∈ ℂ → ( - 1 · 𝑥 ) = - 𝑥 ) |
| 305 |
|
mulass |
⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( i · i ) · 𝑥 ) = ( i · ( i · 𝑥 ) ) ) |
| 306 |
13 13 305
|
mp3an12 |
⊢ ( 𝑥 ∈ ℂ → ( ( i · i ) · 𝑥 ) = ( i · ( i · 𝑥 ) ) ) |
| 307 |
303 304 306
|
3eqtr3a |
⊢ ( 𝑥 ∈ ℂ → - 𝑥 = ( i · ( i · 𝑥 ) ) ) |
| 308 |
307
|
oveq1d |
⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( i · ( i · 𝑥 ) ) + ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 309 |
|
negcl |
⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ ) |
| 310 |
298 309
|
addcomd |
⊢ ( 𝑥 ∈ ℂ → ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + - 𝑥 ) = ( - 𝑥 + ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 311 |
13
|
a1i |
⊢ ( 𝑥 ∈ ℂ → i ∈ ℂ ) |
| 312 |
311 15 20
|
adddid |
⊢ ( 𝑥 ∈ ℂ → ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( i · ( i · 𝑥 ) ) + ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 313 |
308 310 312
|
3eqtr4d |
⊢ ( 𝑥 ∈ ℂ → ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + - 𝑥 ) = ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 314 |
12 313
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + - 𝑥 ) = ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 315 |
314
|
oveq1d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + - 𝑥 ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 316 |
72 112 280
|
divcan4d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = i ) |
| 317 |
316
|
oveq1d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( i · ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( i + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 318 |
300 315 317
|
3eqtr3rd |
⊢ ( 𝑥 ∈ 𝐷 → ( i + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 319 |
318
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( i + ( - 𝑥 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 320 |
296 319
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 321 |
|
logf1o |
⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log |
| 322 |
|
f1of |
⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log ) |
| 323 |
321 322
|
mp1i |
⊢ ( ⊤ → log : ( ℂ ∖ { 0 } ) ⟶ ran log ) |
| 324 |
|
snssi |
⊢ ( 0 ∈ ( -∞ (,] 0 ) → { 0 } ⊆ ( -∞ (,] 0 ) ) |
| 325 |
64 324
|
ax-mp |
⊢ { 0 } ⊆ ( -∞ (,] 0 ) |
| 326 |
|
sscon |
⊢ ( { 0 } ⊆ ( -∞ (,] 0 ) → ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) ) |
| 327 |
325 326
|
mp1i |
⊢ ( ⊤ → ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) ) |
| 328 |
323 327
|
feqresmpt |
⊢ ( ⊤ → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) |
| 329 |
328
|
oveq2d |
⊢ ( ⊤ → ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) ) |
| 330 |
238
|
dvlog |
⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) |
| 331 |
329 330
|
eqtr3di |
⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) ) |
| 332 |
|
fveq2 |
⊢ ( 𝑦 = ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) → ( log ‘ 𝑦 ) = ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 333 |
|
oveq2 |
⊢ ( 𝑦 = ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) → ( 1 / 𝑦 ) = ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 334 |
11 11 57 58 70 71 320 331 332 333
|
dvmptco |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 335 |
22 24
|
reccld |
⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 336 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ ℂ ) → ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 337 |
13 21 336
|
sylancr |
⊢ ( 𝑥 ∈ ℂ → ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 338 |
12 337
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ∈ ℂ ) |
| 339 |
335 338 112 280
|
divassd |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 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 |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 341 |
72 22 24
|
divcan4d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = i ) |
| 342 |
340 341
|
eqtr3d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = i ) |
| 343 |
342
|
oveq1d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 344 |
339 343
|
eqtr3d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 345 |
344
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) · ( ( i · ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 346 |
334 345
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 347 |
|
negicn |
⊢ - i ∈ ℂ |
| 348 |
347
|
a1i |
⊢ ( ⊤ → - i ∈ ℂ ) |
| 349 |
11 26 27 346 348
|
dvmptcmul |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) |
| 350 |
349
|
mptru |
⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( - i · ( log ‘ ( ( i · 𝑥 ) + ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 351 |
|
divass |
⊢ ( ( - i ∈ ℂ ∧ i ∈ ℂ ∧ ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) ) → ( ( - i · i ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 352 |
347 13 351
|
mp3an12 |
⊢ ( ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) → ( ( - i · i ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 353 |
112 280 352
|
syl2anc |
⊢ ( 𝑥 ∈ 𝐷 → ( ( - i · i ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) |
| 354 |
13 13
|
mulneg1i |
⊢ ( - i · i ) = - ( i · i ) |
| 355 |
301
|
negeqi |
⊢ - ( i · i ) = - - 1 |
| 356 |
|
negneg1e1 |
⊢ - - 1 = 1 |
| 357 |
354 355 356
|
3eqtri |
⊢ ( - i · i ) = 1 |
| 358 |
357
|
oveq1i |
⊢ ( ( - i · i ) / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) |
| 359 |
353 358
|
eqtr3di |
⊢ ( 𝑥 ∈ 𝐷 → ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 360 |
359
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( - i · ( i / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |
| 361 |
9 350 360
|
3eqtri |
⊢ ( ℂ D ( arcsin ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) |