dveflem - Intuitionistic Logic Explorer

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

Theorem dveflem 13854

Description: Derivative of the exponential function at 0. The key step in the proof is eftlub 11682, 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 7940	. . 3
2		eqid 2177	. . . . 5
3	2	cntoptop 13700	. . . 4
4		unicntopcntop 13703	. . . . 5
5	4	ntrtop 13295	. . . 4
6	3, 5	ax-mp 5	. . 3
7	1, 6	eleqtrri 2253	. 2
8		ax-1cn 7895	. . 3
9		1rp 9644	. . . . . 6
10		rpmincl 11230	. . . . . 6 $/\$ inf
11	9, 10	mpan2 425	. . . . 5 inf
12		breq1 4003	. . . . . . . 8 # #
13	12	elrab 2893	. . . . . . 7 # $/\$ #
14		simprl 529	. . . . . . . . . . . . 13 $/\$ $/\$ #
15	14	subid1d 8247	. . . . . . . . . . . 12 $/\$ $/\$ #
16	15	fveq2d 5515	. . . . . . . . . . 11 $/\$ $/\$ #
17	16	breq1d 4010	. . . . . . . . . 10 $/\$ $/\$ # inf inf
18	14	abscld 11174	. . . . . . . . . . 11 $/\$ $/\$ #
19		rpre 9647	. . . . . . . . . . . 12
20	19	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ #
21		1red 7963	. . . . . . . . . . 11 $/\$ $/\$ #
22		ltmininf 11227	. . . . . . . . . . 11 $/\$ $/\$ inf $/\$
23	18, 20, 21, 22	syl3anc 1238	. . . . . . . . . 10 $/\$ $/\$ # inf $/\$
24	17, 23	bitrd 188	. . . . . . . . 9 $/\$ $/\$ # inf $/\$
25		eqid 2177	. . . . . . . . . . . . 13 # #
26		fveq2 5511	. . . . . . . . . . . . . . 15
27	26	oveq1d 5884	. . . . . . . . . . . . . 14
28		id 19	. . . . . . . . . . . . . 14
29	27, 28	oveq12d 5887	. . . . . . . . . . . . 13
30		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$ $/\$ #
31	30, 13	sylibr 134	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$ #
32		efcl 11656	. . . . . . . . . . . . . . . 16
33		peano2cnm 8213	. . . . . . . . . . . . . . . 16
34	14, 32, 33	3syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
35		simprr 531	. . . . . . . . . . . . . . 15 $/\$ $/\$ # #
36	34, 14, 35	divclapd 8736	. . . . . . . . . . . . . 14 $/\$ $/\$ #
37	36	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
38	25, 29, 31, 37	fvmptd3 5605	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$ #
39	38	fvoveq1d 5891	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$ #
40		1cnd 7964	. . . . . . . . . . . . . 14 $/\$ $/\$ # $/\$ $/\$
41	37, 40	subcld 8258	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
42	41	abscld 11174	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
43		simplrl 535	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
44	43	abscld 11174	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
45		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$ # $/\$ $/\$
46	45	rpred 9683	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
47		abscl 11044	. . . . . . . . . . . . . . . . . 18
48	47	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
49	32	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
50		subcl 8146	. . . . . . . . . . . . . . . . . . . . 21 $/\$
51	49, 8, 50	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
52		simpll 527	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
53		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$ #
54	51, 52, 53	divclapd 8736	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
55		1cnd 7964	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
56	54, 55	subcld 8258	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
57	56	abscld 11174	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
58	48, 57	remulcld 7978	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
59	48	resqcld 10665	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
60		3re 8982	. . . . . . . . . . . . . . . . . 18
61		4nn 9071	. . . . . . . . . . . . . . . . . 18
62		nndivre 8944	. . . . . . . . . . . . . . . . . 18 $/\$
63	60, 61, 62	mp2an 426	. . . . . . . . . . . . . . . . 17
64		remulcl 7930	. . . . . . . . . . . . . . . . 17 $/\$
65	59, 63, 64	sylancl 413	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
66	51, 52	subcld 8258	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
67	66, 52, 53	divcanap2d 8738	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
68	51, 52, 52, 53	divsubdirapd 8776	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
69	52, 53	dividapd 8732	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
70	69	oveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
71	68, 70	eqtrd 2210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
72	71	oveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
73	49, 55, 52	subsub4d 8289	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
74		addcl 7927	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	8, 52, 74	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
76		2nn0 9182	. . . . . . . . . . . . . . . . . . . . . . . 24
77		eqid 2177	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	eftlcl 11680	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
79	52, 76, 78	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
80		df-2 8967	. . . . . . . . . . . . . . . . . . . . . . . 24
81		1nn0 9181	. . . . . . . . . . . . . . . . . . . . . . . 24
82		1e0p1 9414	. . . . . . . . . . . . . . . . . . . . . . . . 25
83		0nn0 9180	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		0cnd 7941	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
85	77	efval2 11657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
87		nn0uz 9551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
88	87	sumeq1i 11355	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
89	86, 88	eqtr2di 2227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
90	89	oveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
91	49	addid2d 8097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
92	90, 91	eqtr2d 2211	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
93		eft0val 11685	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
94	93	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
95	94	oveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
96	95, 82	eqtr4di 2228	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
97	77, 82, 83, 52, 84, 92, 96	efsep 11683	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
98		exp1 10512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	98	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ # $/\$
100	99	oveq1d 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ # $/\$
101		fac1 10693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
102	101	oveq2i 5880	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
103	100, 102	eqtrdi 2226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
104		div1 8649	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	104	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ # $/\$
106	103, 105	eqtrd 2210	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ # $/\$
107	106	oveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ # $/\$
108	77, 80, 81, 52, 55, 97, 107	efsep 11683	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ # $/\$
109	75, 79, 108	mvrladdd 8314	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ # $/\$
110	73, 109	eqtrd 2210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ # $/\$
111	67, 72, 110	3eqtr3d 2218	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
112	111	fveq2d 5515	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
113	52, 56	absmuld 11187	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
114	112, 113	eqtr3d 2212	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
115		eqid 2177	. . . . . . . . . . . . . . . . . . 19
116		eqid 2177	. . . . . . . . . . . . . . . . . . 19
117		2nn 9069	. . . . . . . . . . . . . . . . . . . 20
118	117	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
119		1red 7963	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
120		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ # $/\$
121	48, 119, 120	ltled 8066	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
122	77, 115, 116, 118, 52, 121	eftlub 11682	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
123	114, 122	eqbrtrrd 4024	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
124		df-3 8968	. . . . . . . . . . . . . . . . . . 19
125		fac2 10695	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 5879	. . . . . . . . . . . . . . . . . . . 20
127		2t2e4 9062	. . . . . . . . . . . . . . . . . . . 20
128	126, 127	eqtr2i 2199	. . . . . . . . . . . . . . . . . . 19
129	124, 128	oveq12i 5881	. . . . . . . . . . . . . . . . . 18
130	129	oveq2i 5880	. . . . . . . . . . . . . . . . 17
131	123, 130	breqtrrdi 4042	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
132	63	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
133	48	sqge0d 10666	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
134		1re 7947	. . . . . . . . . . . . . . . . . . . 20
135		3lt4 9080	. . . . . . . . . . . . . . . . . . . . . 22
136		4cn 8986	. . . . . . . . . . . . . . . . . . . . . . 23
137	136	mulid1i 7950	. . . . . . . . . . . . . . . . . . . . . 22
138	135, 137	breqtrri 4027	. . . . . . . . . . . . . . . . . . . . 21
139		4re 8985	. . . . . . . . . . . . . . . . . . . . . . 23
140		4pos 9005	. . . . . . . . . . . . . . . . . . . . . . 23
141	139, 140	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		ltdivmul 8822	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	60, 134, 141, 142	mp3an 1337	. . . . . . . . . . . . . . . . . . . . 21
144	138, 143	mpbir 146	. . . . . . . . . . . . . . . . . . . 20
145	63, 134, 144	ltleii 8050	. . . . . . . . . . . . . . . . . . 19
146	145	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
147	132, 119, 59, 133, 146	lemul2ad 8886	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
148	48	recnd 7976	. . . . . . . . . . . . . . . . . . 19 $/\$ # $/\$
149	148	sqcld 10637	. . . . . . . . . . . . . . . . . 18 $/\$ # $/\$
150	149	mulid1d 7965	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$
151	147, 150	breqtrd 4026	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
152	58, 65, 59, 131, 151	letrd 8071	. . . . . . . . . . . . . . 15 $/\$ # $/\$
153	148	sqvald 10636	. . . . . . . . . . . . . . 15 $/\$ # $/\$
154	152, 153	breqtrd 4026	. . . . . . . . . . . . . 14 $/\$ # $/\$
155		absgt0ap 11092	. . . . . . . . . . . . . . . . . 18 #
156	155	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ # $/\$ #
157	53, 156	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ # $/\$
158	48, 157	elrpd 9680	. . . . . . . . . . . . . . 15 $/\$ # $/\$
159	57, 48, 158	lemul2d 9728	. . . . . . . . . . . . . 14 $/\$ # $/\$
160	154, 159	mpbird 167	. . . . . . . . . . . . 13 $/\$ # $/\$
161	160	ad2ant2l 508	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
162		simprl 529	. . . . . . . . . . . 12 $/\$ $/\$ # $/\$ $/\$
163	42, 44, 46, 161, 162	lelttrd 8072	. . . . . . . . . . 11 $/\$ $/\$ # $/\$ $/\$
164	39, 163	eqbrtrd 4022	. . . . . . . . . 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 2550	. . . . 5 # # $/\$ inf #
170		brimralrspcev 4059	. . . . 5 inf $/\$ # # $/\$ inf # # # $/\$ #
171	11, 169, 170	syl2anc 411	. . . 4 # # $/\$ #
172	171	rgen 2530	. . 3 # # $/\$ #
173		elrabi 2890	. . . . . . . . . 10 #
174		efcl 11656	. . . . . . . . . 10
175	173, 174	syl 14	. . . . . . . . 9 #
176		1cnd 7964	. . . . . . . . 9 #
177	175, 176	subcld 8258	. . . . . . . 8 #
178		breq1 4003	. . . . . . . . . 10 # #
179	178	elrab 2893	. . . . . . . . 9 # $/\$ #
180	179	simprbi 275	. . . . . . . 8 # #
181	177, 173, 180	divclapd 8736	. . . . . . 7 #
182	25, 181	fmpti 5664	. . . . . 6 # #
183	182	a1i 9	. . . . 5 # #
184		apsscn 8594	. . . . . 6 #
185	184	a1i 9	. . . . 5 #
186		0cnd 7941	. . . . 5
187	183, 185, 186	ellimc3ap 13797	. . . 4 # lim $/\$ # # $/\$ #
188	187	mptru 1362	. . 3 # lim $/\$ # # $/\$ #
189	8, 172, 188	mpbir2an 942	. 2 # lim
190	2	cntoptopon 13699	. . . . 5 TopOn
191	190	toponrestid 13186	. . . 4 ↾_t
192	173	subid1d 8247	. . . . . . 7 #
193	192	oveq2d 5885	. . . . . 6 #
194		ef0 11664	. . . . . . . 8
195	194	oveq2i 5880	. . . . . . 7
196	195	oveq1i 5879	. . . . . 6
197	193, 196	eqtr2di 2227	. . . . 5 #
198	197	mpteq2ia 4086	. . . 4 # #
199		ssidd 3176	. . . 4
200		eff 11655	. . . . 5
201	200	a1i 9	. . . 4
202	191, 2, 198, 199, 201, 199	eldvap 13818	. . 3 $/\$ # lim
203	202	mptru 1362	. 2 $/\$ # lim
204	7, 189, 203	mpbir2an 942	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1353

wtru 1354

wcel 2148

wral 2455

wrex 2456

crab 2459

wss 3129

cpr 3592 class class class wbr 4000

cmpt 4061

ccom 4627

wf 5208

cfv 5212 (class class class)co 5869 infcinf 6976

cc 7800

cr 7801

cc0 7802

c1 7803

caddc 7805

cmul 7807

clt 7982

cle 7983

cmin 8118 # cap 8528

cdiv 8618

cn 8908

c2 8959

c3 8960

c4 8961

cn0 9165

cuz 9517

crp 9640

cexp 10505

cfa 10689

cabs 10990

csu 11345

ce 11634

cmopn 13152

ctop 13162

cnt 13260 lim

climc 13790

cdv 13791

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-isom 5221 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-irdg 6365 df-frec 6386 df-1o 6411 df-oadd 6415 df-er 6529 df-map 6644 df-pm 6645 df-en 6735 df-dom 6736 df-fin 6737 df-sup 6977 df-inf 6978 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-xneg 9759 df-xadd 9760 df-ico 9881 df-fz 9996 df-fzo 10129 df-seqfrec 10432 df-exp 10506 df-fac 10690 df-ihash 10740 df-shft 10808 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-clim 11271 df-sumdc 11346 df-ef 11640 df-rest 12638 df-topgen 12657 df-psmet 13154 df-xmet 13155 df-met 13156 df-bl 13157 df-mopn 13158 df-top 13163 df-topon 13176 df-bases 13208 df-ntr 13263 df-limced 13792 df-dvap 13793

This theorem is referenced by: dvef 13855

W3C validator