dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 15046

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11872, to show that

. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)

**Assertion**
Ref	Expression
dveflem

Proof of Theorem dveflem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0cn 8035	. . 3
2		eqid 2196	. . . . 5
3	2	cntoptop 14853	. . . 4
4		unicntopcntop 14862	. . . . 5
5	4	ntrtop 14448	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2272	. 2
8		ax-1cn 7989	. . 3
9		1rp 9749	. . . . . 6
10		rpmincl 11420	. . . . . 6 $/\$ inf
11	9, 10	mpan2 425	. . . . 5 inf
12		breq1 4037	. . . . . . . 8 # #
13	12	elrab 2920	. . . . . . 7 # $/\$ #
14		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8343	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5565	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 4044	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 11363	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9752	. . . . . . . . . . . 12
20	19	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 8058	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11417	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1249	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 188	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2196	. . . . . . . . . . . . 13 # #
26		fveq2 5561	. . . . . . . . . . . . . . 15
27	26	oveq1d 5940	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5943	. . . . . . . . . . . . 13
30		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 134	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 11846	. . . . . . . . . . . . . . . 16
33		peano2cnm 8309	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8834	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5658	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5947	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 8059	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8354	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 11363	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 11363	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9788	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 11233	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 8242	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 527	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8834	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 8059	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8354	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 11363	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 8074	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10808	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 9081	. . . . . . . . . . . . . . . . . 18
61		4nn 9171	. . . . . . . . . . . . . . . . . 18
62		nndivre 9043	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 426	. . . . . . . . . . . . . . . . 17
64		remulcl 8024	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 413	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8354	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8836	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8830	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5941	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2229	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5941	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8385	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 8021	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 9283	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2196	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 11870	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 9066	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 9282	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9515	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 9281	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 8036	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 11847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11545	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	eqtr2di 2246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addlidd 8193	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2230	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 11875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	eqtr4di 2247	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 11873	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5940	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10838	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5936	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	eqtrdi 2245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2229	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5941	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 11873	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8410	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2229	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2237	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5565	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 11376	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2231	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2196	. . . . . . . . . . . . . . . . . . 19
116		eqid 2196	. . . . . . . . . . . . . . . . . . 19
117		2nn 9169	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 8058	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 8162	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 11872	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 4058	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 9067	. . . . . . . . . . . . . . . . . . 19
125		fac2 10840	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5935	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 9162	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2218	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5937	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5936	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 4076	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10809	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 8042	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 9180	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 9085	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulridi 8045	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 4061	. . . . . . . . . . . . . . . . . . . . 21
139		4re 9084	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 9104	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8920	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1348	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 146	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 8146	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 8984	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 8072	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10780	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulridd 8060	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 4060	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 8167	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10779	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 4060	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 11281	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9785	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9833	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 167	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 508	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 8168	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 4056	. . . . . . . . . 10 $/\$ $/\$ # $/\$ $/\$ #
165	164	ex 115	. . . . . . . . 9 $/\$ $/\$ # $/\$ #
166	24, 165	sylbid 150	. . . . . . . 8 $/\$ $/\$ # inf #
167	166	adantld 278	. . . . . . 7 $/\$ $/\$ # # $/\$ inf #
168	13, 167	sylan2b 287	. . . . . 6 $/\$ # # $/\$ inf #
169	168	ralrimiva 2570	. . . . 5 # # $/\$ inf #
170		brimralrspcev 4093	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 411	. . . 4 # # $/\$ #
172	171	rgen 2550	. . 3 # # $/\$ #
173		elrabi 2917	. . . . . . . . . 10 #
174		efcl 11846	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 8059	. . . . . . . . 9 #
177	175, 176	subcld 8354	. . . . . . . 8 #
178		breq1 4037	. . . . . . . . . 10 # #
179	178	elrab 2920	. . . . . . . . 9 # $/\$ #
180	179	simprbi 275	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8834	. . . . . . 7 #
182	25, 181	fmpti 5717	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8691	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 8036	. . . . 5
187	183, 185, 186	ellimc3ap 14981	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1373	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 944	. 2 # lim
190	2	cntoptopon 14852	. . . . 5 TopOn
191	190	toponrestid 14341	. . . 4 ↾_t
192	173	subid1d 8343	. . . . . . 7 #
193	192	oveq2d 5941	. . . . . 6 #
194		ef0 11854	. . . . . . . 8
195	194	oveq2i 5936	. . . . . . 7
196	195	oveq1i 5935	. . . . . 6
197	193, 196	eqtr2di 2246	. . . . 5 #
198	197	mpteq2ia 4120	. . . 4 # #
199		ssidd 3205	. . . 4
200		eff 11845	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 15002	. . 3 $/\$ # lim
203	202	mptru 1373	. 2 $/\$ # lim
204	7, 189, 203	mpbir2an 944	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1364

wtru 1365

wcel 2167

wral 2475

wrex 2476

crab 2479

wss 3157

cpr 3624 class class class wbr 4034

cmpt 4095

ccom 4668

wf 5255

cfv 5259 (class class class)co 5925 infcinf 7058

cc 7894

cr 7895

cc0 7896

c1 7897

caddc 7899

cmul 7901

clt 8078

cle 8079

cmin 8214 # cap 8625

cdiv 8716

cn 9007

c2 9058

c3 9059

c4 9060

cn0 9266

cuz 9618

crp 9745

cexp 10647

cfa 10834

cabs 11179

csu 11535

ce 11824

cmopn 14173

ctop 14317

cnt 14413 lim

climc 14974

cdv 14975

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-oadd 6487 df-er 6601 df-map 6718 df-pm 6719 df-en 6809 df-dom 6810 df-fin 6811 df-sup 7059 df-inf 7060 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-xneg 9864 df-xadd 9865 df-ico 9986 df-fz 10101 df-fzo 10235 df-seqfrec 10557 df-exp 10648 df-fac 10835 df-ihash 10885 df-shft 10997 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-sumdc 11536 df-ef 11830 df-rest 12943 df-topgen 12962 df-psmet 14175 df-xmet 14176 df-met 14177 df-bl 14178 df-mopn 14179 df-top 14318 df-topon 14331 df-bases 14363 df-ntr 14416 df-limced 14976 df-dvap 14977

This theorem is referenced by: dvef 15047

W3C validator