dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 12855

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11396, 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 7758	. . 3
2		eqid 2139	. . . . 5
3	2	cntoptop 12702	. . . 4
4		unicntopcntop 12705	. . . . 5
5	4	ntrtop 12297	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2215	. 2
8		ax-1cn 7713	. . 3
9		1rp 9445	. . . . . 6
10		rpmincl 11009	. . . . . 6 $/\$ inf
11	9, 10	mpan2 421	. . . . 5 inf
12		breq1 3932	. . . . . . . 8 # #
13	12	elrab 2840	. . . . . . 7 # $/\$ #
14		simprl 520	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8062	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5425	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 3939	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 10953	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9448	. . . . . . . . . . . 12
20	19	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 7781	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11006	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1216	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 187	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2139	. . . . . . . . . . . . 13 # #
26		fveq2 5421	. . . . . . . . . . . . . . 15
27	26	oveq1d 5789	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5792	. . . . . . . . . . . . 13
30		simplr 519	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 133	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 11370	. . . . . . . . . . . . . . . 16
33		peano2cnm 8028	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 521	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8550	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5514	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5796	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 7782	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8073	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 10953	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 524	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 10953	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 518	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9483	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 10823	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 479	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 7961	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 409	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 518	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 519	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8550	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 7782	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8073	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 10953	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 7796	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10450	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 8794	. . . . . . . . . . . . . . . . . 18
61		4nn 8883	. . . . . . . . . . . . . . . . . 18
62		nndivre 8756	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 422	. . . . . . . . . . . . . . . . 17
64		remulcl 7748	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 409	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8073	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8552	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8590	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8546	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2172	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8104	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 7745	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 410	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 8994	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2139	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 11394	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 409	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 8779	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 8993	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9223	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 8992	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 7759	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 11371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	syl6req 2189	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addid2d 7912	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2173	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 11399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	syl6eqr 2190	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 11397	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	syl6eq 2188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2172	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5790	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 11397	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8129	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2172	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2180	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5425	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 10966	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2174	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2139	. . . . . . . . . . . . . . . . . . 19
116		eqid 2139	. . . . . . . . . . . . . . . . . . 19
117		2nn 8881	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 7781	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 109	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 7881	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 11396	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 3952	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 8780	. . . . . . . . . . . . . . . . . . 19
125		fac2 10477	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5784	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 8874	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2161	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5786	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5785	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 3970	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10451	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 7765	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 8892	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 8798	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulid1i 7768	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 3955	. . . . . . . . . . . . . . . . . . . . 21
139		4re 8797	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 8817	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 270	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8634	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1315	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 145	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 7866	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 8698	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 7794	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10422	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulid1d 7783	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 3954	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 7886	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10421	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 3954	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 10871	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 479	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 146	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9481	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9528	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 166	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 499	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 520	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 7887	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 3950	. . . . . . . . . 10 $/\$ $/\$ # $/\$ $/\$ #
165	164	ex 114	. . . . . . . . 9 $/\$ $/\$ # $/\$ #
166	24, 165	sylbid 149	. . . . . . . 8 $/\$ $/\$ # inf #
167	166	adantld 276	. . . . . . 7 $/\$ $/\$ # # $/\$ inf #
168	13, 167	sylan2b 285	. . . . . 6 $/\$ # # $/\$ inf #
169	168	ralrimiva 2505	. . . . 5 # # $/\$ inf #
170		brimralrspcev 3987	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 408	. . . 4 # # $/\$ #
172	171	rgen 2485	. . 3 # # $/\$ #
173		elrabi 2837	. . . . . . . . . 10 #
174		efcl 11370	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 7782	. . . . . . . . 9 #
177	175, 176	subcld 8073	. . . . . . . 8 #
178		breq1 3932	. . . . . . . . . 10 # #
179	178	elrab 2840	. . . . . . . . 9 # $/\$ #
180	179	simprbi 273	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8550	. . . . . . 7 #
182	25, 181	fmpti 5572	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8409	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 7759	. . . . 5
187	183, 185, 186	ellimc3ap 12799	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1340	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 926	. 2 # lim
190	2	cntoptopon 12701	. . . . 5 TopOn
191	190	toponrestid 12188	. . . 4 ↾_t
192	173	subid1d 8062	. . . . . . 7 #
193	192	oveq2d 5790	. . . . . 6 #
194		ef0 11378	. . . . . . . 8
195	194	oveq2i 5785	. . . . . . 7
196	195	oveq1i 5784	. . . . . 6
197	193, 196	syl6req 2189	. . . . 5 #
198	197	mpteq2ia 4014	. . . 4 # #
199		ssidd 3118	. . . 4
200		eff 11369	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 12820	. . 3 $/\$ # lim
203	202	mptru 1340	. 2 $/\$ # lim
204	7, 189, 203	mpbir2an 926	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1331

wtru 1332

wcel 1480

wral 2416

wrex 2417

crab 2420

wss 3071

cpr 3528 class class class wbr 3929

cmpt 3989

ccom 4543

wf 5119

cfv 5123 (class class class)co 5774 infcinf 6870

cc 7618

cr 7619

cc0 7620

c1 7621

caddc 7623

cmul 7625

clt 7800

cle 7801

cmin 7933 # cap 8343

cdiv 8432

cn 8720

c2 8771

c3 8772

c4 8773

cn0 8977

cuz 9326

crp 9441

cexp 10292

cfa 10471

cabs 10769

csu 11122

ce 11348

cmopn 12154

ctop 12164

cnt 12262 lim

climc 12792

cdv 12793

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-mulrcl 7719 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-mulass 7723 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-1rid 7727 ax-0id 7728 ax-rnegex 7729 ax-precex 7730 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735 ax-pre-ltadd 7736 ax-pre-mulgt0 7737 ax-pre-mulext 7738 ax-arch 7739 ax-caucvg 7740

This theorem depends on definitions: df-bi 116 df-stab 816 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-isom 5132 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-frec 6288 df-1o 6313 df-oadd 6317 df-er 6429 df-map 6544 df-pm 6545 df-en 6635 df-dom 6636 df-fin 6637 df-sup 6871 df-inf 6872 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-reap 8337 df-ap 8344 df-div 8433 df-inn 8721 df-2 8779 df-3 8780 df-4 8781 df-n0 8978 df-z 9055 df-uz 9327 df-q 9412 df-rp 9442 df-xneg 9559 df-xadd 9560 df-ico 9677 df-fz 9791 df-fzo 9920 df-seqfrec 10219 df-exp 10293 df-fac 10472 df-ihash 10522 df-shft 10587 df-cj 10614 df-re 10615 df-im 10616 df-rsqrt 10770 df-abs 10771 df-clim 11048 df-sumdc 11123 df-ef 11354 df-rest 12122 df-topgen 12141 df-psmet 12156 df-xmet 12157 df-met 12158 df-bl 12159 df-mopn 12160 df-top 12165 df-topon 12178 df-bases 12210 df-ntr 12265 df-limced 12794 df-dvap 12795

This theorem is referenced by: dvef 12856

W3C validator