Step |
Hyp |
Ref |
Expression |
1 |
|
halfcn |
|- ( 1 / 2 ) e. CC |
2 |
|
dvcxp1 |
|- ( ( 1 / 2 ) e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) ) |
3 |
1 2
|
ax-mp |
|- ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) |
4 |
|
rpcn |
|- ( x e. RR+ -> x e. CC ) |
5 |
|
cxpsqrt |
|- ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) ) |
6 |
4 5
|
syl |
|- ( x e. RR+ -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) ) |
7 |
6
|
mpteq2ia |
|- ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) = ( x e. RR+ |-> ( sqrt ` x ) ) |
8 |
7
|
oveq2i |
|- ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) |
9 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
10 |
|
ax-1cn |
|- 1 e. CC |
11 |
|
2halves |
|- ( 1 e. CC -> ( ( 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 e. CC |
15 |
|
addsubeq4 |
|- ( ( ( 1 e. CC /\ 0 e. CC ) /\ ( ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) ) -> ( ( 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 |
|- -u ( 1 / 2 ) = ( 0 - ( 1 / 2 ) ) |
19 |
17 18
|
eqtr4i |
|- ( ( 1 / 2 ) - 1 ) = -u ( 1 / 2 ) |
20 |
19
|
oveq2i |
|- ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( x ^c -u ( 1 / 2 ) ) |
21 |
|
rpne0 |
|- ( x e. RR+ -> x =/= 0 ) |
22 |
1
|
a1i |
|- ( x e. RR+ -> ( 1 / 2 ) e. CC ) |
23 |
4 21 22
|
cxpnegd |
|- ( x e. RR+ -> ( x ^c -u ( 1 / 2 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) ) |
24 |
20 23
|
syl5eq |
|- ( x e. RR+ -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) ) |
25 |
6
|
oveq2d |
|- ( x e. RR+ -> ( 1 / ( x ^c ( 1 / 2 ) ) ) = ( 1 / ( sqrt ` x ) ) ) |
26 |
24 25
|
eqtrd |
|- ( x e. RR+ -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( sqrt ` x ) ) ) |
27 |
26
|
oveq2d |
|- ( x e. RR+ -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) ) |
28 |
10
|
a1i |
|- ( x e. RR+ -> 1 e. CC ) |
29 |
|
2cnne0 |
|- ( 2 e. CC /\ 2 =/= 0 ) |
30 |
29
|
a1i |
|- ( x e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) ) |
31 |
|
rpsqrtcl |
|- ( x e. RR+ -> ( sqrt ` x ) e. RR+ ) |
32 |
31
|
rpcnne0d |
|- ( x e. RR+ -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) |
33 |
|
divmuldiv |
|- ( ( ( 1 e. CC /\ 1 e. CC ) /\ ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) ) -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) ) |
34 |
28 28 30 32 33
|
syl22anc |
|- ( x e. RR+ -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) ) |
35 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
36 |
35
|
oveq1i |
|- ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) |
37 |
34 36
|
eqtrdi |
|- ( x e. RR+ -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) |
38 |
27 37
|
eqtrd |
|- ( x e. RR+ -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) |
39 |
38
|
mpteq2ia |
|- ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) |
40 |
3 8 39
|
3eqtr3i |
|- ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) |