Theorem 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	⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) )

Proof

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