dvrecap - Intuitionistic Logic Explorer

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

Theorem dvrecap 14365

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 5256	. . . . . . . . 9 #
2		funforn 5447	. . . . . . . . 9 # # # #
3	1, 2	mpbi 145	. . . . . . . 8 # # #
4		fof 5440	. . . . . . . 8 # # # # # #
5	3, 4	ax-mp 5	. . . . . . 7 # # #
6		simpl 109	. . . . . . . . . 10 $/\$ #
7		breq1 4008	. . . . . . . . . . . . . 14 # #
8	7	elrab 2895	. . . . . . . . . . . . 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 8750	. . . . . . . . 9 $/\$ #
14	13	ralrimiva 2550	. . . . . . . 8 #
15		eqid 2177	. . . . . . . . 9 # #
16	15	rnmptss 5680	. . . . . . . 8 # #
17	14, 16	syl 14	. . . . . . 7 #
18		fss 5379	. . . . . . 7 # # # $/\$ # # #
19	5, 17, 18	sylancr 414	. . . . . 6 # #
20	15	dmmpt 5126	. . . . . . 7 # #
21		ssrab2 3242	. . . . . . . 8 # #
22		ssrab2 3242	. . . . . . . 8 #
23	21, 22	sstri 3166	. . . . . . 7 #
24	20, 23	eqsstri 3189	. . . . . 6 #
25		cnex 7938	. . . . . . 7
26	25, 25	elpm2 6683	. . . . . 6 # # # $/\$ #
27	19, 24, 26	sylanblrc 416	. . . . 5 #
28		dvfcnpm 14347	. . . . 5 # # #
29	27, 28	syl 14	. . . 4 # #
30		ssidd 3178	. . . . . . 7
31		divclap 8638	. . . . . . . . . 10 $/\$ $/\$ #
32	31	3expb 1204	. . . . . . . . 9 $/\$ $/\$ #
33	8, 32	sylan2b 287	. . . . . . . 8 $/\$ #
34	33	fmpttd 5674	. . . . . . 7 # #
35	22	a1i 9	. . . . . . 7 #
36	30, 34, 35	dvbss 14342	. . . . . 6 # #
37		elrabi 2892	. . . . . . . 8 #
38	37	adantl 277	. . . . . . 7 $/\$ #
39		simpl 109	. . . . . . . . 9 $/\$ #
40	38	sqcld 10655	. . . . . . . . 9 $/\$ #
41		breq1 4008	. . . . . . . . . . . . 13 # #
42	41	elrab 2895	. . . . . . . . . . . 12 # $/\$ #
43	42	simprbi 275	. . . . . . . . . . 11 # #
44	43	adantl 277	. . . . . . . . . 10 $/\$ # #
45		sqap0 10590	. . . . . . . . . . 11 # #
46	38, 45	syl 14	. . . . . . . . . 10 $/\$ # # #
47	44, 46	mpbird 167	. . . . . . . . 9 $/\$ # #
48	39, 40, 47	divclapd 8750	. . . . . . . 8 $/\$ #
49	48	negcld 8258	. . . . . . 7 $/\$ #
50		simpr 110	. . . . . . . . 9 $/\$ # #
51		eqid 2177	. . . . . . . . . . 11
52	51	cntoptop 14221	. . . . . . . . . 10
53		0cn 7952	. . . . . . . . . . 11
54		cnopnap 14282	. . . . . . . . . . 11 #
55	53, 54	ax-mp 5	. . . . . . . . . 10 #
56		isopn3i 13823	. . . . . . . . . 10 $/\$ # # #
57	52, 55, 56	mp2an 426	. . . . . . . . 9 # #
58	50, 57	eleqtrrdi 2271	. . . . . . . 8 $/\$ # #
59	38	sqvald 10654	. . . . . . . . . . . . . 14 $/\$ #
60	59	oveq2d 5894	. . . . . . . . . . . . 13 $/\$ #
61	39, 38, 38, 44, 44	divdivap1d 8782	. . . . . . . . . . . . 13 $/\$ #
62	60, 61	eqtr4d 2213	. . . . . . . . . . . 12 $/\$ #
63	62	negeqd 8155	. . . . . . . . . . 11 $/\$ #
64	39, 38, 44	divclapd 8750	. . . . . . . . . . . 12 $/\$ #
65	64, 38, 44	divnegapd 8763	. . . . . . . . . . 11 $/\$ #
66	63, 65	eqtrd 2210	. . . . . . . . . 10 $/\$ #
67	64	negcld 8258	. . . . . . . . . . . 12 $/\$ #
68		eqid 2177	. . . . . . . . . . . . 13 # #
69	68	cdivcncfap 14275	. . . . . . . . . . . 12 # #
70	67, 69	syl 14	. . . . . . . . . . 11 $/\$ # # #
71		oveq2 5886	. . . . . . . . . . 11
72	70, 50, 71	cnmptlimc 14331	. . . . . . . . . 10 $/\$ # # lim
73	66, 72	eqeltrd 2254	. . . . . . . . 9 $/\$ # # lim
74		cncff 14252	. . . . . . . . . . . 12 # # # #
75	70, 74	syl 14	. . . . . . . . . . 11 $/\$ # # #
76	22	a1i 9	. . . . . . . . . . 11 $/\$ # #
77	75, 76	limcdifap 14319	. . . . . . . . . 10 $/\$ # # lim # # # lim
78		elrabi 2892	. . . . . . . . . . . . . . . . . . . . 21 # # #
79	78	adantl 277	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
80		breq1 4008	. . . . . . . . . . . . . . . . . . . . 21 # #
81	80	elrab 2895	. . . . . . . . . . . . . . . . . . . 20 # $/\$ #
82	79, 81	sylib 122	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # $/\$ #
83	82	simpld 112	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
84	37	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
85	83, 84	subcld 8271	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
86	64	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
87	81	simprbi 275	. . . . . . . . . . . . . . . . . . 19 # #
88	79, 87	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
89	86, 83, 88	divclapd 8750	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
90		mulneg12 8357	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
92	84, 83, 89	subdird 8375	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
93	83, 84	negsubdi2d 8287	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # #
94	93	oveq1d 5893	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
95		oveq2 5886	. . . . . . . . . . . . . . . . . . . 20
96		simpll 527	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # #
97	96, 83, 88	divclapd 8750	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
98	15, 95, 79, 97	fvmptd3 5612	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
99	43	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$ # # #
100	96, 84, 99	divcanap2d 8752	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # #
101	100	oveq1d 5893	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
102	84, 86, 83, 88	divassapd 8786	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
103	98, 101, 102	3eqtr2d 2216	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
104		oveq2 5886	. . . . . . . . . . . . . . . . . . . 20
105	50	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ # # #
106	15, 104, 105, 86	fvmptd3 5612	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # # #
107	86, 83, 88	divcanap2d 8752	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$ # #
108	106, 107	eqtr4d 2213	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$ # # #
109	103, 108	oveq12d 5896	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # # # #
110	92, 94, 109	3eqtr4d 2220	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # # #
111	86, 83, 88	divnegapd 8763	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ # #
112	111	oveq2d 5894	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
113	91, 110, 112	3eqtr3d 2218	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # # #
114	113	oveq1d 5893	. . . . . . . . . . . . . 14 $/\$ # $/\$ # # # #
115	86	negcld 8258	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # #
116	115, 83, 88	divclapd 8750	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # #
117		breq1 4008	. . . . . . . . . . . . . . . . . . 19 # #
118	117	elrab 2895	. . . . . . . . . . . . . . . . . 18 # # # $/\$ #
119	118	simprbi 275	. . . . . . . . . . . . . . . . 17 # # #
120	119	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ # $/\$ # # #
121	83, 84, 120	subap0d 8604	. . . . . . . . . . . . . . 15 $/\$ # $/\$ # # #
122	116, 85, 121	divcanap3d 8755	. . . . . . . . . . . . . 14 $/\$ # $/\$ # #
123	114, 122	eqtrd 2210	. . . . . . . . . . . . 13 $/\$ # $/\$ # # # #
124	123	mpteq2dva 4095	. . . . . . . . . . . 12 $/\$ # # # # # # #
125		ssrab2 3242	. . . . . . . . . . . . 13 # # #
126		resmpt 4957	. . . . . . . . . . . . 13 # # # # # # # #
127	125, 126	ax-mp 5	. . . . . . . . . . . 12 # # # # #
128	124, 127	eqtr4di 2228	. . . . . . . . . . 11 $/\$ # # # # # # # #
129	128	oveq1d 5893	. . . . . . . . . 10 $/\$ # # # # # lim # # # lim
130	77, 129	eqtr4d 2213	. . . . . . . . 9 $/\$ # # lim # # # # lim
131	73, 130	eleqtrd 2256	. . . . . . . 8 $/\$ # # # # # lim
132	51	cntoptopon 14220	. . . . . . . . . 10 TopOn
133	132	toponrestid 13709	. . . . . . . . 9 ↾_t
134		eqid 2177	. . . . . . . . 9 # # # # # # # #
135		ssidd 3178	. . . . . . . . 9 $/\$ #
136	34	adantr 276	. . . . . . . . 9 $/\$ # # #
137	133, 51, 134, 135, 136, 76	eldvap 14339	. . . . . . . 8 $/\$ # # # $/\$ # # # # lim
138	58, 131, 137	mpbir2and 944	. . . . . . 7 $/\$ # #
139		breldmg 4835	. . . . . . 7 $/\$ $/\$ # #
140	38, 49, 138, 139	syl3anc 1238	. . . . . 6 $/\$ # #
141	36, 140	eqelssd 3176	. . . . 5 # #
142	141	feq2d 5355	. . . 4 # # # #
143	29, 142	mpbid 147	. . 3 # #
144	143	ffnd 5368	. 2 # #
145	11	sqcld 10655	. . . . . 6 $/\$ #
146		sqap0 10590	. . . . . . . 8 # #
147	11, 146	syl 14	. . . . . . 7 $/\$ # # #
148	12, 147	mpbird 167	. . . . . 6 $/\$ # #
149	6, 145, 148	divclapd 8750	. . . . 5 $/\$ #
150	149	negcld 8258	. . . 4 $/\$ #
151	150	ralrimiva 2550	. . 3 #
152		eqid 2177	. . . 4 # #
153	152	fnmpt 5344	. . 3 # # #
154	151, 153	syl 14	. 2 # #
155	29	ffund 5371	. . . . 5 #
156	155	adantr 276	. . . 4 $/\$ # #
157		funbrfv 5557	. . . 4 # # #
158	156, 138, 157	sylc 62	. . 3 $/\$ # #
159		oveq1 5885	. . . . . 6
160	159	oveq2d 5894	. . . . 5
161	160	negeqd 8155	. . . 4
162	152, 161, 50, 49	fvmptd3 5612	. . 3 $/\$ # #
163	158, 162	eqtr4d 2213	. 2 $/\$ # # #
164	144, 154, 163	eqfnfvd 5619	1 # #

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1353

wcel 2148

wral 2455

crab 2459

cvv 2739

wss 3131 class class class wbr 4005

cmpt 4066

cdm 4628

crn 4629

cres 4630

ccom 4632

wfun 5212

wfn 5213

wf 5214

wfo 5216

cfv 5218 (class class class)co 5878

cpm 6652

cc 7812

cc0 7814

cmul 7819

cmin 8131

cneg 8132 # cap 8541

cdiv 8632

c2 8973

cexp 10522

cabs 11009

cmopn 13619

ctop 13685

cnt 13781

ccncf 14245 lim

climc 14311

cdv 14312

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7905 ax-resscn 7906 ax-1cn 7907 ax-1re 7908 ax-icn 7909 ax-addcl 7910 ax-addrcl 7911 ax-mulcl 7912 ax-mulrcl 7913 ax-addcom 7914 ax-mulcom 7915 ax-addass 7916 ax-mulass 7917 ax-distr 7918 ax-i2m1 7919 ax-0lt1 7920 ax-1rid 7921 ax-0id 7922 ax-rnegex 7923 ax-precex 7924 ax-cnre 7925 ax-pre-ltirr 7926 ax-pre-ltwlin 7927 ax-pre-lttrn 7928 ax-pre-apti 7929 ax-pre-ltadd 7930 ax-pre-mulgt0 7931 ax-pre-mulext 7932 ax-arch 7933 ax-caucvg 7934

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-isom 5227 df-riota 5834 df-ov 5881 df-oprab 5882 df-mpo 5883 df-1st 6144 df-2nd 6145 df-recs 6309 df-frec 6395 df-map 6653 df-pm 6654 df-sup 6986 df-inf 6987 df-pnf 7997 df-mnf 7998 df-xr 7999 df-ltxr 8000 df-le 8001 df-sub 8133 df-neg 8134 df-reap 8535 df-ap 8542 df-div 8633 df-inn 8923 df-2 8981 df-3 8982 df-4 8983 df-n0 9180 df-z 9257 df-uz 9532 df-q 9623 df-rp 9657 df-xneg 9775 df-xadd 9776 df-seqfrec 10449 df-exp 10523 df-cj 10854 df-re 10855 df-im 10856 df-rsqrt 11010 df-abs 11011 df-rest 12696 df-topgen 12715 df-psmet 13621 df-xmet 13622 df-met 13623 df-bl 13624 df-mopn 13625 df-top 13686 df-topon 13699 df-bases 13731 df-ntr 13784 df-cn 13876 df-cnp 13877 df-cncf 14246 df-limced 14313 df-dvap 14314

This theorem is referenced by: (None)

W3C validator