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 Visualization version Unicode version

Theorem lhe4.4ex1a 36672

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

. Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22989 as simply the "Fundamental Theorem of Calculus", then ftc1 22987 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 9655	. . . 4
2		2re 10676	. . . . 5
3	2	a1i 11	. . . 4
4		1le2 10820	. . . . 5
5	4	a1i 11	. . . 4
6		reelprrecn 9628	. . . . . . 7
7	6	a1i 11	. . . . . 6
8		recn 9626	. . . . . . . . . 10
9		3nn0 10884	. . . . . . . . . . 11
10		expcl 12287	. . . . . . . . . . 11 $/\$
11	9, 10	mpan2 676	. . . . . . . . . 10
12	8, 11	syl 17	. . . . . . . . 9
13		3cn 10681	. . . . . . . . . 10
14		3ne0 10701	. . . . . . . . . 10
15		divcl 10273	. . . . . . . . . 10 $/\$ $/\$
16	13, 14, 15	mp3an23 1355	. . . . . . . . 9
17	12, 16	syl 17	. . . . . . . 8
18		mulcl 9620	. . . . . . . . 9 $/\$
19	13, 8, 18	sylancr 668	. . . . . . . 8
20	17, 19	subcld 9983	. . . . . . 7
21	20	adantl 468	. . . . . 6 $/\$
22		ovex 6316	. . . . . . 7
23	22	a1i 11	. . . . . 6 $/\$
24	17	adantl 468	. . . . . . 7 $/\$
25		ovex 6316	. . . . . . . 8
26	25	a1i 11	. . . . . . 7 $/\$
27		divrec2 10284	. . . . . . . . . . . . 13 $/\$ $/\$
28	13, 14, 27	mp3an23 1355	. . . . . . . . . . . 12
29	12, 28	syl 17	. . . . . . . . . . 11
30	29	mpteq2ia 4484	. . . . . . . . . 10
31	30	oveq2i 6299	. . . . . . . . 9
32	12	adantl 468	. . . . . . . . . . 11 $/\$
33		ovex 6316	. . . . . . . . . . . 12
34	33	a1i 11	. . . . . . . . . . 11 $/\$
35		eqid 2450	. . . . . . . . . . . . . . 15
36	35, 11	fmpti 6043	. . . . . . . . . . . . . 14
37		ssid 3450	. . . . . . . . . . . . . 14
38		ax-resscn 9593	. . . . . . . . . . . . . . 15
39		3nn 10765	. . . . . . . . . . . . . . . . . 18
40		dvexp 22900	. . . . . . . . . . . . . . . . . 18
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17
42		3m1e2 10723	. . . . . . . . . . . . . . . . . . . 20
43	42	oveq2i 6299	. . . . . . . . . . . . . . . . . . 19
44	43	oveq2i 6299	. . . . . . . . . . . . . . . . . 18
45	44	mpteq2i 4485	. . . . . . . . . . . . . . . . 17
46	41, 45	eqtri 2472	. . . . . . . . . . . . . . . 16
47	33, 46	dmmpti 5705	. . . . . . . . . . . . . . 15
48	38, 47	sseqtr4i 3464	. . . . . . . . . . . . . 14
49		dvres3 22861	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
50	6, 36, 37, 48, 49	mp4an 678	. . . . . . . . . . . . 13
51		resmpt 5153	. . . . . . . . . . . . . . 15
52	38, 51	ax-mp 5	. . . . . . . . . . . . . 14
53	52	oveq2i 6299	. . . . . . . . . . . . 13
54	46	reseq1i 5100	. . . . . . . . . . . . . 14
55		resmpt 5153	. . . . . . . . . . . . . . 15
56	38, 55	ax-mp 5	. . . . . . . . . . . . . 14
57	54, 56	eqtri 2472	. . . . . . . . . . . . 13
58	50, 53, 57	3eqtr3i 2480	. . . . . . . . . . . 12
59	58	a1i 11	. . . . . . . . . . 11
60		ax-1cn 9594	. . . . . . . . . . . . 13
61	60, 13, 14	divcli 10346	. . . . . . . . . . . 12
62	61	a1i 11	. . . . . . . . . . 11
63	7, 32, 34, 59, 62	dvmptcmul 22911	. . . . . . . . . 10
64	63	trud 1452	. . . . . . . . 9
65		sqcl 12334	. . . . . . . . . . . . 13
66		mulcl 9620	. . . . . . . . . . . . 13 $/\$
67	13, 65, 66	sylancr 668	. . . . . . . . . . . 12
68		divrec2 10284	. . . . . . . . . . . . 13 $/\$ $/\$
69	13, 14, 68	mp3an23 1355	. . . . . . . . . . . 12
70	8, 67, 69	3syl 18	. . . . . . . . . . 11
71		divcan3 10291	. . . . . . . . . . . . 13 $/\$ $/\$
72	13, 14, 71	mp3an23 1355	. . . . . . . . . . . 12
73	8, 65, 72	3syl 18	. . . . . . . . . . 11
74	70, 73	eqtr3d 2486	. . . . . . . . . 10
75	74	mpteq2ia 4484	. . . . . . . . 9
76	31, 64, 75	3eqtri 2476	. . . . . . . 8
77	76	a1i 11	. . . . . . 7
78	19	adantl 468	. . . . . . 7 $/\$
79		3ex 10682	. . . . . . . 8
80	79	a1i 11	. . . . . . 7 $/\$
81	8	adantl 468	. . . . . . . . 9 $/\$
82		1red 9655	. . . . . . . . 9 $/\$
83	7	dvmptid 22904	. . . . . . . . 9
84	13	a1i 11	. . . . . . . . 9
85	7, 81, 82, 83, 84	dvmptcmul 22911	. . . . . . . 8
86		3t1e3 10757	. . . . . . . . 9
87	86	mpteq2i 4485	. . . . . . . 8
88	85, 87	syl6eq 2500	. . . . . . 7
89	7, 24, 26, 77, 78, 80, 88	dvmptsub 22914	. . . . . 6
90		1re 9639	. . . . . . . 8
91		iccssre 11713	. . . . . . . 8 $/\$
92	90, 2, 91	mp2an 677	. . . . . . 7
93	92	a1i 11	. . . . . 6
94		eqid 2450	. . . . . . 7 ℂ_fld ℂ_fld
95	94	tgioo2 21814	. . . . . 6 ℂ_fld ↾_t
96		iccntr 21832	. . . . . . . 8 $/\$
97	90, 2, 96	mp2an 677	. . . . . . 7
98	97	a1i 11	. . . . . 6
99	7, 21, 23, 89, 93, 95, 94, 98	dvmptres2 22909	. . . . 5
100		ioossicc 11717	. . . . . . 7
101		resmpt 5153	. . . . . . 7
102	100, 101	ax-mp 5	. . . . . 6
103	92, 38	sstri 3440	. . . . . . . . 9
104		resmpt 5153	. . . . . . . . 9
105	103, 104	ax-mp 5	. . . . . . . 8
106		eqid 2450	. . . . . . . . . . . 12
107		subcl 9871	. . . . . . . . . . . . . 14 $/\$
108	13, 107	mpan2 676	. . . . . . . . . . . . 13
109	65, 108	syl 17	. . . . . . . . . . . 12
110	106, 109	fmpti 6043	. . . . . . . . . . 11
111	37, 110, 37	3pm3.2i 1185	. . . . . . . . . 10 $/\$ $/\$
112		ovex 6316	. . . . . . . . . . 11
113		cnelprrecn 9629	. . . . . . . . . . . . . 14
114	113	a1i 11	. . . . . . . . . . . . 13
115	65	adantl 468	. . . . . . . . . . . . 13 $/\$
116		ovex 6316	. . . . . . . . . . . . . 14
117	116	a1i 11	. . . . . . . . . . . . 13 $/\$
118		2nn 10764	. . . . . . . . . . . . . . 15
119		dvexp 22900	. . . . . . . . . . . . . . 15
120	118, 119	ax-mp 5	. . . . . . . . . . . . . 14
121	120	a1i 11	. . . . . . . . . . . . 13
122	13	a1i 11	. . . . . . . . . . . . 13 $/\$
123		c0ex 9634	. . . . . . . . . . . . . 14
124	123	a1i 11	. . . . . . . . . . . . 13 $/\$
125	114, 84	dvmptc 22905	. . . . . . . . . . . . 13
126	114, 115, 117, 121, 122, 124, 125	dvmptsub 22914	. . . . . . . . . . . 12
127	126	trud 1452	. . . . . . . . . . 11
128	112, 127	dmmpti 5705	. . . . . . . . . 10
129		dvcn 22868	. . . . . . . . . 10 $/\$ $/\$ $/\$
130	111, 128, 129	mp2an 677	. . . . . . . . 9
131		rescncf 21922	. . . . . . . . 9
132	103, 130, 131	mp2 9	. . . . . . . 8
133	105, 132	eqeltrri 2525	. . . . . . 7
134		rescncf 21922	. . . . . . 7
135	100, 133, 134	mp2 9	. . . . . 6
136	102, 135	eqeltrri 2525	. . . . 5
137	99, 136	syl6eqel 2536	. . . 4
138	100	a1i 11	. . . . . 6
139		ioombl 22511	. . . . . . 7
140	139	a1i 11	. . . . . 6
141	22	a1i 11	. . . . . 6 $/\$
142		cniccibl 22791	. . . . . . . 8 $/\$ $/\$
143	90, 2, 133, 142	mp3an 1363	. . . . . . 7
144	143	a1i 11	. . . . . 6
145	138, 140, 141, 144	iblss 22755	. . . . 5
146	99, 145	eqeltrd 2528	. . . 4
147		resmpt 5153	. . . . . . 7
148	92, 147	ax-mp 5	. . . . . 6
149		eqid 2450	. . . . . . . . . 10
150	149, 20	fmpti 6043	. . . . . . . . 9
151		ssid 3450	. . . . . . . . 9
152	38, 150, 151	3pm3.2i 1185	. . . . . . . 8 $/\$ $/\$
153	89	trud 1452	. . . . . . . . 9
154	22, 153	dmmpti 5705	. . . . . . . 8
155		dvcn 22868	. . . . . . . 8 $/\$ $/\$ $/\$
156	152, 154, 155	mp2an 677	. . . . . . 7
157		rescncf 21922	. . . . . . 7
158	92, 156, 157	mp2 9	. . . . . 6
159	148, 158	eqeltrri 2525	. . . . 5
160	159	a1i 11	. . . 4
161	1, 3, 5, 137, 146, 160	ftc2 22989	. . 3
162	161	trud 1452	. 2
163		itgeq2 22728	. . 3
164		oveq1 6295	. . . . 5
165	164	oveq1d 6303	. . . 4
166	99	trud 1452	. . . 4
167		ovex 6316	. . . 4
168	165, 166, 167	fvmpt 5946	. . 3
169	163, 168	mprg 2750	. 2
170	2	leidi 10145	. . . . . . . . 9
171	90, 2	elicc2i 11697	. . . . . . . . 9 $/\$ $/\$
172	2, 4, 170, 171	mpbir3an 1189	. . . . . . . 8
173		oveq1 6295	. . . . . . . . . . . 12
174	173	oveq1d 6303	. . . . . . . . . . 11
175		oveq2 6296	. . . . . . . . . . 11
176	174, 175	oveq12d 6306	. . . . . . . . . 10
177		cu2 12370	. . . . . . . . . . . . 13
178	177	oveq1i 6298	. . . . . . . . . . . 12
179		3t2e6 10758	. . . . . . . . . . . 12
180	178, 179	oveq12i 6300	. . . . . . . . . . 11
181		2cn 10677	. . . . . . . . . . . . . . 15
182		6cn 10688	. . . . . . . . . . . . . . 15
183	181, 182, 13, 14	divdiri 10361	. . . . . . . . . . . . . 14
184		6p2e8 10748	. . . . . . . . . . . . . . . 16
185	182, 181, 184	addcomli 9822	. . . . . . . . . . . . . . 15
186	185	oveq1i 6298	. . . . . . . . . . . . . 14
187	182, 13, 181, 14	divmuli 10358	. . . . . . . . . . . . . . . 16
188	179, 187	mpbir 213	. . . . . . . . . . . . . . 15
189	188	oveq2i 6299	. . . . . . . . . . . . . 14
190	183, 186, 189	3eqtr3i 2480	. . . . . . . . . . . . 13
191	190	oveq1i 6298	. . . . . . . . . . . 12
192	181, 13, 14	divcli 10346	. . . . . . . . . . . . 13
193		subsub3 9903	. . . . . . . . . . . . 13 $/\$ $/\$
194	192, 182, 181, 193	mp3an 1363	. . . . . . . . . . . 12
195	191, 194	eqtr4i 2475	. . . . . . . . . . 11
196		4cn 10684	. . . . . . . . . . . . 13
197		4p2e6 10741	. . . . . . . . . . . . . 14
198	196, 181, 197	addcomli 9822	. . . . . . . . . . . . 13
199	182, 181, 196, 198	subaddrii 9961	. . . . . . . . . . . 12
200	199	oveq2i 6299	. . . . . . . . . . 11
201	180, 195, 200	3eqtri 2476	. . . . . . . . . 10
202	176, 201	syl6eq 2500	. . . . . . . . 9
203		eqid 2450	. . . . . . . . 9
204		ovex 6316	. . . . . . . . 9
205	202, 203, 204	fvmpt 5946	. . . . . . . 8
206	172, 205	ax-mp 5	. . . . . . 7
207	90	leidi 10145	. . . . . . . . 9
208	90, 2	elicc2i 11697	. . . . . . . . 9 $/\$ $/\$
209	90, 207, 4, 208	mpbir3an 1189	. . . . . . . 8
210		oveq1 6295	. . . . . . . . . . . 12
211	210	oveq1d 6303	. . . . . . . . . . 11
212		oveq2 6296	. . . . . . . . . . 11
213	211, 212	oveq12d 6306	. . . . . . . . . 10
214		3z 10967	. . . . . . . . . . . . 13
215		1exp 12298	. . . . . . . . . . . . 13
216	214, 215	ax-mp 5	. . . . . . . . . . . 12
217	216	oveq1i 6298	. . . . . . . . . . 11
218	217, 86	oveq12i 6300	. . . . . . . . . 10
219	213, 218	syl6eq 2500	. . . . . . . . 9
220		ovex 6316	. . . . . . . . 9
221	219, 203, 220	fvmpt 5946	. . . . . . . 8
222	209, 221	ax-mp 5	. . . . . . 7
223	206, 222	oveq12i 6300	. . . . . 6
224		sub4 9916	. . . . . . 7 $/\$ $/\$ $/\$
225	192, 196, 61, 13, 224	mp4an 678	. . . . . 6
226	13, 14	pm3.2i 457	. . . . . . . . 9 $/\$
227		divsubdir 10300	. . . . . . . . 9 $/\$ $/\$ $/\$
228	181, 60, 226, 227	mp3an 1363	. . . . . . . 8
229		2m1e1 10721	. . . . . . . . 9
230	229	oveq1i 6298	. . . . . . . 8
231	228, 230	eqtr3i 2474	. . . . . . 7
232		3p1e4 10732	. . . . . . . 8
233	196, 13, 60, 232	subaddrii 9961	. . . . . . 7
234	231, 233	oveq12i 6300	. . . . . 6
235	223, 225, 234	3eqtri 2476	. . . . 5
236	13, 14	dividi 10337	. . . . . 6
237	236	oveq2i 6299	. . . . 5
238	235, 237	eqtr4i 2475	. . . 4
239		divsubdir 10300	. . . . 5 $/\$ $/\$ $/\$
240	60, 13, 226, 239	mp3an 1363	. . . 4
241	238, 240	eqtr4i 2475	. . 3
242		divneg 10299	. . . . 5 $/\$ $/\$
243	181, 13, 14, 242	mp3an 1363	. . . 4
244	13, 60	negsubdi2i 9958	. . . . . 6
245	42	negeqi 9865	. . . . . 6
246	244, 245	eqtr3i 2474	. . . . 5
247	246	oveq1i 6298	. . . 4
248	243, 247	eqtr4i 2475	. . 3
249	241, 248	eqtr4i 2475	. 2
250	162, 169, 249	3eqtr3i 2480	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 371 $/\$ w3a 984

wceq 1443

wtru 1444

wcel 1886

wne 2621

cvv 3044

wss 3403

cpr 3969 class class class wbr 4401

cmpt 4460

cdm 4833

crn 4834

cres 4835

wf 5577

cfv 5581 (class class class)co 6288

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

cmul 9541

cle 9673

cmin 9857

cneg 9858

cdiv 10266

cn 10606

c2 10656

c3 10657

c4 10658

c6 10660

c8 10662

cn0 10866

cz 10934

cioo 11632

cicc 11635

cexp 12269

ctopn 15313

ctg 15329 ℂ_fldccnfld 18963

cnt 20025

ccncf 21901

cvol 22408

cibl 22568

citg 22569

cdv 22811

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cc 8862 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614 ax-addf 9615 ax-mulf 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-iin 4280 df-disj 4373 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-ofr 6529 df-om 6690 df-1st 6790 df-2nd 6791 df-supp 6912 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-omul 7184 df-er 7360 df-map 7471 df-pm 7472 df-ixp 7520 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-fsupp 7881 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-acn 8373 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-5 10668 df-6 10669 df-7 10670 df-8 10671 df-9 10672 df-10 10673 df-n0 10867 df-z 10935 df-dec 11049 df-uz 11157 df-q 11262 df-rp 11300 df-xneg 11406 df-xadd 11407 df-xmul 11408 df-ioo 11636 df-ioc 11637 df-ico 11638 df-icc 11639 df-fz 11782 df-fzo 11913 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-limsup 13519 df-clim 13545 df-rlim 13546 df-sum 13746 df-struct 15116 df-ndx 15117 df-slot 15118 df-base 15119 df-sets 15120 df-ress 15121 df-plusg 15196 df-mulr 15197 df-starv 15198 df-sca 15199 df-vsca 15200 df-ip 15201 df-tset 15202 df-ple 15203 df-ds 15205 df-unif 15206 df-hom 15207 df-cco 15208 df-rest 15314 df-topn 15315 df-0g 15333 df-gsum 15334 df-topgen 15335 df-pt 15336 df-prds 15339 df-xrs 15393 df-qtop 15399 df-imas 15400 df-xps 15403 df-mre 15485 df-mrc 15486 df-acs 15488 df-mgm 16481 df-sgrp 16520 df-mnd 16530 df-submnd 16576 df-mulg 16669 df-cntz 16964 df-cmn 17425 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-fbas 18960 df-fg 18961 df-cnfld 18964 df-top 19914 df-bases 19915 df-topon 19916 df-topsp 19917 df-cld 20027 df-ntr 20028 df-cls 20029 df-nei 20107 df-lp 20145 df-perf 20146 df-cn 20236 df-cnp 20237 df-haus 20324 df-cmp 20395 df-tx 20570 df-hmeo 20763 df-fil 20854 df-fm 20946 df-flim 20947 df-flf 20948 df-xms 21328 df-ms 21329 df-tms 21330 df-cncf 21903 df-ovol 22409 df-vol 22411 df-mbf 22570 df-itg1 22571 df-itg2 22572 df-ibl 22573 df-itg 22574 df-0p 22621 df-limc 22814 df-dv 22815

This theorem is referenced by: (None)

W3C validator