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 eqtrid ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑𝑐 ( ( 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 · ( √ ‘ 𝑥 ) ) ) )