dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 15313

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 12116, 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 8099	. . 3
2		eqid 2207	. . . . 5
3	2	cntoptop 15120	. . . 4
4		unicntopcntop 15129	. . . . 5
5	4	ntrtop 14715	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2283	. 2
8		ax-1cn 8053	. . 3
9		1rp 9814	. . . . . 6
10		rpmincl 11664	. . . . . 6 $/\$ inf
11	9, 10	mpan2 425	. . . . 5 inf
12		breq1 4062	. . . . . . . 8 # #
13	12	elrab 2936	. . . . . . 7 # $/\$ #
14		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8407	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5603	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 4069	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 11607	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9817	. . . . . . . . . . . 12
20	19	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 8122	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11661	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1250	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 188	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2207	. . . . . . . . . . . . 13 # #
26		fveq2 5599	. . . . . . . . . . . . . . 15
27	26	oveq1d 5982	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5985	. . . . . . . . . . . . 13
30		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 134	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 12090	. . . . . . . . . . . . . . . 16
33		peano2cnm 8373	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8898	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5696	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5989	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 8123	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8418	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 11607	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 11607	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9853	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 11477	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 8306	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 527	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8898	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 8123	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8418	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 11607	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 8138	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10881	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 9145	. . . . . . . . . . . . . . . . . 18
61		4nn 9235	. . . . . . . . . . . . . . . . . 18
62		nndivre 9107	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 426	. . . . . . . . . . . . . . . . 17
64		remulcl 8088	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 413	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8418	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8900	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8938	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8894	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2240	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8449	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 8085	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 9347	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2207	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 12114	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 9130	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 9346	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9580	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 9345	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 8100	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 12091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11789	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	eqtr2di 2257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addlidd 8257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2241	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 12119	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	eqtr4di 2258	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 12117	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10911	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	eqtrdi 2256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2240	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5983	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 12117	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2240	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2248	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5603	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 11620	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2242	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2207	. . . . . . . . . . . . . . . . . . 19
116		eqid 2207	. . . . . . . . . . . . . . . . . . 19
117		2nn 9233	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 8122	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 8226	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 12116	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 4083	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 9131	. . . . . . . . . . . . . . . . . . 19
125		fac2 10913	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5977	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 9226	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2229	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5979	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5978	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 4101	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10882	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 8106	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 9244	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 9149	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulridi 8109	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 4086	. . . . . . . . . . . . . . . . . . . . 21
139		4re 9148	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 9168	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8984	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1350	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 146	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 8210	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 9048	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 8136	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10853	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulridd 8124	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 4085	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 8231	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10852	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 4085	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 11525	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9850	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9898	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 167	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 508	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 8232	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 4081	. . . . . . . . . 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 2581	. . . . 5 # # $/\$ inf #
170		brimralrspcev 4119	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 411	. . . 4 # # $/\$ #
172	171	rgen 2561	. . 3 # # $/\$ #
173		elrabi 2933	. . . . . . . . . 10 #
174		efcl 12090	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 8123	. . . . . . . . 9 #
177	175, 176	subcld 8418	. . . . . . . 8 #
178		breq1 4062	. . . . . . . . . 10 # #
179	178	elrab 2936	. . . . . . . . 9 # $/\$ #
180	179	simprbi 275	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8898	. . . . . . 7 #
182	25, 181	fmpti 5755	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8755	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 8100	. . . . 5
187	183, 185, 186	ellimc3ap 15248	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1382	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 945	. 2 # lim
190	2	cntoptopon 15119	. . . . 5 TopOn
191	190	toponrestid 14608	. . . 4 ↾_t
192	173	subid1d 8407	. . . . . . 7 #
193	192	oveq2d 5983	. . . . . 6 #
194		ef0 12098	. . . . . . . 8
195	194	oveq2i 5978	. . . . . . 7
196	195	oveq1i 5977	. . . . . 6
197	193, 196	eqtr2di 2257	. . . . 5 #
198	197	mpteq2ia 4146	. . . 4 # #
199		ssidd 3222	. . . 4
200		eff 12089	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 15269	. . 3 $/\$ # lim
203	202	mptru 1382	. 2 $/\$ # lim
204	7, 189, 203	mpbir2an 945	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1373

wtru 1374

wcel 2178

wral 2486

wrex 2487

crab 2490

wss 3174

cpr 3644 class class class wbr 4059

cmpt 4121

ccom 4697

wf 5286

cfv 5290 (class class class)co 5967 infcinf 7111

cc 7958

cr 7959

cc0 7960

c1 7961

caddc 7963

cmul 7965

clt 8142

cle 8143

cmin 8278 # cap 8689

cdiv 8780

cn 9071

c2 9122

c3 9123

c4 9124

cn0 9330

cuz 9683

crp 9810

cexp 10720

cfa 10907

cabs 11423

csu 11779

ce 12068

cmopn 14418

ctop 14584

cnt 14680 lim

climc 15241

cdv 15242

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-coll 4175 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-iinf 4654 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-mulrcl 8059 ax-addcom 8060 ax-mulcom 8061 ax-addass 8062 ax-mulass 8063 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-1rid 8067 ax-0id 8068 ax-rnegex 8069 ax-precex 8070 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076 ax-pre-mulgt0 8077 ax-pre-mulext 8078 ax-arch 8079 ax-caucvg 8080

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rmo 2494 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-if 3580 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-po 4361 df-iso 4362 df-iord 4431 df-on 4433 df-ilim 4434 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-isom 5299 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-recs 6414 df-irdg 6479 df-frec 6500 df-1o 6525 df-oadd 6529 df-er 6643 df-map 6760 df-pm 6761 df-en 6851 df-dom 6852 df-fin 6853 df-sup 7112 df-inf 7113 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-reap 8683 df-ap 8690 df-div 8781 df-inn 9072 df-2 9130 df-3 9131 df-4 9132 df-n0 9331 df-z 9408 df-uz 9684 df-q 9776 df-rp 9811 df-xneg 9929 df-xadd 9930 df-ico 10051 df-fz 10166 df-fzo 10300 df-seqfrec 10630 df-exp 10721 df-fac 10908 df-ihash 10958 df-shft 11241 df-cj 11268 df-re 11269 df-im 11270 df-rsqrt 11424 df-abs 11425 df-clim 11705 df-sumdc 11780 df-ef 12074 df-rest 13188 df-topgen 13207 df-psmet 14420 df-xmet 14421 df-met 14422 df-bl 14423 df-mopn 14424 df-top 14585 df-topon 14598 df-bases 14630 df-ntr 14683 df-limced 15243 df-dvap 15244

This theorem is referenced by: dvef 15314

W3C validator