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 ) ) ) )