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