dvrec

Description: Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 28-Dec-2016)

		Ref	Expression
	Assertion	dvrec	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}})$

Proof

Step	Hyp	Ref	Expression
1		dvfcn	$⊢ \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} ⟶ ℂ$
2		ssidd	$⊢ A \in ℂ \to ℂ \subseteq ℂ$
3		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
4		divcl	$⊢ (A \in ℂ \land x \in ℂ \land x \neq 0) \to \frac{A}{x} \in ℂ$
5	4	3expb	$⊢ (A \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{A}{x} \in ℂ$
6	3 5	sylan2b	$⊢ (A \in ℂ \land x \in (ℂ ∖ \{0\})) \to \frac{A}{x} \in ℂ$
7	6	fmpttd	$⊢ A \in ℂ \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) : ℂ ∖ \{0\} ⟶ ℂ$
8		difssd	$⊢ A \in ℂ \to ℂ ∖ \{0\} \subseteq ℂ$
9	2 7 8	dvbss	$⊢ A \in ℂ \to dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} \subseteq ℂ ∖ \{0\}$
10		simpr	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in (ℂ ∖ \{0\})$
11		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
12	11	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
13		cnn0opn	$⊢ ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
14		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\}) = ℂ ∖ \{0\}$
15	12 13 14	mp2an	$⊢ int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\}) = ℂ ∖ \{0\}$
16	10 15	eleqtrrdi	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\})$
17		eldifi	$⊢ y \in (ℂ ∖ \{0\}) \to y \in ℂ$
18	17	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
19	18	sqvald	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y^{2} = y y$
20	19	oveq2d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y^{2}} = \frac{A}{y y}$
21		simpl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to A \in ℂ$
22		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
23	22	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
24	21 18 18 23 23	divdiv1d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{\frac{A}{y}}{y} = \frac{A}{y y}$
25	20 24	eqtr4d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y^{2}} = \frac{\frac{A}{y}}{y}$
26	25	negeqd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} = - \frac{\frac{A}{y}}{y}$
27	21 18 23	divcld	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y} \in ℂ$
28	27 18 23	divnegd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{\frac{A}{y}}{y} = \frac{- \frac{A}{y}}{y}$
29	26 28	eqtrd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} = \frac{- \frac{A}{y}}{y}$
30	27	negcld	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y} \in ℂ$
31		eqid	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) = (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z})$
32	31	cdivcncf	$⊢ - \frac{A}{y} \in ℂ \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
33	30 32	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
34		oveq2	$⊢ z = y \to \frac{- \frac{A}{y}}{z} = \frac{- \frac{A}{y}}{y}$
35	33 10 34	cnmptlimc	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{- \frac{A}{y}}{y} \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y)$
36	29 35	eqeltrd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y)$
37		cncff	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
38	33 37	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
39	38	limcdif	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y = ({(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})}) {lim}_{ℂ} y$
40		eldifi	$⊢ z \in ((ℂ ∖ \{0\}) ∖ \{y\}) \to z \in (ℂ ∖ \{0\})$
41	40	adantl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \in (ℂ ∖ \{0\})$
42	41	eldifad	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \in ℂ$
43	17	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y \in ℂ$
44	42 43	subcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z - y \in ℂ$
45	27	adantr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{A}{y} \in ℂ$
46		eldifsni	$⊢ z \in (ℂ ∖ \{0\}) \to z \neq 0$
47	41 46	syl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \neq 0$
48	45 42 47	divcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{\frac{A}{y}}{z} \in ℂ$
49		mulneg12	$⊢ (z - y \in ℂ \land \frac{\frac{A}{y}}{z} \in ℂ) \to (- (z - y)) (\frac{\frac{A}{y}}{z}) = (z - y) (- \frac{\frac{A}{y}}{z})$
50	44 48 49	syl2anc	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (- (z - y)) (\frac{\frac{A}{y}}{z}) = (z - y) (- \frac{\frac{A}{y}}{z})$
51	43 42 48	subdird	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (y - z) (\frac{\frac{A}{y}}{z}) = y (\frac{\frac{A}{y}}{z}) - z (\frac{\frac{A}{y}}{z})$
52	42 43	negsubdi2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - (z - y) = y - z$
53	52	oveq1d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (- (z - y)) (\frac{\frac{A}{y}}{z}) = (y - z) (\frac{\frac{A}{y}}{z})$
54		oveq2	$⊢ x = z \to \frac{A}{x} = \frac{A}{z}$
55		eqid	$⊢ (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x})$
56		ovex	$⊢ \frac{A}{z} \in V$
57	54 55 56	fvmpt	$⊢ z \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) = \frac{A}{z}$
58	41 57	syl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) = \frac{A}{z}$
59		simpll	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to A \in ℂ$
60	22	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y \neq 0$
61	59 43 60	divcan2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y (\frac{A}{y}) = A$
62	61	oveq1d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{y (\frac{A}{y})}{z} = \frac{A}{z}$
63	43 45 42 47	divassd	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{y (\frac{A}{y})}{z} = y (\frac{\frac{A}{y}}{z})$
64	58 62 63	3eqtr2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) = y (\frac{\frac{A}{y}}{z})$
65		oveq2	$⊢ x = y \to \frac{A}{x} = \frac{A}{y}$
66		ovex	$⊢ \frac{A}{y} \in V$
67	65 55 66	fvmpt	$⊢ y \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = \frac{A}{y}$
68	67	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = \frac{A}{y}$
69	45 42 47	divcan2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z (\frac{\frac{A}{y}}{z}) = \frac{A}{y}$
70	68 69	eqtr4d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = z (\frac{\frac{A}{y}}{z})$
71	64 70	oveq12d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = y (\frac{\frac{A}{y}}{z}) - z (\frac{\frac{A}{y}}{z})$
72	51 53 71	3eqtr4d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (- (z - y)) (\frac{\frac{A}{y}}{z}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)$
73	45 42 47	divnegd	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - \frac{\frac{A}{y}}{z} = \frac{- \frac{A}{y}}{z}$
74	73	oveq2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (z - y) (- \frac{\frac{A}{y}}{z}) = (z - y) (\frac{- \frac{A}{y}}{z})$
75	50 72 74	3eqtr3d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = (z - y) (\frac{- \frac{A}{y}}{z})$
76	75	oveq1d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y} = \frac{(z - y) (\frac{- \frac{A}{y}}{z})}{z - y}$
77	45	negcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - \frac{A}{y} \in ℂ$
78	77 42 47	divcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{- \frac{A}{y}}{z} \in ℂ$
79		eldifsni	$⊢ z \in ((ℂ ∖ \{0\}) ∖ \{y\}) \to z \neq y$
80	79	adantl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \neq y$
81	42 43 80	subne0d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z - y \neq 0$
82	78 44 81	divcan3d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{(z - y) (\frac{- \frac{A}{y}}{z})}{z - y} = \frac{- \frac{A}{y}}{z}$
83	76 82	eqtrd	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y} = \frac{- \frac{A}{y}}{z}$
84	83	mpteq2dva	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{- \frac{A}{y}}{z})$
85		difss	$⊢ (ℂ ∖ \{0\}) ∖ \{y\} \subseteq ℂ ∖ \{0\}$
86		resmpt	$⊢ (ℂ ∖ \{0\}) ∖ \{y\} \subseteq ℂ ∖ \{0\} \to {(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})} = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{- \frac{A}{y}}{z})$
87	85 86	ax-mp	$⊢ {(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})} = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{- \frac{A}{y}}{z})$
88	84 87	eqtr4di	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) = {(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})}$
89	88	oveq1d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) {lim}_{ℂ} y = ({(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})}) {lim}_{ℂ} y$
90	39 89	eqtr4d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) {lim}_{ℂ} y$
91	36 90	eleqtrd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} \in ((z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) {lim}_{ℂ} y)$
92	11	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
93	92	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
94		eqid	$⊢ (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y})$
95		ssidd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to ℂ \subseteq ℂ$
96	7	adantr	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) : ℂ ∖ \{0\} ⟶ ℂ$
97		difssd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to ℂ ∖ \{0\} \subseteq ℂ$
98	93 11 94 95 96 97	eldv	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (y \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (- \frac{A}{y^{2}}) \leftrightarrow (y \in int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\}) \land - \frac{A}{y^{2}} \in ((z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{(x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) - (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y)}{z - y}) {lim}_{ℂ} y)))$
99	16 91 98	mpbir2and	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (- \frac{A}{y^{2}})$
100		vex	$⊢ y \in V$
101		negex	$⊢ - \frac{A}{y^{2}} \in V$
102	100 101	breldm	$⊢ y \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (- \frac{A}{y^{2}}) \to y \in dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
103	99 102	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
104	9 103	eqelssd	$⊢ A \in ℂ \to dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} = ℂ ∖ \{0\}$
105	104	feq2d	$⊢ A \in ℂ \to (\frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} ⟶ ℂ \leftrightarrow \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : ℂ ∖ \{0\} ⟶ ℂ)$
106	1 105	mpbii	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : ℂ ∖ \{0\} ⟶ ℂ$
107	106	ffnd	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} Fn (ℂ ∖ \{0\})$
108		negex	$⊢ - \frac{A}{x^{2}} \in V$
109	108	rgenw	$⊢ \forall x \in (ℂ ∖ \{0\}) - \frac{A}{x^{2}} \in V$
110		eqid	$⊢ (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) = (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}})$
111	110	fnmpt	$⊢ \forall x \in (ℂ ∖ \{0\}) - \frac{A}{x^{2}} \in V \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) Fn (ℂ ∖ \{0\})$
112	109 111	mp1i	$⊢ A \in ℂ \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) Fn (ℂ ∖ \{0\})$
113		ffun	$⊢ \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} ⟶ ℂ \to Fun \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
114	1 113	mp1i	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to Fun \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
115		funbrfv	$⊢ Fun \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} \to (y \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (- \frac{A}{y^{2}}) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (y) = - \frac{A}{y^{2}})$
116	114 99 115	sylc	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (y) = - \frac{A}{y^{2}}$
117		oveq1	$⊢ x = y \to x^{2} = y^{2}$
118	117	oveq2d	$⊢ x = y \to \frac{A}{x^{2}} = \frac{A}{y^{2}}$
119	118	negeqd	$⊢ x = y \to - \frac{A}{x^{2}} = - \frac{A}{y^{2}}$
120	119 110 101	fvmpt	$⊢ y \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) (y) = - \frac{A}{y^{2}}$
121	120	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) (y) = - \frac{A}{y^{2}}$
122	116 121	eqtr4d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (y) = (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) (y)$
123	107 112 122	eqfnfvd	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}})$

Metamath Proof Explorer

Theorem dvrec

Proof