dvrecap - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dvrecap		Unicode version

Theorem dvrecap 14473

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

**Assertion**
Ref	Expression
dvrecap	# #

Distinct variable group:

Proof of Theorem dvrecap Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funmpt 5266	. . . . . . . . 9 #
2		funforn 5457	. . . . . . . . 9 # # # #
3	1, 2	mpbi 145	. . . . . . . 8 # # #
4		fof 5450	. . . . . . . 8 # # # # # #
5	3, 4	ax-mp 5	. . . . . . 7 # # #
6		simpl 109	. . . . . . . . . 10 $/\$ #
7		breq1 4018	. . . . . . . . . . . . . 14 # #
8	7	elrab 2905	. . . . . . . . . . . . 13 # $/\$ #
9	8	biimpi 120	. . . . . . . . . . . 12 # $/\$ #
10	9	adantl 277	. . . . . . . . . . 11 $/\$ # $/\$ #
11	10	simpld 112	. . . . . . . . . 10 $/\$ #
12	10	simprd 114	. . . . . . . . . 10 $/\$ # #
13	6, 11, 12	divclapd 8761	. . . . . . . . 9 $/\$ #
14	13	ralrimiva 2560	. . . . . . . 8 #
15		eqid 2187	. . . . . . . . 9 # #
16	15	rnmptss 5690	. . . . . . . 8 # #
17	14, 16	syl 14	. . . . . . 7 #
18		fss 5389	. . . . . . 7 # # # $/\$ # # #
19	5, 17, 18	sylancr 414	. . . . . 6 # #
20	15	dmmpt 5136	. . . . . . 7 # #
21		ssrab2 3252	. . . . . . . 8 # #
22		ssrab2 3252	. . . . . . . 8 #
23	21, 22	sstri 3176	. . . . . . 7 #
24	20, 23	eqsstri 3199	. . . . . 6 #
25		cnex 7949	. . . . . . 7
26	25, 25	elpm2 6694	. . . . . 6 # # # $/\$ #
27	19, 24, 26	sylanblrc 416	. . . . 5 #
28		dvfcnpm 14455	. . . . 5 # # #
29	27, 28	syl 14	. . . 4 # #
30		ssidd 3188	. . . . . . 7
31		divclap 8649	. . . . . . . . . 10 $/\$ $/\$ #
32	31	3expb 1205	. . . . . . . . 9 $/\$ $/\$ #
33	8, 32	sylan2b 287	. . . . . . . 8 $/\$ #
34	33	fmpttd 5684	. . . . . . 7 # #
35	22	a1i 9	. . . . . . 7 #
36	30, 34, 35	dvbss 14450	. . . . . 6 # #
37		elrabi 2902	. . . . . . . 8 #
38	37	adantl 277	. . . . . . 7 $/\$ #
39		simpl 109	. . . . . . . . 9 $/\$ #
40	38	sqcld 10666	. . . . . . . . 9 $/\$ #
41		breq1 4018	. . . . . . . . . . . . 13 # #
42	41	elrab 2905	. . . . . . . . . . . 12 # $/\$ #
43	42	simprbi 275	. . . . . . . . . . 11 # #
44	43	adantl 277	. . . . . . . . . 10 $/\$ # #
45		sqap0 10601	. . . . . . . . . . 11 # #
46	38, 45	syl 14	. . . . . . . . . 10 $/\$ # # #
47	44, 46	mpbird 167	. . . . . . . . 9 $/\$ # #
48	39, 40, 47	divclapd 8761	. . . . . . . 8 $/\$ #
49	48	negcld 8269	. . . . . . 7 $/\$ #
50		simpr 110	. . . . . . . . 9 $/\$ # #
51		eqid 2187	. . . . . . . . . . 11
52	51	cntoptop 14329	. . . . . . . . . 10
53		0cn 7963	. . . . . . . . . . 11
54		cnopnap 14390	. . . . . . . . . . 11 #
55	53, 54	ax-mp 5	. . . . . . . . . 10 #
56		isopn3i 13931	. . . . . . . . . 10 $/\$ # # #
57	52, 55, 56	mp2an 426	. . . . . . . . 9 # #
58	50, 57	eleqtrrdi 2281	. . . . . . . 8 $/\$ # #
59	38	sqvald 10665	. . . . . . . . . . . . . 14 $/\$ #
60	59	oveq2d 5904	. . . . . . . . . . . . 13 $/\$ #
61	39, 38, 38, 44, 44	divdivap1d 8793	. . . . . . . . . . . . 13 $/\$ #
62	60, 61	eqtr4d 2223	. . . . . . . . . . . 12 $/\$ #
63	62	negeqd 8166	. . . . . . . . . . 11 $/\$ #
64	39, 38, 44	divclapd 8761	. . . . . . . . . . . 12 $/\$ #
65	64, 38, 44	divnegapd 8774	. . . . . . . . . . 11 $/\$ #
66	63, 65	eqtrd 2220	. . . . . . . . . 10 $/\$ #
67	64	negcld 8269	. . . . . . . . . . . 12 $/\$ #
68		eqid 2187	. . . . . . . . . . . . 13 # #
69	68	cdivcncfap 14383	. . . . . . . . . . . 12 # #
70	67, 69	syl 14	. . . . . . . . . . 11 $/\$ # # #
71		oveq2 5896	. . . . . . . . . . 11
72	70, 50, 71	cnmptlimc 14439	. . . . . . . . . 10 $/\$ # # lim
73	66, 72	eqeltrd 2264	. . . . . . . . 9 $/\$ # # lim
74		cncff 14360	. . . . . . . . . . . 12 # # # #
75	70, 74	syl 14	. . . . . . . . . . 11 $/\$ # # #
76	22	a1i 9	. . . . . . . . . . 11 $/\$ # #
77	75, 76	limcdifap 14427	. . . . . . . . . 10 $/\$ # # lim # # # lim
78		elrabi 2902	. . . . . . . . . . . . . . . . . . . . 21 # # #
79	78	adantl 277	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
80		breq1 4018	. . . . . . . . . . . . . . . . . . . . 21 # #
81	80	elrab 2905	. . . . . . . . . . . . . . . . . . . 20 # $/\$ #
82	79, 81	sylib 122	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # $/\$ #
83	82	simpld 112	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
84	37	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
85	83, 84	subcld 8282	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
86	64	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
87	81	simprbi 275	. . . . . . . . . . . . . . . . . . 19 # #
88	79, 87	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
89	86, 83, 88	divclapd 8761	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
90		mulneg12 8368	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
92	84, 83, 89	subdird 8386	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
93	83, 84	negsubdi2d 8298	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
94	93	oveq1d 5903	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
95		oveq2 5896	. . . . . . . . . . . . . . . . . . . 20
96		simpll 527	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # #
97	96, 83, 88	divclapd 8761	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
98	15, 95, 79, 97	fvmptd3 5622	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
99	43	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # # #
100	96, 84, 99	divcanap2d 8763	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
101	100	oveq1d 5903	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
102	84, 86, 83, 88	divassapd 8797	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
103	98, 101, 102	3eqtr2d 2226	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
104		oveq2 5896	. . . . . . . . . . . . . . . . . . . 20
105	50	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
106	15, 104, 105, 86	fvmptd3 5622	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
107	86, 83, 88	divcanap2d 8763	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
108	106, 107	eqtr4d 2223	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
109	103, 108	oveq12d 5906	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # # # #
110	92, 94, 109	3eqtr4d 2230	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # # #
111	86, 83, 88	divnegapd 8774	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
112	111	oveq2d 5904	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
113	91, 110, 112	3eqtr3d 2228	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # # #
114	113	oveq1d 5903	. . . . . . . . . . . . . 14 $/\$ # $/\$ # # # #
115	86	negcld 8269	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
116	115, 83, 88	divclapd 8761	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # #
117		breq1 4018	. . . . . . . . . . . . . . . . . . 19 # #
118	117	elrab 2905	. . . . . . . . . . . . . . . . . 18 # # # $/\$ #
119	118	simprbi 275	. . . . . . . . . . . . . . . . 17 # # #
120	119	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # #
121	83, 84, 120	subap0d 8615	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # #
122	116, 85, 121	divcanap3d 8766	. . . . . . . . . . . . . 14 $/\$ # $/\$ # #
123	114, 122	eqtrd 2220	. . . . . . . . . . . . 13 $/\$ # $/\$ # # # #
124	123	mpteq2dva 4105	. . . . . . . . . . . 12 $/\$ # # # # # # #
125		ssrab2 3252	. . . . . . . . . . . . 13 # # #
126		resmpt 4967	. . . . . . . . . . . . 13 # # # # # # # #
127	125, 126	ax-mp 5	. . . . . . . . . . . 12 # # # # #
128	124, 127	eqtr4di 2238	. . . . . . . . . . 11 $/\$ # # # # # # # #
129	128	oveq1d 5903	. . . . . . . . . 10 $/\$ # # # # # lim # # # lim
130	77, 129	eqtr4d 2223	. . . . . . . . 9 $/\$ # # lim # # # # lim
131	73, 130	eleqtrd 2266	. . . . . . . 8 $/\$ # # # # # lim
132	51	cntoptopon 14328	. . . . . . . . . 10 TopOn
133	132	toponrestid 13817	. . . . . . . . 9 ↾_t
134		eqid 2187	. . . . . . . . 9 # # # # # # # #
135		ssidd 3188	. . . . . . . . 9 $/\$ #
136	34	adantr 276	. . . . . . . . 9 $/\$ # # #
137	133, 51, 134, 135, 136, 76	eldvap 14447	. . . . . . . 8 $/\$ # # # $/\$ # # # # lim
138	58, 131, 137	mpbir2and 945	. . . . . . 7 $/\$ # #
139		breldmg 4845	. . . . . . 7 $/\$ $/\$ # #
140	38, 49, 138, 139	syl3anc 1248	. . . . . 6 $/\$ # #
141	36, 140	eqelssd 3186	. . . . 5 # #
142	141	feq2d 5365	. . . 4 # # # #
143	29, 142	mpbid 147	. . 3 # #
144	143	ffnd 5378	. 2 # #
145	11	sqcld 10666	. . . . . 6 $/\$ #
146		sqap0 10601	. . . . . . . 8 # #
147	11, 146	syl 14	. . . . . . 7 $/\$ # # #
148	12, 147	mpbird 167	. . . . . 6 $/\$ # #
149	6, 145, 148	divclapd 8761	. . . . 5 $/\$ #
150	149	negcld 8269	. . . 4 $/\$ #
151	150	ralrimiva 2560	. . 3 #
152		eqid 2187	. . . 4 # #
153	152	fnmpt 5354	. . 3 # # #
154	151, 153	syl 14	. 2 # #
155	29	ffund 5381	. . . . 5 #
156	155	adantr 276	. . . 4 $/\$ # #
157		funbrfv 5567	. . . 4 # # #
158	156, 138, 157	sylc 62	. . 3 $/\$ # #
159		oveq1 5895	. . . . . 6
160	159	oveq2d 5904	. . . . 5
161	160	negeqd 8166	. . . 4
162	152, 161, 50, 49	fvmptd3 5622	. . 3 $/\$ # #
163	158, 162	eqtr4d 2223	. 2 $/\$ # # #
164	144, 154, 163	eqfnfvd 5629	1 # #

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1363

wcel 2158

wral 2465

crab 2469

cvv 2749

wss 3141 class class class wbr 4015

cmpt 4076

cdm 4638

crn 4639

cres 4640

ccom 4642

wfun 5222

wfn 5223

wf 5224

wfo 5226

cfv 5228 (class class class)co 5888

cpm 6663

cc 7823

cc0 7825

cmul 7830

cmin 8142

cneg 8143 # cap 8552

cdiv 8643

c2 8984

cexp 10533

cabs 11020

cmopn 13727

ctop 13793

cnt 13889

ccncf 14353 lim

climc 14419

cdv 14420

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944 ax-caucvg 7945

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-isom 5237 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-frec 6406 df-map 6664 df-pm 6665 df-sup 6997 df-inf 6998 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-2 8992 df-3 8993 df-4 8994 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-xneg 9786 df-xadd 9787 df-seqfrec 10460 df-exp 10534 df-cj 10865 df-re 10866 df-im 10867 df-rsqrt 11021 df-abs 11022 df-rest 12708 df-topgen 12727 df-psmet 13729 df-xmet 13730 df-met 13731 df-bl 13732 df-mopn 13733 df-top 13794 df-topon 13807 df-bases 13839 df-ntr 13892 df-cn 13984 df-cnp 13985 df-cncf 14354 df-limced 14421 df-dvap 14422

This theorem is referenced by: (None)

W3C validator