Metamath Proof Explorer


Theorem dvsqrt

Description: The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016)

Ref Expression
Assertion dvsqrt ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) )

Proof

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 · ( √ ‘ 𝑥 ) ) ) )