Step |
Hyp |
Ref |
Expression |
1 |
|
halfcn |
⊢ ( 1 / 2 ) ∈ ℂ |
2 |
|
dvcxp1 |
⊢ ( ( 1 / 2 ) ∈ ℂ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) |
4 |
|
rpcn |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ ) |
5 |
|
cxpsqrt |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) ) |
6 |
4 5
|
syl |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) ) |
7 |
6
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) |
8 |
7
|
oveq2i |
⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) |
9 |
|
1p0e1 |
⊢ ( 1 + 0 ) = 1 |
10 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
11 |
|
2halves |
⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 ) |
12 |
10 11
|
ax-mp |
⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 |
13 |
9 12
|
eqtr4i |
⊢ ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) |
14 |
|
0cn |
⊢ 0 ∈ ℂ |
15 |
|
addsubeq4 |
⊢ ( ( ( 1 ∈ ℂ ∧ 0 ∈ ℂ ) ∧ ( ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) ) → ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) ↔ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) ) ) |
16 |
10 14 1 1 15
|
mp4an |
⊢ ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) ↔ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) ) |
17 |
13 16
|
mpbi |
⊢ ( ( 1 / 2 ) − 1 ) = ( 0 − ( 1 / 2 ) ) |
18 |
|
df-neg |
⊢ - ( 1 / 2 ) = ( 0 − ( 1 / 2 ) ) |
19 |
17 18
|
eqtr4i |
⊢ ( ( 1 / 2 ) − 1 ) = - ( 1 / 2 ) |
20 |
19
|
oveq2i |
⊢ ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 𝑥 ↑𝑐 - ( 1 / 2 ) ) |
21 |
|
rpne0 |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 ) |
22 |
1
|
a1i |
⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 2 ) ∈ ℂ ) |
23 |
4 21 22
|
cxpnegd |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ↑𝑐 - ( 1 / 2 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) |
24 |
20 23
|
syl5eq |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ) |
25 |
6
|
oveq2d |
⊢ ( 𝑥 ∈ ℝ+ → ( 1 / ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) ) |
26 |
24 25
|
eqtrd |
⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) = ( 1 / ( √ ‘ 𝑥 ) ) ) |
27 |
26
|
oveq2d |
⊢ ( 𝑥 ∈ ℝ+ → ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) = ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) ) |
28 |
10
|
a1i |
⊢ ( 𝑥 ∈ ℝ+ → 1 ∈ ℂ ) |
29 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
30 |
29
|
a1i |
⊢ ( 𝑥 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) |
31 |
|
rpsqrtcl |
⊢ ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ ) |
32 |
31
|
rpcnne0d |
⊢ ( 𝑥 ∈ ℝ+ → ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ) |
33 |
|
divmuldiv |
⊢ ( ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ) ) → ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) = ( ( 1 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
34 |
28 28 30 32 33
|
syl22anc |
⊢ ( 𝑥 ∈ ℝ+ → ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) = ( ( 1 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
35 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
36 |
35
|
oveq1i |
⊢ ( ( 1 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) |
37 |
34 36
|
eqtrdi |
⊢ ( 𝑥 ∈ ℝ+ → ( ( 1 / 2 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
38 |
27 37
|
eqtrd |
⊢ ( 𝑥 ∈ ℝ+ → ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) = ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
39 |
38
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 2 ) · ( 𝑥 ↑𝑐 ( ( 1 / 2 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |
40 |
3 8 39
|
3eqtr3i |
⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) |