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	11	cnfldhaus	$⊢ TopOpen (ℂ_{fld}) \in Haus$
14		0cn	$⊢ 0 \in ℂ$
15		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
16	15	sncld	$⊢ (TopOpen (ℂ_{fld}) \in Haus \land 0 \in ℂ) \to \{0\} \in Clsd (TopOpen (ℂ_{fld}))$
17	13 14 16	mp2an	$⊢ \{0\} \in Clsd (TopOpen (ℂ_{fld}))$
18	15	cldopn	$⊢ \{0\} \in Clsd (TopOpen (ℂ_{fld})) \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
19	17 18	ax-mp	$⊢ ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
20		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\}) = ℂ ∖ \{0\}$
21	12 19 20	mp2an	$⊢ int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\}) = ℂ ∖ \{0\}$
22	10 21	eleqtrrdi	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in int (TopOpen (ℂ_{fld})) (ℂ ∖ \{0\})$
23		eldifi	$⊢ y \in (ℂ ∖ \{0\}) \to y \in ℂ$
24	23	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
25	24	sqvald	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y^{2} = y y$
26	25	oveq2d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y^{2}} = \frac{A}{y y}$
27		simpl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to A \in ℂ$
28		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
29	28	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
30	27 24 24 29 29	divdiv1d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{\frac{A}{y}}{y} = \frac{A}{y y}$
31	26 30	eqtr4d	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y^{2}} = \frac{\frac{A}{y}}{y}$
32	31	negeqd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} = - \frac{\frac{A}{y}}{y}$
33	27 24 29	divcld	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{A}{y} \in ℂ$
34	33 24 29	divnegd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{\frac{A}{y}}{y} = \frac{- \frac{A}{y}}{y}$
35	32 34	eqtrd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} = \frac{- \frac{A}{y}}{y}$
36	33	negcld	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y} \in ℂ$
37		eqid	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) = (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z})$
38	37	cdivcncf	$⊢ - \frac{A}{y} \in ℂ \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
39	36 38	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
40		oveq2	$⊢ z = y \to \frac{- \frac{A}{y}}{z} = \frac{- \frac{A}{y}}{y}$
41	39 10 40	cnmptlimc	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{- \frac{A}{y}}{y} \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y)$
42	35 41	eqeltrd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to - \frac{A}{y^{2}} \in ((z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) {lim}_{ℂ} y)$
43		cncff	$⊢ (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
44	39 43	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) : ℂ ∖ \{0\} ⟶ ℂ$
45	44	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$
46		eldifi	$⊢ z \in ((ℂ ∖ \{0\}) ∖ \{y\}) \to z \in (ℂ ∖ \{0\})$
47	46	adantl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \in (ℂ ∖ \{0\})$
48	47	eldifad	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \in ℂ$
49	23	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y \in ℂ$
50	48 49	subcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z - y \in ℂ$
51	33	adantr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{A}{y} \in ℂ$
52		eldifsni	$⊢ z \in (ℂ ∖ \{0\}) \to z \neq 0$
53	47 52	syl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \neq 0$
54	51 48 53	divcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{\frac{A}{y}}{z} \in ℂ$
55		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})$
56	50 54 55	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})$
57	49 48 54	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})$
58	48 49	negsubdi2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - (z - y) = y - z$
59	58	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})$
60		oveq2	$⊢ x = z \to \frac{A}{x} = \frac{A}{z}$
61		eqid	$⊢ (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x})$
62		ovex	$⊢ \frac{A}{z} \in V$
63	60 61 62	fvmpt	$⊢ z \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) = \frac{A}{z}$
64	47 63	syl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (z) = \frac{A}{z}$
65		simpll	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to A \in ℂ$
66	28	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y \neq 0$
67	65 49 66	divcan2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to y (\frac{A}{y}) = A$
68	67	oveq1d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{y (\frac{A}{y})}{z} = \frac{A}{z}$
69	49 51 48 53	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})$
70	64 68 69	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})$
71		oveq2	$⊢ x = y \to \frac{A}{x} = \frac{A}{y}$
72		ovex	$⊢ \frac{A}{y} \in V$
73	71 61 72	fvmpt	$⊢ y \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = \frac{A}{y}$
74	73	ad2antlr	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) (y) = \frac{A}{y}$
75	51 48 53	divcan2d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z (\frac{\frac{A}{y}}{z}) = \frac{A}{y}$
76	74 75	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})$
77	70 76	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})$
78	57 59 77	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)$
79	51 48 53	divnegd	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - \frac{\frac{A}{y}}{z} = \frac{- \frac{A}{y}}{z}$
80	79	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})$
81	56 78 80	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})$
82	81	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}$
83	51	negcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to - \frac{A}{y} \in ℂ$
84	83 48 53	divcld	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to \frac{- \frac{A}{y}}{z} \in ℂ$
85		eldifsni	$⊢ z \in ((ℂ ∖ \{0\}) ∖ \{y\}) \to z \neq y$
86	85	adantl	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z \neq y$
87	48 49 86	subne0d	$⊢ ((A \in ℂ \land y \in (ℂ ∖ \{0\})) \land z \in ((ℂ ∖ \{0\}) ∖ \{y\})) \to z - y \neq 0$
88	84 50 87	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}$
89	82 88	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}$
90	89	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})$
91		difss	$⊢ (ℂ ∖ \{0\}) ∖ \{y\} \subseteq ℂ ∖ \{0\}$
92		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})$
93	91 92	ax-mp	$⊢ {(z \in (ℂ ∖ \{0\}) ⟼ \frac{- \frac{A}{y}}{z}) ↾}_{((ℂ ∖ \{0\}) ∖ \{y\})} = (z \in ((ℂ ∖ \{0\}) ∖ \{y\}) ⟼ \frac{- \frac{A}{y}}{z})$
94	90 93	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\})}$
95	94	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$
96	45 95	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$
97	42 96	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)$
98	11	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
99	98	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
100		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})$
101		ssidd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to ℂ \subseteq ℂ$
102	7	adantr	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x \in (ℂ ∖ \{0\}) ⟼ \frac{A}{x}) : ℂ ∖ \{0\} ⟶ ℂ$
103		difssd	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to ℂ ∖ \{0\} \subseteq ℂ$
104	99 11 100 101 102 103	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)))$
105	22 97 104	mpbir2and	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (- \frac{A}{y^{2}})$
106		vex	$⊢ y \in V$
107		negex	$⊢ - \frac{A}{y^{2}} \in V$
108	106 107	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}$
109	105 108	syl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
110	9 109	eqelssd	$⊢ A \in ℂ \to dom \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} = ℂ ∖ \{0\}$
111	110	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\} ⟶ ℂ)$
112	1 111	mpbii	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} : ℂ ∖ \{0\} ⟶ ℂ$
113	112	ffnd	$⊢ A \in ℂ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} Fn (ℂ ∖ \{0\})$
114		negex	$⊢ - \frac{A}{x^{2}} \in V$
115	114	rgenw	$⊢ \forall x \in (ℂ ∖ \{0\}) - \frac{A}{x^{2}} \in V$
116		eqid	$⊢ (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) = (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}})$
117	116	fnmpt	$⊢ \forall x \in (ℂ ∖ \{0\}) - \frac{A}{x^{2}} \in V \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) Fn (ℂ ∖ \{0\})$
118	115 117	mp1i	$⊢ A \in ℂ \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) Fn (ℂ ∖ \{0\})$
119		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}$
120	1 119	mp1i	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to Fun \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x}$
121		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}})$
122	120 105 121	sylc	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{A}{x})}{d_{ℂ} x} (y) = - \frac{A}{y^{2}}$
123		oveq1	$⊢ x = y \to x^{2} = y^{2}$
124	123	oveq2d	$⊢ x = y \to \frac{A}{x^{2}} = \frac{A}{y^{2}}$
125	124	negeqd	$⊢ x = y \to - \frac{A}{x^{2}} = - \frac{A}{y^{2}}$
126	125 116 107	fvmpt	$⊢ y \in (ℂ ∖ \{0\}) \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) (y) = - \frac{A}{y^{2}}$
127	126	adantl	$⊢ (A \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x \in (ℂ ∖ \{0\}) ⟼ - \frac{A}{x^{2}}) (y) = - \frac{A}{y^{2}}$
128	122 127	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)$
129	113 118 128	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