lhe4.4ex1a - Mathbox for Steve Rodriguez

	Mathbox for Steve Rodriguez	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lhe4.4ex1a		Structured version Unicode version

Theorem lhe4.4ex1a 31438

Description: Example of the Fundamental Theorem of Calculus, part two (ftc2 22571):

. Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22571 as simply the "Fundamental Theorem of Calculus", then ftc1 22569 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015.) (Revised by Steve Rodriguez, 31-Oct-2015.)

**Assertion**
Ref	Expression
lhe4.4ex1a

Proof of Theorem lhe4.4ex1a Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 9628	. . . 4
2		2re 10626	. . . . 5
3	2	a1i 11	. . . 4
4		1le2 10770	. . . . 5
5	4	a1i 11	. . . 4
6		reelprrecn 9601	. . . . . . 7
7	6	a1i 11	. . . . . 6
8		recn 9599	. . . . . . . . . 10
9		3nn0 10834	. . . . . . . . . . 11
10		expcl 12187	. . . . . . . . . . 11 $/\$
11	9, 10	mpan2 671	. . . . . . . . . 10
12	8, 11	syl 16	. . . . . . . . 9
13		3cn 10631	. . . . . . . . . 10
14		3ne0 10651	. . . . . . . . . 10
15		divcl 10234	. . . . . . . . . 10 $/\$ $/\$
16	13, 14, 15	mp3an23 1316	. . . . . . . . 9
17	12, 16	syl 16	. . . . . . . 8
18		mulcl 9593	. . . . . . . . 9 $/\$
19	13, 8, 18	sylancr 663	. . . . . . . 8
20	17, 19	subcld 9950	. . . . . . 7
21	20	adantl 466	. . . . . 6 $/\$
22		ovex 6324	. . . . . . 7
23	22	a1i 11	. . . . . 6 $/\$
24	17	adantl 466	. . . . . . 7 $/\$
25		ovex 6324	. . . . . . . 8
26	25	a1i 11	. . . . . . 7 $/\$
27		divrec2 10245	. . . . . . . . . . . . 13 $/\$ $/\$
28	13, 14, 27	mp3an23 1316	. . . . . . . . . . . 12
29	12, 28	syl 16	. . . . . . . . . . 11
30	29	mpteq2ia 4539	. . . . . . . . . 10
31	30	oveq2i 6307	. . . . . . . . 9
32	12	adantl 466	. . . . . . . . . . 11 $/\$
33		ovex 6324	. . . . . . . . . . . 12
34	33	a1i 11	. . . . . . . . . . 11 $/\$
35		eqid 2457	. . . . . . . . . . . . . . 15
36	35, 11	fmpti 6055	. . . . . . . . . . . . . 14
37		ssid 3518	. . . . . . . . . . . . . 14
38		ax-resscn 9566	. . . . . . . . . . . . . . 15
39		3nn 10715	. . . . . . . . . . . . . . . . . 18
40		dvexp 22482	. . . . . . . . . . . . . . . . . 18
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17
42		3m1e2 10673	. . . . . . . . . . . . . . . . . . . 20
43	42	oveq2i 6307	. . . . . . . . . . . . . . . . . . 19
44	43	oveq2i 6307	. . . . . . . . . . . . . . . . . 18
45	44	mpteq2i 4540	. . . . . . . . . . . . . . . . 17
46	41, 45	eqtri 2486	. . . . . . . . . . . . . . . 16
47	33, 46	dmmpti 5716	. . . . . . . . . . . . . . 15
48	38, 47	sseqtr4i 3532	. . . . . . . . . . . . . 14
49		dvres3 22443	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
50	6, 36, 37, 48, 49	mp4an 673	. . . . . . . . . . . . 13
51		resmpt 5333	. . . . . . . . . . . . . . 15
52	38, 51	ax-mp 5	. . . . . . . . . . . . . 14
53	52	oveq2i 6307	. . . . . . . . . . . . 13
54	46	reseq1i 5279	. . . . . . . . . . . . . 14
55		resmpt 5333	. . . . . . . . . . . . . . 15
56	38, 55	ax-mp 5	. . . . . . . . . . . . . 14
57	54, 56	eqtri 2486	. . . . . . . . . . . . 13
58	50, 53, 57	3eqtr3i 2494	. . . . . . . . . . . 12
59	58	a1i 11	. . . . . . . . . . 11
60		ax-1cn 9567	. . . . . . . . . . . . 13
61	60, 13, 14	divcli 10307	. . . . . . . . . . . 12
62	61	a1i 11	. . . . . . . . . . 11
63	7, 32, 34, 59, 62	dvmptcmul 22493	. . . . . . . . . 10
64	63	trud 1404	. . . . . . . . 9
65		sqcl 12233	. . . . . . . . . . . . 13
66		mulcl 9593	. . . . . . . . . . . . 13 $/\$
67	13, 65, 66	sylancr 663	. . . . . . . . . . . 12
68		divrec2 10245	. . . . . . . . . . . . 13 $/\$ $/\$
69	13, 14, 68	mp3an23 1316	. . . . . . . . . . . 12
70	8, 67, 69	3syl 20	. . . . . . . . . . 11
71		divcan3 10252	. . . . . . . . . . . . 13 $/\$ $/\$
72	13, 14, 71	mp3an23 1316	. . . . . . . . . . . 12
73	8, 65, 72	3syl 20	. . . . . . . . . . 11
74	70, 73	eqtr3d 2500	. . . . . . . . . 10
75	74	mpteq2ia 4539	. . . . . . . . 9
76	31, 64, 75	3eqtri 2490	. . . . . . . 8
77	76	a1i 11	. . . . . . 7
78	19	adantl 466	. . . . . . 7 $/\$
79		3ex 10632	. . . . . . . 8
80	79	a1i 11	. . . . . . 7 $/\$
81	8	adantl 466	. . . . . . . . 9 $/\$
82		1red 9628	. . . . . . . . 9 $/\$
83	7	dvmptid 22486	. . . . . . . . 9
84	13	a1i 11	. . . . . . . . 9
85	7, 81, 82, 83, 84	dvmptcmul 22493	. . . . . . . 8
86		3t1e3 10707	. . . . . . . . 9
87	86	mpteq2i 4540	. . . . . . . 8
88	85, 87	syl6eq 2514	. . . . . . 7
89	7, 24, 26, 77, 78, 80, 88	dvmptsub 22496	. . . . . 6
90		1re 9612	. . . . . . . 8
91		iccssre 11631	. . . . . . . 8 $/\$
92	90, 2, 91	mp2an 672	. . . . . . 7
93	92	a1i 11	. . . . . 6
94		eqid 2457	. . . . . . 7 ℂ_fld ℂ_fld
95	94	tgioo2 21434	. . . . . 6 ℂ_fld ↾_t
96		iccntr 21452	. . . . . . . 8 $/\$
97	90, 2, 96	mp2an 672	. . . . . . 7
98	97	a1i 11	. . . . . 6
99	7, 21, 23, 89, 93, 95, 94, 98	dvmptres2 22491	. . . . 5
100		ioossicc 11635	. . . . . . 7
101		resmpt 5333	. . . . . . 7
102	100, 101	ax-mp 5	. . . . . 6
103	92, 38	sstri 3508	. . . . . . . . 9
104		resmpt 5333	. . . . . . . . 9
105	103, 104	ax-mp 5	. . . . . . . 8
106		eqid 2457	. . . . . . . . . . . 12
107		subcl 9838	. . . . . . . . . . . . . 14 $/\$
108	13, 107	mpan2 671	. . . . . . . . . . . . 13
109	65, 108	syl 16	. . . . . . . . . . . 12
110	106, 109	fmpti 6055	. . . . . . . . . . 11
111	37, 110, 37	3pm3.2i 1174	. . . . . . . . . 10 $/\$ $/\$
112		ovex 6324	. . . . . . . . . . 11
113		cnelprrecn 9602	. . . . . . . . . . . . . 14
114	113	a1i 11	. . . . . . . . . . . . 13
115	65	adantl 466	. . . . . . . . . . . . 13 $/\$
116		ovex 6324	. . . . . . . . . . . . . 14
117	116	a1i 11	. . . . . . . . . . . . 13 $/\$
118		2nn 10714	. . . . . . . . . . . . . . 15
119		dvexp 22482	. . . . . . . . . . . . . . 15
120	118, 119	ax-mp 5	. . . . . . . . . . . . . 14
121	120	a1i 11	. . . . . . . . . . . . 13
122	13	a1i 11	. . . . . . . . . . . . 13 $/\$
123		c0ex 9607	. . . . . . . . . . . . . 14
124	123	a1i 11	. . . . . . . . . . . . 13 $/\$
125	114, 84	dvmptc 22487	. . . . . . . . . . . . 13
126	114, 115, 117, 121, 122, 124, 125	dvmptsub 22496	. . . . . . . . . . . 12
127	126	trud 1404	. . . . . . . . . . 11
128	112, 127	dmmpti 5716	. . . . . . . . . 10
129		dvcn 22450	. . . . . . . . . 10 $/\$ $/\$ $/\$
130	111, 128, 129	mp2an 672	. . . . . . . . 9
131		rescncf 21527	. . . . . . . . 9
132	103, 130, 131	mp2 9	. . . . . . . 8
133	105, 132	eqeltrri 2542	. . . . . . 7
134		rescncf 21527	. . . . . . 7
135	100, 133, 134	mp2 9	. . . . . 6
136	102, 135	eqeltrri 2542	. . . . 5
137	99, 136	syl6eqel 2553	. . . 4
138	100	a1i 11	. . . . . 6
139		ioombl 22101	. . . . . . 7
140	139	a1i 11	. . . . . 6
141	22	a1i 11	. . . . . 6 $/\$
142		cniccibl 22373	. . . . . . . 8 $/\$ $/\$
143	90, 2, 133, 142	mp3an 1324	. . . . . . 7
144	143	a1i 11	. . . . . 6
145	138, 140, 141, 144	iblss 22337	. . . . 5
146	99, 145	eqeltrd 2545	. . . 4
147		resmpt 5333	. . . . . . 7
148	92, 147	ax-mp 5	. . . . . 6
149		eqid 2457	. . . . . . . . . 10
150	149, 20	fmpti 6055	. . . . . . . . 9
151		ssid 3518	. . . . . . . . 9
152	38, 150, 151	3pm3.2i 1174	. . . . . . . 8 $/\$ $/\$
153	89	trud 1404	. . . . . . . . 9
154	22, 153	dmmpti 5716	. . . . . . . 8
155		dvcn 22450	. . . . . . . 8 $/\$ $/\$ $/\$
156	152, 154, 155	mp2an 672	. . . . . . 7
157		rescncf 21527	. . . . . . 7
158	92, 156, 157	mp2 9	. . . . . 6
159	148, 158	eqeltrri 2542	. . . . 5
160	159	a1i 11	. . . 4
161	1, 3, 5, 137, 146, 160	ftc2 22571	. . 3
162	161	trud 1404	. 2
163		itgeq2 22310	. . 3
164		oveq1 6303	. . . . 5
165	164	oveq1d 6311	. . . 4
166	99	trud 1404	. . . 4
167		ovex 6324	. . . 4
168	165, 166, 167	fvmpt 5956	. . 3
169	163, 168	mprg 2820	. 2
170	2	leidi 10108	. . . . . . . . 9
171	90, 2	elicc2i 11615	. . . . . . . . 9 $/\$ $/\$
172	2, 4, 170, 171	mpbir3an 1178	. . . . . . . 8
173		oveq1 6303	. . . . . . . . . . . 12
174	173	oveq1d 6311	. . . . . . . . . . 11
175		oveq2 6304	. . . . . . . . . . 11
176	174, 175	oveq12d 6314	. . . . . . . . . 10
177		cu2 12269	. . . . . . . . . . . . 13
178	177	oveq1i 6306	. . . . . . . . . . . 12
179		3t2e6 10708	. . . . . . . . . . . 12
180	178, 179	oveq12i 6308	. . . . . . . . . . 11
181		2cn 10627	. . . . . . . . . . . . . . 15
182		6cn 10638	. . . . . . . . . . . . . . 15
183	181, 182, 13, 14	divdiri 10322	. . . . . . . . . . . . . 14
184		6p2e8 10698	. . . . . . . . . . . . . . . 16
185	182, 181, 184	addcomli 9789	. . . . . . . . . . . . . . 15
186	185	oveq1i 6306	. . . . . . . . . . . . . 14
187	182, 13, 181, 14	divmuli 10319	. . . . . . . . . . . . . . . 16
188	179, 187	mpbir 209	. . . . . . . . . . . . . . 15
189	188	oveq2i 6307	. . . . . . . . . . . . . 14
190	183, 186, 189	3eqtr3i 2494	. . . . . . . . . . . . 13
191	190	oveq1i 6306	. . . . . . . . . . . 12
192	181, 13, 14	divcli 10307	. . . . . . . . . . . . 13
193		subsub3 9870	. . . . . . . . . . . . 13 $/\$ $/\$
194	192, 182, 181, 193	mp3an 1324	. . . . . . . . . . . 12
195	191, 194	eqtr4i 2489	. . . . . . . . . . 11
196		4cn 10634	. . . . . . . . . . . . 13
197		4p2e6 10691	. . . . . . . . . . . . . 14
198	196, 181, 197	addcomli 9789	. . . . . . . . . . . . 13
199	182, 181, 196, 198	subaddrii 9928	. . . . . . . . . . . 12
200	199	oveq2i 6307	. . . . . . . . . . 11
201	180, 195, 200	3eqtri 2490	. . . . . . . . . 10
202	176, 201	syl6eq 2514	. . . . . . . . 9
203		eqid 2457	. . . . . . . . 9
204		ovex 6324	. . . . . . . . 9
205	202, 203, 204	fvmpt 5956	. . . . . . . 8
206	172, 205	ax-mp 5	. . . . . . 7
207	90	leidi 10108	. . . . . . . . 9
208	90, 2	elicc2i 11615	. . . . . . . . 9 $/\$ $/\$
209	90, 207, 4, 208	mpbir3an 1178	. . . . . . . 8
210		oveq1 6303	. . . . . . . . . . . 12
211	210	oveq1d 6311	. . . . . . . . . . 11
212		oveq2 6304	. . . . . . . . . . 11
213	211, 212	oveq12d 6314	. . . . . . . . . 10
214		3z 10918	. . . . . . . . . . . . 13
215		1exp 12198	. . . . . . . . . . . . 13
216	214, 215	ax-mp 5	. . . . . . . . . . . 12
217	216	oveq1i 6306	. . . . . . . . . . 11
218	217, 86	oveq12i 6308	. . . . . . . . . 10
219	213, 218	syl6eq 2514	. . . . . . . . 9
220		ovex 6324	. . . . . . . . 9
221	219, 203, 220	fvmpt 5956	. . . . . . . 8
222	209, 221	ax-mp 5	. . . . . . 7
223	206, 222	oveq12i 6308	. . . . . 6
224		sub4 9883	. . . . . . 7 $/\$ $/\$ $/\$
225	192, 196, 61, 13, 224	mp4an 673	. . . . . 6
226	13, 14	pm3.2i 455	. . . . . . . . 9 $/\$
227		divsubdir 10261	. . . . . . . . 9 $/\$ $/\$ $/\$
228	181, 60, 226, 227	mp3an 1324	. . . . . . . 8
229		2m1e1 10671	. . . . . . . . 9
230	229	oveq1i 6306	. . . . . . . 8
231	228, 230	eqtr3i 2488	. . . . . . 7
232		3p1e4 10682	. . . . . . . 8
233	196, 13, 60, 232	subaddrii 9928	. . . . . . 7
234	231, 233	oveq12i 6308	. . . . . 6
235	223, 225, 234	3eqtri 2490	. . . . 5
236	13, 14	dividi 10298	. . . . . 6
237	236	oveq2i 6307	. . . . 5
238	235, 237	eqtr4i 2489	. . . 4
239		divsubdir 10261	. . . . 5 $/\$ $/\$ $/\$
240	60, 13, 226, 239	mp3an 1324	. . . 4
241	238, 240	eqtr4i 2489	. . 3
242		divneg 10260	. . . . 5 $/\$ $/\$
243	181, 13, 14, 242	mp3an 1324	. . . 4
244	13, 60	negsubdi2i 9925	. . . . . 6
245	42	negeqi 9832	. . . . . 6
246	244, 245	eqtr3i 2488	. . . . 5
247	246	oveq1i 6306	. . . 4
248	243, 247	eqtr4i 2489	. . 3
249	241, 248	eqtr4i 2489	. 2
250	162, 169, 249	3eqtr3i 2494	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369 $/\$ w3a 973

wceq 1395

wtru 1396

wcel 1819

wne 2652

cvv 3109

wss 3471

cpr 4034 class class class wbr 4456

cmpt 4515

cdm 5008

crn 5009

cres 5010

wf 5590

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

cle 9646

cmin 9824

cneg 9825

cdiv 10227

cn 10556

c2 10606

c3 10607

c4 10608

c6 10610

c8 10612

cn0 10816

cz 10885

cioo 11554

cicc 11557

cexp 12169

ctopn 14839

ctg 14855 ℂ_fldccnfld 18547

cnt 19645

ccncf 21506

cvol 22001

cibl 22152

citg 22153

cdv 22393

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cc 8832 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-ofr 6540 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-omul 7153 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-acn 8340 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-mod 12000 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-limsup 13306 df-clim 13323 df-rlim 13324 df-sum 13521 df-struct 14646 df-ndx 14647 df-slot 14648 df-base 14649 df-sets 14650 df-ress 14651 df-plusg 14725 df-mulr 14726 df-starv 14727 df-sca 14728 df-vsca 14729 df-ip 14730 df-tset 14731 df-ple 14732 df-ds 14734 df-unif 14735 df-hom 14736 df-cco 14737 df-rest 14840 df-topn 14841 df-0g 14859 df-gsum 14860 df-topgen 14861 df-pt 14862 df-prds 14865 df-xrs 14919 df-qtop 14924 df-imas 14925 df-xps 14927 df-mre 15003 df-mrc 15004 df-acs 15006 df-mgm 15999 df-sgrp 16038 df-mnd 16048 df-submnd 16094 df-mulg 16187 df-cntz 16482 df-cmn 16927 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-mopn 18542 df-fbas 18543 df-fg 18544 df-cnfld 18548 df-top 19526 df-bases 19528 df-topon 19529 df-topsp 19530 df-cld 19647 df-ntr 19648 df-cls 19649 df-nei 19726 df-lp 19764 df-perf 19765 df-cn 19855 df-cnp 19856 df-haus 19943 df-cmp 20014 df-tx 20189 df-hmeo 20382 df-fil 20473 df-fm 20565 df-flim 20566 df-flf 20567 df-xms 20949 df-ms 20950 df-tms 20951 df-cncf 21508 df-ovol 22002 df-vol 22003 df-mbf 22154 df-itg1 22155 df-itg2 22156 df-ibl 22157 df-itg 22158 df-0p 22203 df-limc 22396 df-dv 22397

This theorem is referenced by: (None)

W3C validator