dvrecap - Intuitionistic Logic Explorer

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

Theorem dvrecap 15939

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 5418	. . . . . . . . 9 #
2		funforn 5625	. . . . . . . . 9 # # # #
3	1, 2	mpbi 145	. . . . . . . 8 # # #
4		fof 5618	. . . . . . . 8 # # # # # #
5	3, 4	ax-mp 5	. . . . . . 7 # # #
6		simpl 109	. . . . . . . . . 10 $/\$ #
7		breq1 4134	. . . . . . . . . . . . . 14 # #
8	7	elrab 2982	. . . . . . . . . . . . 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 9128	. . . . . . . . 9 $/\$ #
14	13	ralrimiva 2623	. . . . . . . 8 #
15		eqid 2238	. . . . . . . . 9 # #
16	15	rnmptss 5872	. . . . . . . 8 # #
17	14, 16	syl 14	. . . . . . 7 #
18		fss 5549	. . . . . . 7 # # # $/\$ # # #
19	5, 17, 18	sylancr 418	. . . . . 6 # #
20	15	dmmpt 5286	. . . . . . 7 # #
21		ssrab2 3333	. . . . . . . 8 # #
22		ssrab2 3333	. . . . . . . 8 #
23	21, 22	sstri 3257	. . . . . . 7 #
24	20, 23	eqsstri 3280	. . . . . 6 #
25		cnex 8309	. . . . . . 7
26	25, 25	elpm2 6965	. . . . . 6 # # # $/\$ #
27	19, 24, 26	sylanblrc 420	. . . . 5 #
28		dvfcnpm 15916	. . . . 5 # # #
29	27, 28	syl 14	. . . 4 # #
30		ssidd 3269	. . . . . . 7
31		divclap 9016	. . . . . . . . . 10 $/\$ $/\$ #
32	31	3expb 1235	. . . . . . . . 9 $/\$ $/\$ #
33	8, 32	sylan2b 287	. . . . . . . 8 $/\$ #
34	33	fmpttd 5866	. . . . . . 7 # #
35	22	a1i 9	. . . . . . 7 #
36	30, 34, 35	dvbss 15911	. . . . . 6 # #
37		elrabi 2979	. . . . . . . 8 #
38	37	adantl 277	. . . . . . 7 $/\$ #
39		simpl 109	. . . . . . . . 9 $/\$ #
40	38	sqcld 11130	. . . . . . . . 9 $/\$ #
41		breq1 4134	. . . . . . . . . . . . 13 # #
42	41	elrab 2982	. . . . . . . . . . . 12 # $/\$ #
43	42	simprbi 275	. . . . . . . . . . 11 # #
44	43	adantl 277	. . . . . . . . . 10 $/\$ # #
45		sqap0 11064	. . . . . . . . . . 11 # #
46	38, 45	syl 14	. . . . . . . . . 10 $/\$ # # #
47	44, 46	mpbird 167	. . . . . . . . 9 $/\$ # #
48	39, 40, 47	divclapd 9128	. . . . . . . 8 $/\$ #
49	48	negcld 8631	. . . . . . 7 $/\$ #
50		simpr 110	. . . . . . . . 9 $/\$ # #
51		eqid 2238	. . . . . . . . . . 11
52	51	cntoptop 15759	. . . . . . . . . 10
53		0cn 8324	. . . . . . . . . . 11
54		cnopnap 15837	. . . . . . . . . . 11 #
55	53, 54	ax-mp 5	. . . . . . . . . 10 #
56		isopn3i 15361	. . . . . . . . . 10 $/\$ # # #
57	52, 55, 56	mp2an 430	. . . . . . . . 9 # #
58	50, 57	eleqtrrdi 2332	. . . . . . . 8 $/\$ # #
59	38	sqvald 11129	. . . . . . . . . . . . . 14 $/\$ #
60	59	oveq2d 6104	. . . . . . . . . . . . 13 $/\$ #
61	39, 38, 38, 44, 44	divdivap1d 9160	. . . . . . . . . . . . 13 $/\$ #
62	60, 61	eqtr4d 2274	. . . . . . . . . . . 12 $/\$ #
63	62	negeqd 8528	. . . . . . . . . . 11 $/\$ #
64	39, 38, 44	divclapd 9128	. . . . . . . . . . . 12 $/\$ #
65	64, 38, 44	divnegapd 9141	. . . . . . . . . . 11 $/\$ #
66	63, 65	eqtrd 2271	. . . . . . . . . 10 $/\$ #
67	64	negcld 8631	. . . . . . . . . . . 12 $/\$ #
68		eqid 2238	. . . . . . . . . . . . 13 # #
69	68	cdivcncfap 15830	. . . . . . . . . . . 12 # #
70	67, 69	syl 14	. . . . . . . . . . 11 $/\$ # # #
71		oveq2 6096	. . . . . . . . . . 11
72	70, 50, 71	cnmptlimc 15900	. . . . . . . . . 10 $/\$ # # lim
73	66, 72	eqeltrd 2315	. . . . . . . . 9 $/\$ # # lim
74		cncff 15803	. . . . . . . . . . . 12 # # # #
75	70, 74	syl 14	. . . . . . . . . . 11 $/\$ # # #
76	22	a1i 9	. . . . . . . . . . 11 $/\$ # #
77	75, 76	limcdifap 15888	. . . . . . . . . 10 $/\$ # # lim # # # lim
78		elrabi 2979	. . . . . . . . . . . . . . . . . . . . 21 # # #
79	78	adantl 277	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
80		breq1 4134	. . . . . . . . . . . . . . . . . . . . 21 # #
81	80	elrab 2982	. . . . . . . . . . . . . . . . . . . 20 # $/\$ #
82	79, 81	sylib 122	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # $/\$ #
83	82	simpld 112	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
84	37	ad2antlr 493	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
85	83, 84	subcld 8644	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
86	64	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
87	81	simprbi 275	. . . . . . . . . . . . . . . . . . 19 # #
88	79, 87	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
89	86, 83, 88	divclapd 9128	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
90		mulneg12 8731	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
92	84, 83, 89	subdird 8749	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
93	83, 84	negsubdi2d 8660	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
94	93	oveq1d 6103	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
95		oveq2 6096	. . . . . . . . . . . . . . . . . . . 20
96		simpll 531	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # #
97	96, 83, 88	divclapd 9128	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
98	15, 95, 79, 97	fvmptd3 5802	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
99	43	ad2antlr 493	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # # #
100	96, 84, 99	divcanap2d 9130	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
101	100	oveq1d 6103	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
102	84, 86, 83, 88	divassapd 9164	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
103	98, 101, 102	3eqtr2d 2277	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
104		oveq2 6096	. . . . . . . . . . . . . . . . . . . 20
105	50	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
106	15, 104, 105, 86	fvmptd3 5802	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
107	86, 83, 88	divcanap2d 9130	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
108	106, 107	eqtr4d 2274	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
109	103, 108	oveq12d 6106	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # # # #
110	92, 94, 109	3eqtr4d 2281	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # # #
111	86, 83, 88	divnegapd 9141	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
112	111	oveq2d 6104	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
113	91, 110, 112	3eqtr3d 2279	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # # #
114	113	oveq1d 6103	. . . . . . . . . . . . . 14 $/\$ # $/\$ # # # #
115	86	negcld 8631	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
116	115, 83, 88	divclapd 9128	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # #
117		breq1 4134	. . . . . . . . . . . . . . . . . . 19 # #
118	117	elrab 2982	. . . . . . . . . . . . . . . . . 18 # # # $/\$ #
119	118	simprbi 275	. . . . . . . . . . . . . . . . 17 # # #
120	119	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # #
121	83, 84, 120	subap0d 8980	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # #
122	116, 85, 121	divcanap3d 9133	. . . . . . . . . . . . . 14 $/\$ # $/\$ # #
123	114, 122	eqtrd 2271	. . . . . . . . . . . . 13 $/\$ # $/\$ # # # #
124	123	mpteq2dva 4223	. . . . . . . . . . . 12 $/\$ # # # # # # #
125		ssrab2 3333	. . . . . . . . . . . . 13 # # #
126		resmpt 5114	. . . . . . . . . . . . 13 # # # # # # # #
127	125, 126	ax-mp 5	. . . . . . . . . . . 12 # # # # #
128	124, 127	eqtr4di 2289	. . . . . . . . . . 11 $/\$ # # # # # # # #
129	128	oveq1d 6103	. . . . . . . . . 10 $/\$ # # # # # lim # # # lim
130	77, 129	eqtr4d 2274	. . . . . . . . 9 $/\$ # # lim # # # # lim
131	73, 130	eleqtrd 2317	. . . . . . . 8 $/\$ # # # # # lim
132	51	cntoptopon 15758	. . . . . . . . . 10 TopOn
133	132	toponrestid 15247	. . . . . . . . 9 ↾_t
134		eqid 2238	. . . . . . . . 9 # # # # # # # #
135		ssidd 3269	. . . . . . . . 9 $/\$ #
136	34	adantr 276	. . . . . . . . 9 $/\$ # # #
137	133, 51, 134, 135, 136, 76	eldvap 15908	. . . . . . . 8 $/\$ # # # $/\$ # # # # lim
138	58, 131, 137	mpbir2and 957	. . . . . . 7 $/\$ # #
139		breldmg 4989	. . . . . . 7 $/\$ $/\$ # #
140	38, 49, 138, 139	syl3anc 1278	. . . . . 6 $/\$ # #
141	36, 140	eqelssd 3267	. . . . 5 # #
142	141	feq2d 5524	. . . 4 # # # #
143	29, 142	mpbid 147	. . 3 # #
144	143	ffnd 5537	. 2 # #
145	11	sqcld 11130	. . . . . 6 $/\$ #
146		sqap0 11064	. . . . . . . 8 # #
147	11, 146	syl 14	. . . . . . 7 $/\$ # # #
148	12, 147	mpbird 167	. . . . . 6 $/\$ # #
149	6, 145, 148	divclapd 9128	. . . . 5 $/\$ #
150	149	negcld 8631	. . . 4 $/\$ #
151	150	ralrimiva 2623	. . 3 #
152		eqid 2238	. . . 4 # #
153	152	fnmpt 5513	. . 3 # # #
154	151, 153	syl 14	. 2 # #
155	29	ffund 5540	. . . . 5 #
156	155	adantr 276	. . . 4 $/\$ # #
157		funbrfv 5742	. . . 4 # # #
158	156, 138, 157	sylc 62	. . 3 $/\$ # #
159		oveq1 6095	. . . . . 6
160	159	oveq2d 6104	. . . . 5
161	160	negeqd 8528	. . . 4
162	152, 161, 50, 49	fvmptd3 5802	. . 3 $/\$ # #
163	158, 162	eqtr4d 2274	. 2 $/\$ # # #
164	144, 154, 163	eqfnfvd 5812	1 # #

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4 $/\$ wa 104

wb 105

wceq 1402

wcel 2209

wral 2528

crab 2532

cvv 2821

wss 3220 class class class wbr 4131

cmpt 4193

cdm 4776

crn 4777

cres 4778

ccom 4780

wfun 5374

wfn 5375

wf 5376

wfo 5378

cfv 5380 (class class class)co 6088

cpm 6927

cc 8183

cc0 8185

cmul 8190

cmin 8504

cneg 8505 # cap 8917

cdiv 9010

c2 9364

cexp 10996

cabs 11785

cmopn 14987

ctop 15223

cnt 15319

ccncf 15796 lim

climc 15880

cdv 15881

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-frec 6666 df-map 6928 df-pm 6929 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-n0 9575 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-xneg 10191 df-xadd 10192 df-seqfrec 10906 df-exp 10997 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-rest 13654 df-topgen 13673 df-psmet 14989 df-xmet 14990 df-met 14991 df-bl 14992 df-mopn 14993 df-top 15224 df-topon 15237 df-bases 15269 df-ntr 15322 df-cn 15414 df-cnp 15415 df-cncf 15797 df-limced 15882 df-dvap 15883

This theorem is used by: (None)

W3C validator