dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 14872

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11833, 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 8011	. . 3
2		eqid 2193	. . . . 5
3	2	cntoptop 14701	. . . 4
4		unicntopcntop 14704	. . . . 5
5	4	ntrtop 14296	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2269	. 2
8		ax-1cn 7965	. . 3
9		1rp 9723	. . . . . 6
10		rpmincl 11381	. . . . . 6 $/\$ inf
11	9, 10	mpan2 425	. . . . 5 inf
12		breq1 4032	. . . . . . . 8 # #
13	12	elrab 2916	. . . . . . 7 # $/\$ #
14		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8319	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5558	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 4039	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 11325	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9726	. . . . . . . . . . . 12
20	19	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 8034	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11378	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1249	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 188	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2193	. . . . . . . . . . . . 13 # #
26		fveq2 5554	. . . . . . . . . . . . . . 15
27	26	oveq1d 5933	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5936	. . . . . . . . . . . . 13
30		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 134	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 11807	. . . . . . . . . . . . . . . 16
33		peano2cnm 8285	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8809	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5651	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5940	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 8035	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8330	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 11325	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 11325	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9762	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 11195	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 8218	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 527	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8809	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 8035	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8330	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 11325	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 8050	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10770	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 9056	. . . . . . . . . . . . . . . . . 18
61		4nn 9145	. . . . . . . . . . . . . . . . . 18
62		nndivre 9018	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 426	. . . . . . . . . . . . . . . . 17
64		remulcl 8000	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 413	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8330	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8811	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8849	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8805	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8361	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 7997	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 9257	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2193	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 11831	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 9041	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 9256	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9489	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 9255	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 8012	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 11808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11506	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	eqtr2di 2243	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addlidd 8169	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2227	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 11836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	eqtr4di 2244	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 11834	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	eqtrdi 2242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2226	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 11834	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8386	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2226	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2234	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5558	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 11338	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2228	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2193	. . . . . . . . . . . . . . . . . . 19
116		eqid 2193	. . . . . . . . . . . . . . . . . . 19
117		2nn 9143	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 8034	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 8138	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 11833	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 4053	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 9042	. . . . . . . . . . . . . . . . . . 19
125		fac2 10802	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5928	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 9136	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2215	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5930	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5929	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 4071	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10771	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 8018	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 9154	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 9060	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulid1i 8021	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 4056	. . . . . . . . . . . . . . . . . . . . 21
139		4re 9059	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 9079	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8895	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1348	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 146	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 8122	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 8959	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 8048	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10742	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulridd 8036	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 4055	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 8143	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10741	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 4055	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 11243	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9759	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9807	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 167	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 508	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 8144	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 4051	. . . . . . . . . 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 2567	. . . . 5 # # $/\$ inf #
170		brimralrspcev 4088	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 411	. . . 4 # # $/\$ #
172	171	rgen 2547	. . 3 # # $/\$ #
173		elrabi 2913	. . . . . . . . . 10 #
174		efcl 11807	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 8035	. . . . . . . . 9 #
177	175, 176	subcld 8330	. . . . . . . 8 #
178		breq1 4032	. . . . . . . . . 10 # #
179	178	elrab 2916	. . . . . . . . 9 # $/\$ #
180	179	simprbi 275	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8809	. . . . . . 7 #
182	25, 181	fmpti 5710	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8666	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 8012	. . . . 5
187	183, 185, 186	ellimc3ap 14815	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1373	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 944	. 2 # lim
190	2	cntoptopon 14700	. . . . 5 TopOn
191	190	toponrestid 14189	. . . 4 ↾_t
192	173	subid1d 8319	. . . . . . 7 #
193	192	oveq2d 5934	. . . . . 6 #
194		ef0 11815	. . . . . . . 8
195	194	oveq2i 5929	. . . . . . 7
196	195	oveq1i 5928	. . . . . 6
197	193, 196	eqtr2di 2243	. . . . 5 #
198	197	mpteq2ia 4115	. . . 4 # #
199		ssidd 3200	. . . 4
200		eff 11806	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 14836	. . 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 2164

wral 2472

wrex 2473

crab 2476

wss 3153

cpr 3619 class class class wbr 4029

cmpt 4090

ccom 4663

wf 5250

cfv 5254 (class class class)co 5918 infcinf 7042

cc 7870

cr 7871

cc0 7872

c1 7873

caddc 7875

cmul 7877

clt 8054

cle 8055

cmin 8190 # cap 8600

cdiv 8691

cn 8982

c2 9033

c3 9034

c4 9035

cn0 9240

cuz 9592

crp 9719

cexp 10609

cfa 10796

cabs 11141

csu 11496

ce 11785

cmopn 14037

ctop 14165

cnt 14261 lim

climc 14808

cdv 14809

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 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992

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 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-isom 5263 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-irdg 6423 df-frec 6444 df-1o 6469 df-oadd 6473 df-er 6587 df-map 6704 df-pm 6705 df-en 6795 df-dom 6796 df-fin 6797 df-sup 7043 df-inf 7044 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-n0 9241 df-z 9318 df-uz 9593 df-q 9685 df-rp 9720 df-xneg 9838 df-xadd 9839 df-ico 9960 df-fz 10075 df-fzo 10209 df-seqfrec 10519 df-exp 10610 df-fac 10797 df-ihash 10847 df-shft 10959 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-clim 11422 df-sumdc 11497 df-ef 11791 df-rest 12852 df-topgen 12871 df-psmet 14039 df-xmet 14040 df-met 14041 df-bl 14042 df-mopn 14043 df-top 14166 df-topon 14179 df-bases 14211 df-ntr 14264 df-limced 14810 df-dvap 14811

This theorem is referenced by: dvef 14873

W3C validator