This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvrecg

Description: Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvrecg.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvrecg.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
dvrecg.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
dvrecg.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ 𝑉 )
dvrecg.db ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
Assertion dvrecg ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ - ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvrecg.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvrecg.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3 dvrecg.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
4 dvrecg.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ 𝑉 )
5 dvrecg.db ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
6 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
7 6 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝐴 ∈ ℂ )
9 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
11 eldifsni ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
13 8 10 12 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / 𝑦 ) ∈ ℂ )
14 10 sqcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ↑ 2 ) ∈ ℂ )
15 2z ⊢ 2 ∈ ℤ
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 2 ∈ ℤ )
17 10 12 16 expne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ↑ 2 ) ≠ 0 )
18 8 14 17 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ ℂ )
19 18 negcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ ℂ )
20 dvrec ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ) )
21 2 20 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ) )
22 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 / 𝑦 ) = ( 𝐴 / 𝐵 ) )
23 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
24 23 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 / ( 𝑦 ↑ 2 ) ) = ( 𝐴 / ( 𝐵 ↑ 2 ) ) )
25 24 negeqd ⊢ ( 𝑦 = 𝐵 → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) = - ( 𝐴 / ( 𝐵 ↑ 2 ) ) )
26 1 7 3 4 13 19 5 21 22 25 dvmptco ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( - ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
28 eldifi ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) → 𝐵 ∈ ℂ )
29 3 28 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
30 29 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
31 eldifsn ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
32 3 31 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
33 32 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ≠ 0 )
34 15 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 2 ∈ ℤ )
35 29 33 34 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 ↑ 2 ) ≠ 0 )
36 27 30 35 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 / ( 𝐵 ↑ 2 ) ) ∈ ℂ )
37 1 29 4 5 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
38 36 37 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( - ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) = - ( ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) )
39 27 37 30 35 div23d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) )
40 39 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) )
41 40 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → - ( ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) = - ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) )
42 38 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( - ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) = - ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) )
43 42 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( - ( 𝐴 / ( 𝐵 ↑ 2 ) ) · 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ - ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) ) )
44 26 43 eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 / 𝐵 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ - ( ( 𝐴 · 𝐶 ) / ( 𝐵 ↑ 2 ) ) ) )