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 30834

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

. Section 4.4 example 1a of [LarsonHostetlerEdwards] p. 311. (The book teaches ftc2 22180 as simply the "Fundamental Theorem of Calculus", then ftc1 22178 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		1re 9591	. . . . 5
2	1	a1i 11	. . . 4
3		2re 10601	. . . . 5
4	3	a1i 11	. . . 4
5		1le2 10745	. . . . 5
6	5	a1i 11	. . . 4
7		reelprrecn 9580	. . . . . . 7
8	7	a1i 11	. . . . . 6
9		recn 9578	. . . . . . . . . 10
10		3nn0 10809	. . . . . . . . . . 11
11		expcl 12148	. . . . . . . . . . 11 $/\$
12	10, 11	mpan2 671	. . . . . . . . . 10
13	9, 12	syl 16	. . . . . . . . 9
14		3cn 10606	. . . . . . . . . 10
15		3ne0 10626	. . . . . . . . . 10
16		divcl 10209	. . . . . . . . . 10 $/\$ $/\$
17	14, 15, 16	mp3an23 1316	. . . . . . . . 9
18	13, 17	syl 16	. . . . . . . 8
19		mulcl 9572	. . . . . . . . 9 $/\$
20	14, 9, 19	sylancr 663	. . . . . . . 8
21	18, 20	subcld 9926	. . . . . . 7
22	21	adantl 466	. . . . . 6 $/\$
23		ovex 6307	. . . . . . 7
24	23	a1i 11	. . . . . 6 $/\$
25	18	adantl 466	. . . . . . 7 $/\$
26		ovex 6307	. . . . . . . 8
27	26	a1i 11	. . . . . . 7 $/\$
28		divrec2 10220	. . . . . . . . . . . . 13 $/\$ $/\$
29	14, 15, 28	mp3an23 1316	. . . . . . . . . . . 12
30	13, 29	syl 16	. . . . . . . . . . 11
31	30	mpteq2ia 4529	. . . . . . . . . 10
32	31	oveq2i 6293	. . . . . . . . 9
33	13	adantl 466	. . . . . . . . . . 11 $/\$
34		ovex 6307	. . . . . . . . . . . 12
35	34	a1i 11	. . . . . . . . . . 11 $/\$
36		eqid 2467	. . . . . . . . . . . . . . 15
37	36, 12	fmpti 6042	. . . . . . . . . . . . . 14
38		ssid 3523	. . . . . . . . . . . . . 14
39		ax-resscn 9545	. . . . . . . . . . . . . . 15
40		3nn 10690	. . . . . . . . . . . . . . . . . 18
41		dvexp 22091	. . . . . . . . . . . . . . . . . 18
42	40, 41	ax-mp 5	. . . . . . . . . . . . . . . . 17
43		3m1e2 10648	. . . . . . . . . . . . . . . . . . . 20
44	43	oveq2i 6293	. . . . . . . . . . . . . . . . . . 19
45	44	oveq2i 6293	. . . . . . . . . . . . . . . . . 18
46	45	mpteq2i 4530	. . . . . . . . . . . . . . . . 17
47	42, 46	eqtri 2496	. . . . . . . . . . . . . . . 16
48	34, 47	dmmpti 5708	. . . . . . . . . . . . . . 15
49	39, 48	sseqtr4i 3537	. . . . . . . . . . . . . 14
50		dvres3 22052	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
51	7, 37, 38, 49, 50	mp4an 673	. . . . . . . . . . . . 13
52		resmpt 5321	. . . . . . . . . . . . . . 15
53	39, 52	ax-mp 5	. . . . . . . . . . . . . 14
54	53	oveq2i 6293	. . . . . . . . . . . . 13
55	47	reseq1i 5267	. . . . . . . . . . . . . 14
56		resmpt 5321	. . . . . . . . . . . . . . 15
57	39, 56	ax-mp 5	. . . . . . . . . . . . . 14
58	55, 57	eqtri 2496	. . . . . . . . . . . . 13
59	51, 54, 58	3eqtr3i 2504	. . . . . . . . . . . 12
60	59	a1i 11	. . . . . . . . . . 11
61		ax-1cn 9546	. . . . . . . . . . . . 13
62	61, 14, 15	divcli 10282	. . . . . . . . . . . 12
63	62	a1i 11	. . . . . . . . . . 11
64	8, 33, 35, 60, 63	dvmptcmul 22102	. . . . . . . . . 10
65	64	trud 1388	. . . . . . . . 9
66		sqcl 12194	. . . . . . . . . . . . 13
67		mulcl 9572	. . . . . . . . . . . . 13 $/\$
68	14, 66, 67	sylancr 663	. . . . . . . . . . . 12
69		divrec2 10220	. . . . . . . . . . . . 13 $/\$ $/\$
70	14, 15, 69	mp3an23 1316	. . . . . . . . . . . 12
71	9, 68, 70	3syl 20	. . . . . . . . . . 11
72		divcan3 10227	. . . . . . . . . . . . 13 $/\$ $/\$
73	14, 15, 72	mp3an23 1316	. . . . . . . . . . . 12
74	9, 66, 73	3syl 20	. . . . . . . . . . 11
75	71, 74	eqtr3d 2510	. . . . . . . . . 10
76	75	mpteq2ia 4529	. . . . . . . . 9
77	32, 65, 76	3eqtri 2500	. . . . . . . 8
78	77	a1i 11	. . . . . . 7
79	20	adantl 466	. . . . . . 7 $/\$
80		3ex 10607	. . . . . . . 8
81	80	a1i 11	. . . . . . 7 $/\$
82	9	adantl 466	. . . . . . . . 9 $/\$
83	1	a1i 11	. . . . . . . . 9 $/\$
84	8	dvmptid 22095	. . . . . . . . 9
85	14	a1i 11	. . . . . . . . 9
86	8, 82, 83, 84, 85	dvmptcmul 22102	. . . . . . . 8
87		3t1e3 10682	. . . . . . . . 9
88	87	mpteq2i 4530	. . . . . . . 8
89	86, 88	syl6eq 2524	. . . . . . 7
90	8, 25, 27, 78, 79, 81, 89	dvmptsub 22105	. . . . . 6
91		iccssre 11602	. . . . . . . 8 $/\$
92	1, 3, 91	mp2an 672	. . . . . . 7
93	92	a1i 11	. . . . . 6
94		eqid 2467	. . . . . . 7 ℂ_fld ℂ_fld
95	94	tgioo2 21043	. . . . . 6 ℂ_fld ↾_t
96		iccntr 21061	. . . . . . . 8 $/\$
97	1, 3, 96	mp2an 672	. . . . . . 7
98	97	a1i 11	. . . . . 6
99	8, 22, 24, 90, 93, 95, 94, 98	dvmptres2 22100	. . . . 5
100		ioossicc 11606	. . . . . . 7
101		resmpt 5321	. . . . . . 7
102	100, 101	ax-mp 5	. . . . . 6
103	92, 39	sstri 3513	. . . . . . . . 9
104		resmpt 5321	. . . . . . . . 9
105	103, 104	ax-mp 5	. . . . . . . 8
106		eqid 2467	. . . . . . . . . . . 12
107		subcl 9815	. . . . . . . . . . . . . 14 $/\$
108	14, 107	mpan2 671	. . . . . . . . . . . . 13
109	66, 108	syl 16	. . . . . . . . . . . 12
110	106, 109	fmpti 6042	. . . . . . . . . . 11
111	38, 110, 38	3pm3.2i 1174	. . . . . . . . . 10 $/\$ $/\$
112		ovex 6307	. . . . . . . . . . 11
113		cnelprrecn 9581	. . . . . . . . . . . . . 14
114	113	a1i 11	. . . . . . . . . . . . 13
115	66	adantl 466	. . . . . . . . . . . . 13 $/\$
116		ovex 6307	. . . . . . . . . . . . . 14
117	116	a1i 11	. . . . . . . . . . . . 13 $/\$
118		2nn 10689	. . . . . . . . . . . . . . 15
119		dvexp 22091	. . . . . . . . . . . . . . 15
120	118, 119	ax-mp 5	. . . . . . . . . . . . . 14
121	120	a1i 11	. . . . . . . . . . . . 13
122	14	a1i 11	. . . . . . . . . . . . 13 $/\$
123		c0ex 9586	. . . . . . . . . . . . . 14
124	123	a1i 11	. . . . . . . . . . . . 13 $/\$
125	114, 85	dvmptc 22096	. . . . . . . . . . . . 13
126	114, 115, 117, 121, 122, 124, 125	dvmptsub 22105	. . . . . . . . . . . 12
127	126	trud 1388	. . . . . . . . . . 11
128	112, 127	dmmpti 5708	. . . . . . . . . 10
129		dvcn 22059	. . . . . . . . . 10 $/\$ $/\$ $/\$
130	111, 128, 129	mp2an 672	. . . . . . . . 9
131		rescncf 21136	. . . . . . . . 9
132	103, 130, 131	mp2 9	. . . . . . . 8
133	105, 132	eqeltrri 2552	. . . . . . 7
134		rescncf 21136	. . . . . . 7
135	100, 133, 134	mp2 9	. . . . . 6
136	102, 135	eqeltrri 2552	. . . . 5
137	99, 136	syl6eqel 2563	. . . 4
138	100	a1i 11	. . . . . 6
139		ioombl 21710	. . . . . . 7
140	139	a1i 11	. . . . . 6
141	23	a1i 11	. . . . . 6 $/\$
142		cniccibl 21982	. . . . . . . 8 $/\$ $/\$
143	1, 3, 133, 142	mp3an 1324	. . . . . . 7
144	143	a1i 11	. . . . . 6
145	138, 140, 141, 144	iblss 21946	. . . . 5
146	99, 145	eqeltrd 2555	. . . 4
147		resmpt 5321	. . . . . . 7
148	92, 147	ax-mp 5	. . . . . 6
149		eqid 2467	. . . . . . . . . 10
150	149, 21	fmpti 6042	. . . . . . . . 9
151		ssid 3523	. . . . . . . . 9
152	39, 150, 151	3pm3.2i 1174	. . . . . . . 8 $/\$ $/\$
153	90	trud 1388	. . . . . . . . 9
154	23, 153	dmmpti 5708	. . . . . . . 8
155		dvcn 22059	. . . . . . . 8 $/\$ $/\$ $/\$
156	152, 154, 155	mp2an 672	. . . . . . 7
157		rescncf 21136	. . . . . . 7
158	92, 156, 157	mp2 9	. . . . . 6
159	148, 158	eqeltrri 2552	. . . . 5
160	159	a1i 11	. . . 4
161	2, 4, 6, 137, 146, 160	ftc2 22180	. . 3
162	161	trud 1388	. 2
163		itgeq2 21919	. . 3
164		oveq1 6289	. . . . 5
165	164	oveq1d 6297	. . . 4
166	99	trud 1388	. . . 4
167		ovex 6307	. . . 4
168	165, 166, 167	fvmpt 5948	. . 3
169	163, 168	mprg 2827	. 2
170	3	leidi 10083	. . . . . . . . 9
171	1, 3	elicc2i 11586	. . . . . . . . 9 $/\$ $/\$
172	3, 5, 170, 171	mpbir3an 1178	. . . . . . . 8
173		oveq1 6289	. . . . . . . . . . . 12
174	173	oveq1d 6297	. . . . . . . . . . 11
175		oveq2 6290	. . . . . . . . . . 11
176	174, 175	oveq12d 6300	. . . . . . . . . 10
177		cu2 12230	. . . . . . . . . . . . 13
178	177	oveq1i 6292	. . . . . . . . . . . 12
179		3t2e6 10683	. . . . . . . . . . . 12
180	178, 179	oveq12i 6294	. . . . . . . . . . 11
181		2cn 10602	. . . . . . . . . . . . . . 15
182		6cn 10613	. . . . . . . . . . . . . . 15
183	181, 182, 14, 15	divdiri 10297	. . . . . . . . . . . . . 14
184		6p2e8 10673	. . . . . . . . . . . . . . . 16
185	182, 181, 184	addcomli 9767	. . . . . . . . . . . . . . 15
186	185	oveq1i 6292	. . . . . . . . . . . . . 14
187	182, 14, 181, 15	divmuli 10294	. . . . . . . . . . . . . . . 16
188	179, 187	mpbir 209	. . . . . . . . . . . . . . 15
189	188	oveq2i 6293	. . . . . . . . . . . . . 14
190	183, 186, 189	3eqtr3i 2504	. . . . . . . . . . . . 13
191	190	oveq1i 6292	. . . . . . . . . . . 12
192	181, 14, 15	divcli 10282	. . . . . . . . . . . . 13
193		subsub3 9847	. . . . . . . . . . . . 13 $/\$ $/\$
194	192, 182, 181, 193	mp3an 1324	. . . . . . . . . . . 12
195	191, 194	eqtr4i 2499	. . . . . . . . . . 11
196		4cn 10609	. . . . . . . . . . . . 13
197		4p2e6 10666	. . . . . . . . . . . . . 14
198	196, 181, 197	addcomli 9767	. . . . . . . . . . . . 13
199	182, 181, 196, 198	subaddrii 9904	. . . . . . . . . . . 12
200	199	oveq2i 6293	. . . . . . . . . . 11
201	180, 195, 200	3eqtri 2500	. . . . . . . . . 10
202	176, 201	syl6eq 2524	. . . . . . . . 9
203		eqid 2467	. . . . . . . . 9
204		ovex 6307	. . . . . . . . 9
205	202, 203, 204	fvmpt 5948	. . . . . . . 8
206	172, 205	ax-mp 5	. . . . . . 7
207	1	leidi 10083	. . . . . . . . 9
208	1, 3	elicc2i 11586	. . . . . . . . 9 $/\$ $/\$
209	1, 207, 5, 208	mpbir3an 1178	. . . . . . . 8
210		oveq1 6289	. . . . . . . . . . . 12
211	210	oveq1d 6297	. . . . . . . . . . 11
212		oveq2 6290	. . . . . . . . . . 11
213	211, 212	oveq12d 6300	. . . . . . . . . 10
214		3z 10893	. . . . . . . . . . . . 13
215		1exp 12159	. . . . . . . . . . . . 13
216	214, 215	ax-mp 5	. . . . . . . . . . . 12
217	216	oveq1i 6292	. . . . . . . . . . 11
218	217, 87	oveq12i 6294	. . . . . . . . . 10
219	213, 218	syl6eq 2524	. . . . . . . . 9
220		ovex 6307	. . . . . . . . 9
221	219, 203, 220	fvmpt 5948	. . . . . . . 8
222	209, 221	ax-mp 5	. . . . . . 7
223	206, 222	oveq12i 6294	. . . . . 6
224		sub4 9860	. . . . . . 7 $/\$ $/\$ $/\$
225	192, 196, 62, 14, 224	mp4an 673	. . . . . 6
226	14, 15	pm3.2i 455	. . . . . . . . 9 $/\$
227		divsubdir 10236	. . . . . . . . 9 $/\$ $/\$ $/\$
228	181, 61, 226, 227	mp3an 1324	. . . . . . . 8
229		2m1e1 10646	. . . . . . . . 9
230	229	oveq1i 6292	. . . . . . . 8
231	228, 230	eqtr3i 2498	. . . . . . 7
232		3p1e4 10657	. . . . . . . 8
233	196, 14, 61, 232	subaddrii 9904	. . . . . . 7
234	231, 233	oveq12i 6294	. . . . . 6
235	223, 225, 234	3eqtri 2500	. . . . 5
236	14, 15	dividi 10273	. . . . . 6
237	236	oveq2i 6293	. . . . 5
238	235, 237	eqtr4i 2499	. . . 4
239		divsubdir 10236	. . . . 5 $/\$ $/\$ $/\$
240	61, 14, 226, 239	mp3an 1324	. . . 4
241	238, 240	eqtr4i 2499	. . 3
242		divneg 10235	. . . . 5 $/\$ $/\$
243	181, 14, 15, 242	mp3an 1324	. . . 4
244	14, 61	negsubdi2i 9901	. . . . . 6
245	43	negeqi 9809	. . . . . 6
246	244, 245	eqtr3i 2498	. . . . 5
247	246	oveq1i 6292	. . . 4
248	243, 247	eqtr4i 2499	. . 3
249	241, 248	eqtr4i 2499	. 2
250	162, 169, 249	3eqtr3i 2504	1

Colors of variables: wff setvar class

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

wceq 1379

wtru 1380

wcel 1767

wne 2662

cvv 3113

wss 3476

cpr 4029 class class class wbr 4447

cmpt 4505

cdm 4999

crn 5000

cres 5001

wf 5582

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

cle 9625

cmin 9801

cneg 9802

cdiv 10202

cn 10532

c2 10581

c3 10582

c4 10583

c6 10585

c8 10587

cn0 10791

cz 10860

cioo 11525

cicc 11528

cexp 12130

ctopn 14673

ctg 14689 ℂ_fldccnfld 18191

cnt 19284

ccncf 21115

cvol 21610

cibl 21761

citg 21762

cdv 22002

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cc 8811 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-ofr 6523 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-omul 7132 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-acn 8319 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-cmp 19653 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-ovol 21611 df-vol 21612 df-mbf 21763 df-itg1 21764 df-itg2 21765 df-ibl 21766 df-itg 21767 df-0p 21812 df-limc 22005 df-dv 22006

This theorem is referenced by: (None)

W3C validator