Metamath Proof Explorer


Theorem dvcnsqrt

Description: Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018)

Ref Expression
Hypothesis dvcncxp1.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion dvcnsqrt ( ℂ D ( 𝑥𝐷 ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥𝐷 ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) )

Proof

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