dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 14664

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11733, 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 7980	. . 3
2		eqid 2189	. . . . 5
3	2	cntoptop 14510	. . . 4
4		unicntopcntop 14513	. . . . 5
5	4	ntrtop 14105	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2265	. 2
8		ax-1cn 7935	. . 3
9		1rp 9689	. . . . . 6
10		rpmincl 11281	. . . . . 6 $/\$ inf
11	9, 10	mpan2 425	. . . . 5 inf
12		breq1 4021	. . . . . . . 8 # #
13	12	elrab 2908	. . . . . . 7 # $/\$ #
14		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8288	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5538	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 4028	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 11225	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9692	. . . . . . . . . . . 12
20	19	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 8003	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11278	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1249	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 188	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2189	. . . . . . . . . . . . 13 # #
26		fveq2 5534	. . . . . . . . . . . . . . 15
27	26	oveq1d 5912	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5915	. . . . . . . . . . . . 13
30		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 134	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 11707	. . . . . . . . . . . . . . . 16
33		peano2cnm 8254	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8778	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5630	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5919	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 8004	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8299	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 11225	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 11225	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9728	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 11095	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 8187	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 527	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8778	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 8004	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8299	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 11225	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 8019	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10714	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 9024	. . . . . . . . . . . . . . . . . 18
61		4nn 9113	. . . . . . . . . . . . . . . . . 18
62		nndivre 8986	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 426	. . . . . . . . . . . . . . . . 17
64		remulcl 7970	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 413	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8299	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8780	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8818	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8774	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8330	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 7967	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 9224	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2189	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 11731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 9009	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 9223	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9456	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 9222	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 7981	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 11708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	eqtr2di 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addlidd 8138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2223	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 11736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	eqtr4di 2240	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 11734	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5912	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5908	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	eqtrdi 2238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5913	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 11734	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8355	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2230	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5538	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 11238	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2224	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2189	. . . . . . . . . . . . . . . . . . 19
116		eqid 2189	. . . . . . . . . . . . . . . . . . 19
117		2nn 9111	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 8003	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 8107	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 11733	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 4042	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 9010	. . . . . . . . . . . . . . . . . . 19
125		fac2 10746	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5907	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 9104	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2211	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5909	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5908	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 4060	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10715	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 7987	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 9122	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 9028	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulid1i 7990	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 4045	. . . . . . . . . . . . . . . . . . . . 21
139		4re 9027	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 9047	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8864	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1348	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 146	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 8091	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 8928	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 8017	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10686	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulridd 8005	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 4044	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 8112	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10685	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 4044	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 11143	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9725	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9773	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 167	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 508	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 8113	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 4040	. . . . . . . . . 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 2563	. . . . 5 # # $/\$ inf #
170		brimralrspcev 4077	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 411	. . . 4 # # $/\$ #
172	171	rgen 2543	. . 3 # # $/\$ #
173		elrabi 2905	. . . . . . . . . 10 #
174		efcl 11707	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 8004	. . . . . . . . 9 #
177	175, 176	subcld 8299	. . . . . . . 8 #
178		breq1 4021	. . . . . . . . . 10 # #
179	178	elrab 2908	. . . . . . . . 9 # $/\$ #
180	179	simprbi 275	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8778	. . . . . . 7 #
182	25, 181	fmpti 5689	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8635	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 7981	. . . . 5
187	183, 185, 186	ellimc3ap 14607	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1373	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 944	. 2 # lim
190	2	cntoptopon 14509	. . . . 5 TopOn
191	190	toponrestid 13998	. . . 4 ↾_t
192	173	subid1d 8288	. . . . . . 7 #
193	192	oveq2d 5913	. . . . . 6 #
194		ef0 11715	. . . . . . . 8
195	194	oveq2i 5908	. . . . . . 7
196	195	oveq1i 5907	. . . . . 6
197	193, 196	eqtr2di 2239	. . . . 5 #
198	197	mpteq2ia 4104	. . . 4 # #
199		ssidd 3191	. . . 4
200		eff 11706	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 14628	. . 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 2160

wral 2468

wrex 2469

crab 2472

wss 3144

cpr 3608 class class class wbr 4018

cmpt 4079

ccom 4648

wf 5231

cfv 5235 (class class class)co 5897 infcinf 7013

cc 7840

cr 7841

cc0 7842

c1 7843

caddc 7845

cmul 7847

clt 8023

cle 8024

cmin 8159 # cap 8569

cdiv 8660

cn 8950

c2 9001

c3 9002

c4 9003

cn0 9207

cuz 9559

crp 9685

cexp 10553

cfa 10740

cabs 11041

csu 11396

ce 11685

cmopn 13871

ctop 13974

cnt 14070 lim

climc 14600

cdv 14601

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-mulrcl 7941 ax-addcom 7942 ax-mulcom 7943 ax-addass 7944 ax-mulass 7945 ax-distr 7946 ax-i2m1 7947 ax-0lt1 7948 ax-1rid 7949 ax-0id 7950 ax-rnegex 7951 ax-precex 7952 ax-cnre 7953 ax-pre-ltirr 7954 ax-pre-ltwlin 7955 ax-pre-lttrn 7956 ax-pre-apti 7957 ax-pre-ltadd 7958 ax-pre-mulgt0 7959 ax-pre-mulext 7960 ax-arch 7961 ax-caucvg 7962

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 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5852 df-ov 5900 df-oprab 5901 df-mpo 5902 df-1st 6166 df-2nd 6167 df-recs 6331 df-irdg 6396 df-frec 6417 df-1o 6442 df-oadd 6446 df-er 6560 df-map 6677 df-pm 6678 df-en 6768 df-dom 6769 df-fin 6770 df-sup 7014 df-inf 7015 df-pnf 8025 df-mnf 8026 df-xr 8027 df-ltxr 8028 df-le 8029 df-sub 8161 df-neg 8162 df-reap 8563 df-ap 8570 df-div 8661 df-inn 8951 df-2 9009 df-3 9010 df-4 9011 df-n0 9208 df-z 9285 df-uz 9560 df-q 9652 df-rp 9686 df-xneg 9804 df-xadd 9805 df-ico 9926 df-fz 10041 df-fzo 10175 df-seqfrec 10479 df-exp 10554 df-fac 10741 df-ihash 10791 df-shft 10859 df-cj 10886 df-re 10887 df-im 10888 df-rsqrt 11042 df-abs 11043 df-clim 11322 df-sumdc 11397 df-ef 11691 df-rest 12749 df-topgen 12768 df-psmet 13873 df-xmet 13874 df-met 13875 df-bl 13876 df-mopn 13877 df-top 13975 df-topon 13988 df-bases 14020 df-ntr 14073 df-limced 14602 df-dvap 14603

This theorem is referenced by: dvef 14665

W3C validator