dvrecg

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

	Ref	Expression
Hypotheses	dvrecg.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvrecg.a	$⊢ φ \to A \in ℂ$
	dvrecg.b	$⊢ (φ \land x \in X) \to B \in (ℂ ∖ \{0\})$
	dvrecg.c	$⊢ (φ \land x \in X) \to C \in V$
	dvrecg.db	$⊢ φ \to \frac{d (x \in X⟼ B)}{d_{S} x} = (x \in X ⟼ C)$
Assertion	dvrecg	$⊢ φ \to \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x} = (x \in X ⟼ - \frac{A C}{B^{2}})$

Proof

Step	Hyp	Ref	Expression
1		dvrecg.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvrecg.a	$⊢ φ \to A \in ℂ$
3		dvrecg.b	$⊢ (φ \land x \in X) \to B \in (ℂ ∖ \{0\})$
4		dvrecg.c	$⊢ (φ \land x \in X) \to C \in V$
5		dvrecg.db	$⊢ φ \to \frac{d (x \in X⟼ B)}{d_{S} x} = (x \in X ⟼ C)$
6		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
7	6	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
8	2	adantr	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to A \in ℂ$
9		eldifi	$⊢ y \in (ℂ ∖ \{0\}) \to y \in ℂ$
10	9	adantl	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
11		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
12	11	adantl	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
13	8 10 12	divcld	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y} \in ℂ$
14	10	sqcld	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to y^{2} \in ℂ$
15		2z	$⊢ 2 \in ℤ$
16	15	a1i	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to 2 \in ℤ$
17	10 12 16	expne0d	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to y^{2} \neq 0$
18	8 14 17	divcld	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y^{2}} \in ℂ$
19	18	negcld	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} \in ℂ$
20		dvrec	$⊢ A \in ℂ \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{A}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{y^{2}})$
21	2 20	syl	$⊢ φ \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{A}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{y^{2}})$
22		oveq2	$⊢ y = B \to \frac{A}{y} = \frac{A}{B}$
23		oveq1	$⊢ y = B \to y^{2} = B^{2}$
24	23	oveq2d	$⊢ y = B \to \frac{A}{y^{2}} = \frac{A}{B^{2}}$
25	24	negeqd	$⊢ y = B \to - \frac{A}{y^{2}} = - \frac{A}{B^{2}}$
26	1 7 3 4 13 19 5 21 22 25	dvmptco	$⊢ φ \to \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x} = (x \in X ⟼ (- \frac{A}{B^{2}}) C)$
27	2	adantr	$⊢ (φ \land x \in X) \to A \in ℂ$
28		eldifi	$⊢ B \in (ℂ ∖ \{0\}) \to B \in ℂ$
29	3 28	syl	$⊢ (φ \land x \in X) \to B \in ℂ$
30	29	sqcld	$⊢ (φ \land x \in X) \to B^{2} \in ℂ$
31		eldifsn	$⊢ B \in (ℂ ∖ \{0\}) \leftrightarrow (B \in ℂ \land B \neq 0)$
32	3 31	sylib	$⊢ (φ \land x \in X) \to (B \in ℂ \land B \neq 0)$
33	32	simprd	$⊢ (φ \land x \in X) \to B \neq 0$
34	15	a1i	$⊢ (φ \land x \in X) \to 2 \in ℤ$
35	29 33 34	expne0d	$⊢ (φ \land x \in X) \to B^{2} \neq 0$
36	27 30 35	divcld	$⊢ (φ \land x \in X) \to \frac{A}{B^{2}} \in ℂ$
37	1 29 4 5	dvmptcl	$⊢ (φ \land x \in X) \to C \in ℂ$
38	36 37	mulneg1d	$⊢ (φ \land x \in X) \to (- \frac{A}{B^{2}}) C = - (\frac{A}{B^{2}}) C$
39	27 37 30 35	div23d	$⊢ (φ \land x \in X) \to \frac{A C}{B^{2}} = (\frac{A}{B^{2}}) C$
40	39	eqcomd	$⊢ (φ \land x \in X) \to (\frac{A}{B^{2}}) C = \frac{A C}{B^{2}}$
41	40	negeqd	$⊢ (φ \land x \in X) \to - (\frac{A}{B^{2}}) C = - \frac{A C}{B^{2}}$
42	38 41	eqtrd	$⊢ (φ \land x \in X) \to (- \frac{A}{B^{2}}) C = - \frac{A C}{B^{2}}$
43	42	mpteq2dva	$⊢ φ \to (x \in X ⟼ (- \frac{A}{B^{2}}) C) = (x \in X ⟼ - \frac{A C}{B^{2}})$
44	26 43	eqtrd	$⊢ φ \to \frac{d (x \in X⟼ \frac{A}{B})}{d_{S} x} = (x \in X ⟼ - \frac{A C}{B^{2}})$

Metamath Proof Explorer

Theorem dvrecg

Proof