Step |
Hyp |
Ref |
Expression |
1 |
|
dvcncxp1.d |
⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) |
2 |
|
halfcn |
⊢ ( 1 / 2 ) ∈ ℂ |
3 |
1
|
dvcncxp1 |
⊢ ( ( 1 / 2 ) ∈ ℂ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) ) |
4 |
2 3
|
ax-mp |
⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) |
5 |
|
difss |
⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ |
6 |
1 5
|
eqsstri |
⊢ 𝐷 ⊆ ℂ |
7 |
6
|
sseli |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ ) |
8 |
|
cxpsqrt |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) ) |
9 |
7 8
|
syl |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) ) |
10 |
9
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) |
11 |
10
|
oveq2i |
⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) ) |
12 |
|
1p0e1 |
⊢ ( 1 + 0 ) = 1 |
13 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
14 |
|
2halves |
⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 ) |
15 |
13 14
|
ax-mp |
⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 |
16 |
12 15
|
eqtr4i |
⊢ ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) |
17 |
|
0cn |
⊢ 0 ∈ ℂ |
18 |
|
addsubeq4 |
⊢ ( ( ( 1 ∈ ℂ ∧ 0 ∈ ℂ ) ∧ ( ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) ) → ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) ↔ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) ) ) |
19 |
13 17 2 2 18
|
mp4an |
⊢ ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) ↔ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) ) |
20 |
16 19
|
mpbi |
⊢ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) |
21 |
|
df-neg |
⊢ - ( 1 / 2 ) = ( 0 − ( 1 / 2 ) ) |
22 |
20 21
|
eqtr4i |
⊢ ( ( 1 / 2 ) − 1 ) = - ( 1 / 2 ) |
23 |
22
|
oveq2i |
⊢ ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 𝑥 ↑𝑐 - ( 1 / 2 ) ) |
24 |
1
|
logdmn0 |
⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 ) |
25 |
2
|
a1i |
⊢ ( 𝑥 ∈ 𝐷 → ( 1 / 2 ) ∈ ℂ ) |
26 |
7 24 25
|
cxpnegd |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑𝑐 - ( 1 / 2 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) |
27 |
23 26
|
syl5eq |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) |
28 |
9
|
oveq2d |
⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) ) |
29 |
27 28
|
eqtrd |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 1 / ( √ ‘ 𝑥 ) ) ) |
30 |
29
|
oveq2d |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) = ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) ) |
31 |
|
1cnd |
⊢ ( 𝑥 ∈ 𝐷 → 1 ∈ ℂ ) |
32 |
|
2cnd |
⊢ ( 𝑥 ∈ 𝐷 → 2 ∈ ℂ ) |
33 |
7
|
sqrtcld |
⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ 𝑥 ) ∈ ℂ ) |
34 |
|
2ne0 |
⊢ 2 ≠ 0 |
35 |
34
|
a1i |
⊢ ( 𝑥 ∈ 𝐷 → 2 ≠ 0 ) |
36 |
7
|
adantr |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( √ ‘ 𝑥 ) = 0 ) → 𝑥 ∈ ℂ ) |
37 |
|
simpr |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( √ ‘ 𝑥 ) = 0 ) → ( √ ‘ 𝑥 ) = 0 ) |
38 |
36 37
|
sqr00d |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( √ ‘ 𝑥 ) = 0 ) → 𝑥 = 0 ) |
39 |
38
|
ex |
⊢ ( 𝑥 ∈ 𝐷 → ( ( √ ‘ 𝑥 ) = 0 → 𝑥 = 0 ) ) |
40 |
39
|
necon3d |
⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ≠ 0 → ( √ ‘ 𝑥 ) ≠ 0 ) ) |
41 |
24 40
|
mpd |
⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ 𝑥 ) ≠ 0 ) |
42 |
31 32 31 33 35 41
|
divmuldivd |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) = ( ( 1 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
43 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
44 |
43
|
oveq1i |
⊢ ( ( 1 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) |
45 |
42 44
|
eqtrdi |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
46 |
30 45
|
eqtrd |
⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
47 |
46
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
48 |
4 11 47
|
3eqtr3i |
⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |