lhe4.4ex1a

Description: Example of the Fundamental Theorem of Calculus, part two ( ftc2 ): S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 ) . Section 4.4 example 1a of LarsonHostetlerEdwards p. 311. (The book teaches ftc2 as simply the "Fundamental Theorem of Calculus", then ftc1 as the "Second Fundamental Theorem of Calculus".) (Contributed by Steve Rodriguez, 28-Oct-2015) (Revised by Steve Rodriguez, 31-Oct-2015)

		Ref	Expression
	Assertion	lhe4.4ex1a	\|- S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 )

Proof

Step	Hyp	Ref	Expression
1		1red	\|- ( T. -> 1 e. RR )
2		2re	\|- 2 e. RR
3	2	a1i	\|- ( T. -> 2 e. RR )
4		1le2	\|- 1 <_ 2
5	4	a1i	\|- ( T. -> 1 <_ 2 )
6		reelprrecn	\|- RR e. { RR , CC }
7	6	a1i	\|- ( T. -> RR e. { RR , CC } )
8		recn	\|- ( y e. RR -> y e. CC )
9		3nn0	\|- 3 e. NN0
10		expcl	\|- ( ( y e. CC /\ 3 e. NN0 ) -> ( y ^ 3 ) e. CC )
11	9 10	mpan2	\|- ( y e. CC -> ( y ^ 3 ) e. CC )
12	8 11	syl	\|- ( y e. RR -> ( y ^ 3 ) e. CC )
13		3cn	\|- 3 e. CC
14		3ne0	\|- 3 =/= 0
15		divcl	\|- ( ( ( y ^ 3 ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( y ^ 3 ) / 3 ) e. CC )
16	13 14 15	mp3an23	\|- ( ( y ^ 3 ) e. CC -> ( ( y ^ 3 ) / 3 ) e. CC )
17	12 16	syl	\|- ( y e. RR -> ( ( y ^ 3 ) / 3 ) e. CC )
18		mulcl	\|- ( ( 3 e. CC /\ y e. CC ) -> ( 3 x. y ) e. CC )
19	13 8 18	sylancr	\|- ( y e. RR -> ( 3 x. y ) e. CC )
20	17 19	subcld	\|- ( y e. RR -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) e. CC )
21	20	adantl	\|- ( ( T. /\ y e. RR ) -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) e. CC )
22		ovexd	\|- ( ( T. /\ y e. RR ) -> ( ( y ^ 2 ) - 3 ) e. _V )
23	17	adantl	\|- ( ( T. /\ y e. RR ) -> ( ( y ^ 3 ) / 3 ) e. CC )
24		ovexd	\|- ( ( T. /\ y e. RR ) -> ( y ^ 2 ) e. _V )
25		divrec2	\|- ( ( ( y ^ 3 ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( y ^ 3 ) / 3 ) = ( ( 1 / 3 ) x. ( y ^ 3 ) ) )
26	13 14 25	mp3an23	\|- ( ( y ^ 3 ) e. CC -> ( ( y ^ 3 ) / 3 ) = ( ( 1 / 3 ) x. ( y ^ 3 ) ) )
27	12 26	syl	\|- ( y e. RR -> ( ( y ^ 3 ) / 3 ) = ( ( 1 / 3 ) x. ( y ^ 3 ) ) )
28	27	mpteq2ia	\|- ( y e. RR \|-> ( ( y ^ 3 ) / 3 ) ) = ( y e. RR \|-> ( ( 1 / 3 ) x. ( y ^ 3 ) ) )
29	28	oveq2i	\|- ( RR _D ( y e. RR \|-> ( ( y ^ 3 ) / 3 ) ) ) = ( RR _D ( y e. RR \|-> ( ( 1 / 3 ) x. ( y ^ 3 ) ) ) )
30	12	adantl	\|- ( ( T. /\ y e. RR ) -> ( y ^ 3 ) e. CC )
31		ovexd	\|- ( ( T. /\ y e. RR ) -> ( 3 x. ( y ^ 2 ) ) e. _V )
32		eqid	\|- ( y e. CC \|-> ( y ^ 3 ) ) = ( y e. CC \|-> ( y ^ 3 ) )
33	32 11	fmpti	\|- ( y e. CC \|-> ( y ^ 3 ) ) : CC --> CC
34		ssid	\|- CC C_ CC
35		ax-resscn	\|- RR C_ CC
36		ovex	\|- ( 3 x. ( y ^ 2 ) ) e. _V
37		3nn	\|- 3 e. NN
38		dvexp	\|- ( 3 e. NN -> ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) = ( y e. CC \|-> ( 3 x. ( y ^ ( 3 - 1 ) ) ) ) )
39	37 38	ax-mp	\|- ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) = ( y e. CC \|-> ( 3 x. ( y ^ ( 3 - 1 ) ) ) )
40		3m1e2	\|- ( 3 - 1 ) = 2
41	40	oveq2i	\|- ( y ^ ( 3 - 1 ) ) = ( y ^ 2 )
42	41	oveq2i	\|- ( 3 x. ( y ^ ( 3 - 1 ) ) ) = ( 3 x. ( y ^ 2 ) )
43	42	mpteq2i	\|- ( y e. CC \|-> ( 3 x. ( y ^ ( 3 - 1 ) ) ) ) = ( y e. CC \|-> ( 3 x. ( y ^ 2 ) ) )
44	39 43	eqtri	\|- ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) = ( y e. CC \|-> ( 3 x. ( y ^ 2 ) ) )
45	36 44	dmmpti	\|- dom ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) = CC
46	35 45	sseqtrri	\|- RR C_ dom ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) )
47		dvres3	\|- ( ( ( RR e. { RR , CC } /\ ( y e. CC \|-> ( y ^ 3 ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) ) ) -> ( RR _D ( ( y e. CC \|-> ( y ^ 3 ) ) \|` RR ) ) = ( ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) \|` RR ) )
48	6 33 34 46 47	mp4an	\|- ( RR _D ( ( y e. CC \|-> ( y ^ 3 ) ) \|` RR ) ) = ( ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) \|` RR )
49		resmpt	\|- ( RR C_ CC -> ( ( y e. CC \|-> ( y ^ 3 ) ) \|` RR ) = ( y e. RR \|-> ( y ^ 3 ) ) )
50	35 49	ax-mp	\|- ( ( y e. CC \|-> ( y ^ 3 ) ) \|` RR ) = ( y e. RR \|-> ( y ^ 3 ) )
51	50	oveq2i	\|- ( RR _D ( ( y e. CC \|-> ( y ^ 3 ) ) \|` RR ) ) = ( RR _D ( y e. RR \|-> ( y ^ 3 ) ) )
52	44	reseq1i	\|- ( ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) \|` RR ) = ( ( y e. CC \|-> ( 3 x. ( y ^ 2 ) ) ) \|` RR )
53		resmpt	\|- ( RR C_ CC -> ( ( y e. CC \|-> ( 3 x. ( y ^ 2 ) ) ) \|` RR ) = ( y e. RR \|-> ( 3 x. ( y ^ 2 ) ) ) )
54	35 53	ax-mp	\|- ( ( y e. CC \|-> ( 3 x. ( y ^ 2 ) ) ) \|` RR ) = ( y e. RR \|-> ( 3 x. ( y ^ 2 ) ) )
55	52 54	eqtri	\|- ( ( CC _D ( y e. CC \|-> ( y ^ 3 ) ) ) \|` RR ) = ( y e. RR \|-> ( 3 x. ( y ^ 2 ) ) )
56	48 51 55	3eqtr3i	\|- ( RR _D ( y e. RR \|-> ( y ^ 3 ) ) ) = ( y e. RR \|-> ( 3 x. ( y ^ 2 ) ) )
57	56	a1i	\|- ( T. -> ( RR _D ( y e. RR \|-> ( y ^ 3 ) ) ) = ( y e. RR \|-> ( 3 x. ( y ^ 2 ) ) ) )
58		ax-1cn	\|- 1 e. CC
59	58 13 14	divcli	\|- ( 1 / 3 ) e. CC
60	59	a1i	\|- ( T. -> ( 1 / 3 ) e. CC )
61	7 30 31 57 60	dvmptcmul	\|- ( T. -> ( RR _D ( y e. RR \|-> ( ( 1 / 3 ) x. ( y ^ 3 ) ) ) ) = ( y e. RR \|-> ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) ) )
62	61	mptru	\|- ( RR _D ( y e. RR \|-> ( ( 1 / 3 ) x. ( y ^ 3 ) ) ) ) = ( y e. RR \|-> ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) )
63		sqcl	\|- ( y e. CC -> ( y ^ 2 ) e. CC )
64		mulcl	\|- ( ( 3 e. CC /\ ( y ^ 2 ) e. CC ) -> ( 3 x. ( y ^ 2 ) ) e. CC )
65	13 63 64	sylancr	\|- ( y e. CC -> ( 3 x. ( y ^ 2 ) ) e. CC )
66		divrec2	\|- ( ( ( 3 x. ( y ^ 2 ) ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) )
67	13 14 66	mp3an23	\|- ( ( 3 x. ( y ^ 2 ) ) e. CC -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) )
68	8 65 67	3syl	\|- ( y e. RR -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) )
69		divcan3	\|- ( ( ( y ^ 2 ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( y ^ 2 ) )
70	13 14 69	mp3an23	\|- ( ( y ^ 2 ) e. CC -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( y ^ 2 ) )
71	8 63 70	3syl	\|- ( y e. RR -> ( ( 3 x. ( y ^ 2 ) ) / 3 ) = ( y ^ 2 ) )
72	68 71	eqtr3d	\|- ( y e. RR -> ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) = ( y ^ 2 ) )
73	72	mpteq2ia	\|- ( y e. RR \|-> ( ( 1 / 3 ) x. ( 3 x. ( y ^ 2 ) ) ) ) = ( y e. RR \|-> ( y ^ 2 ) )
74	29 62 73	3eqtri	\|- ( RR _D ( y e. RR \|-> ( ( y ^ 3 ) / 3 ) ) ) = ( y e. RR \|-> ( y ^ 2 ) )
75	74	a1i	\|- ( T. -> ( RR _D ( y e. RR \|-> ( ( y ^ 3 ) / 3 ) ) ) = ( y e. RR \|-> ( y ^ 2 ) ) )
76	19	adantl	\|- ( ( T. /\ y e. RR ) -> ( 3 x. y ) e. CC )
77		3ex	\|- 3 e. _V
78	77	a1i	\|- ( ( T. /\ y e. RR ) -> 3 e. _V )
79	8	adantl	\|- ( ( T. /\ y e. RR ) -> y e. CC )
80		1red	\|- ( ( T. /\ y e. RR ) -> 1 e. RR )
81	7	dvmptid	\|- ( T. -> ( RR _D ( y e. RR \|-> y ) ) = ( y e. RR \|-> 1 ) )
82	13	a1i	\|- ( T. -> 3 e. CC )
83	7 79 80 81 82	dvmptcmul	\|- ( T. -> ( RR _D ( y e. RR \|-> ( 3 x. y ) ) ) = ( y e. RR \|-> ( 3 x. 1 ) ) )
84		3t1e3	\|- ( 3 x. 1 ) = 3
85	84	mpteq2i	\|- ( y e. RR \|-> ( 3 x. 1 ) ) = ( y e. RR \|-> 3 )
86	83 85	eqtrdi	\|- ( T. -> ( RR _D ( y e. RR \|-> ( 3 x. y ) ) ) = ( y e. RR \|-> 3 ) )
87	7 23 24 75 76 78 86	dvmptsub	\|- ( T. -> ( RR _D ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = ( y e. RR \|-> ( ( y ^ 2 ) - 3 ) ) )
88		1re	\|- 1 e. RR
89		iccssre	\|- ( ( 1 e. RR /\ 2 e. RR ) -> ( 1 [,] 2 ) C_ RR )
90	88 2 89	mp2an	\|- ( 1 [,] 2 ) C_ RR
91	90	a1i	\|- ( T. -> ( 1 [,] 2 ) C_ RR )
92		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
93	92	tgioo2	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
94		iccntr	\|- ( ( 1 e. RR /\ 2 e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 1 [,] 2 ) ) = ( 1 (,) 2 ) )
95	88 2 94	mp2an	\|- ( ( int ` ( topGen ` ran (,) ) ) ` ( 1 [,] 2 ) ) = ( 1 (,) 2 )
96	95	a1i	\|- ( T. -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 1 [,] 2 ) ) = ( 1 (,) 2 ) )
97	7 21 22 87 91 93 92 96	dvmptres2	\|- ( T. -> ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) )
98		ioossicc	\|- ( 1 (,) 2 ) C_ ( 1 [,] 2 )
99		resmpt	\|- ( ( 1 (,) 2 ) C_ ( 1 [,] 2 ) -> ( ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 (,) 2 ) ) = ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) )
100	98 99	ax-mp	\|- ( ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 (,) 2 ) ) = ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) )
101	90 35	sstri	\|- ( 1 [,] 2 ) C_ CC
102		resmpt	\|- ( ( 1 [,] 2 ) C_ CC -> ( ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 [,] 2 ) ) = ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) )
103	101 102	ax-mp	\|- ( ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 [,] 2 ) ) = ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) )
104		eqid	\|- ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) = ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) )
105		subcl	\|- ( ( ( y ^ 2 ) e. CC /\ 3 e. CC ) -> ( ( y ^ 2 ) - 3 ) e. CC )
106	13 105	mpan2	\|- ( ( y ^ 2 ) e. CC -> ( ( y ^ 2 ) - 3 ) e. CC )
107	63 106	syl	\|- ( y e. CC -> ( ( y ^ 2 ) - 3 ) e. CC )
108	104 107	fmpti	\|- ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) : CC --> CC
109	34 108 34	3pm3.2i	\|- ( CC C_ CC /\ ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) : CC --> CC /\ CC C_ CC )
110		ovex	\|- ( ( 2 x. ( y ^ ( 2 - 1 ) ) ) - 0 ) e. _V
111		cnelprrecn	\|- CC e. { RR , CC }
112	111	a1i	\|- ( T. -> CC e. { RR , CC } )
113	63	adantl	\|- ( ( T. /\ y e. CC ) -> ( y ^ 2 ) e. CC )
114		ovexd	\|- ( ( T. /\ y e. CC ) -> ( 2 x. ( y ^ ( 2 - 1 ) ) ) e. _V )
115		2nn	\|- 2 e. NN
116		dvexp	\|- ( 2 e. NN -> ( CC _D ( y e. CC \|-> ( y ^ 2 ) ) ) = ( y e. CC \|-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) ) )
117	115 116	ax-mp	\|- ( CC _D ( y e. CC \|-> ( y ^ 2 ) ) ) = ( y e. CC \|-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) )
118	117	a1i	\|- ( T. -> ( CC _D ( y e. CC \|-> ( y ^ 2 ) ) ) = ( y e. CC \|-> ( 2 x. ( y ^ ( 2 - 1 ) ) ) ) )
119	13	a1i	\|- ( ( T. /\ y e. CC ) -> 3 e. CC )
120		c0ex	\|- 0 e. _V
121	120	a1i	\|- ( ( T. /\ y e. CC ) -> 0 e. _V )
122	112 82	dvmptc	\|- ( T. -> ( CC _D ( y e. CC \|-> 3 ) ) = ( y e. CC \|-> 0 ) )
123	112 113 114 118 119 121 122	dvmptsub	\|- ( T. -> ( CC _D ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) ) = ( y e. CC \|-> ( ( 2 x. ( y ^ ( 2 - 1 ) ) ) - 0 ) ) )
124	123	mptru	\|- ( CC _D ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) ) = ( y e. CC \|-> ( ( 2 x. ( y ^ ( 2 - 1 ) ) ) - 0 ) )
125	110 124	dmmpti	\|- dom ( CC _D ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) ) = CC
126		dvcn	\|- ( ( ( CC C_ CC /\ ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) : CC --> CC /\ CC C_ CC ) /\ dom ( CC _D ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) ) = CC ) -> ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) e. ( CC -cn-> CC ) )
127	109 125 126	mp2an	\|- ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) e. ( CC -cn-> CC )
128		rescncf	\|- ( ( 1 [,] 2 ) C_ CC -> ( ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) e. ( CC -cn-> CC ) -> ( ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 [,] 2 ) ) e. ( ( 1 [,] 2 ) -cn-> CC ) ) )
129	101 127 128	mp2	\|- ( ( y e. CC \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 [,] 2 ) ) e. ( ( 1 [,] 2 ) -cn-> CC )
130	103 129	eqeltrri	\|- ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. ( ( 1 [,] 2 ) -cn-> CC )
131		rescncf	\|- ( ( 1 (,) 2 ) C_ ( 1 [,] 2 ) -> ( ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. ( ( 1 [,] 2 ) -cn-> CC ) -> ( ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 (,) 2 ) ) e. ( ( 1 (,) 2 ) -cn-> CC ) ) )
132	98 130 131	mp2	\|- ( ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) \|` ( 1 (,) 2 ) ) e. ( ( 1 (,) 2 ) -cn-> CC )
133	100 132	eqeltrri	\|- ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. ( ( 1 (,) 2 ) -cn-> CC )
134	97 133	eqeltrdi	\|- ( T. -> ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) e. ( ( 1 (,) 2 ) -cn-> CC ) )
135	98	a1i	\|- ( T. -> ( 1 (,) 2 ) C_ ( 1 [,] 2 ) )
136		ioombl	\|- ( 1 (,) 2 ) e. dom vol
137	136	a1i	\|- ( T. -> ( 1 (,) 2 ) e. dom vol )
138		ovexd	\|- ( ( T. /\ y e. ( 1 [,] 2 ) ) -> ( ( y ^ 2 ) - 3 ) e. _V )
139		cniccibl	\|- ( ( 1 e. RR /\ 2 e. RR /\ ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. ( ( 1 [,] 2 ) -cn-> CC ) ) -> ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. L^1 )
140	88 2 130 139	mp3an	\|- ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. L^1
141	140	a1i	\|- ( T. -> ( y e. ( 1 [,] 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. L^1 )
142	135 137 138 141	iblss	\|- ( T. -> ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) ) e. L^1 )
143	97 142	eqeltrd	\|- ( T. -> ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) e. L^1 )
144		resmpt	\|- ( ( 1 [,] 2 ) C_ RR -> ( ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) \|` ( 1 [,] 2 ) ) = ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) )
145	90 144	ax-mp	\|- ( ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) \|` ( 1 [,] 2 ) ) = ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) )
146		eqid	\|- ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) = ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) )
147	146 20	fmpti	\|- ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) : RR --> CC
148		ssid	\|- RR C_ RR
149	35 147 148	3pm3.2i	\|- ( RR C_ CC /\ ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) : RR --> CC /\ RR C_ RR )
150		ovex	\|- ( ( y ^ 2 ) - 3 ) e. _V
151	87	mptru	\|- ( RR _D ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = ( y e. RR \|-> ( ( y ^ 2 ) - 3 ) )
152	150 151	dmmpti	\|- dom ( RR _D ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = RR
153		dvcn	\|- ( ( ( RR C_ CC /\ ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) : RR --> CC /\ RR C_ RR ) /\ dom ( RR _D ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = RR ) -> ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) e. ( RR -cn-> CC ) )
154	149 152 153	mp2an	\|- ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) e. ( RR -cn-> CC )
155		rescncf	\|- ( ( 1 [,] 2 ) C_ RR -> ( ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) e. ( RR -cn-> CC ) -> ( ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) \|` ( 1 [,] 2 ) ) e. ( ( 1 [,] 2 ) -cn-> CC ) ) )
156	90 154 155	mp2	\|- ( ( y e. RR \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) \|` ( 1 [,] 2 ) ) e. ( ( 1 [,] 2 ) -cn-> CC )
157	145 156	eqeltrri	\|- ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) e. ( ( 1 [,] 2 ) -cn-> CC )
158	157	a1i	\|- ( T. -> ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) e. ( ( 1 [,] 2 ) -cn-> CC ) )
159	1 3 5 134 143 158	ftc2	\|- ( T. -> S. ( 1 (,) 2 ) ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) _d x = ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) )
160	159	mptru	\|- S. ( 1 (,) 2 ) ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) _d x = ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) )
161		itgeq2	\|- ( A. x e. ( 1 (,) 2 ) ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) = ( ( x ^ 2 ) - 3 ) -> S. ( 1 (,) 2 ) ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) _d x = S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x )
162		oveq1	\|- ( y = x -> ( y ^ 2 ) = ( x ^ 2 ) )
163	162	oveq1d	\|- ( y = x -> ( ( y ^ 2 ) - 3 ) = ( ( x ^ 2 ) - 3 ) )
164	97	mptru	\|- ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) = ( y e. ( 1 (,) 2 ) \|-> ( ( y ^ 2 ) - 3 ) )
165		ovex	\|- ( ( x ^ 2 ) - 3 ) e. _V
166	163 164 165	fvmpt	\|- ( x e. ( 1 (,) 2 ) -> ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) = ( ( x ^ 2 ) - 3 ) )
167	161 166	mprg	\|- S. ( 1 (,) 2 ) ( ( RR _D ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ) ` x ) _d x = S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x
168	2	leidi	\|- 2 <_ 2
169	88 2	elicc2i	\|- ( 2 e. ( 1 [,] 2 ) <-> ( 2 e. RR /\ 1 <_ 2 /\ 2 <_ 2 ) )
170	2 4 168 169	mpbir3an	\|- 2 e. ( 1 [,] 2 )
171		oveq1	\|- ( y = 2 -> ( y ^ 3 ) = ( 2 ^ 3 ) )
172	171	oveq1d	\|- ( y = 2 -> ( ( y ^ 3 ) / 3 ) = ( ( 2 ^ 3 ) / 3 ) )
173		oveq2	\|- ( y = 2 -> ( 3 x. y ) = ( 3 x. 2 ) )
174	172 173	oveq12d	\|- ( y = 2 -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) = ( ( ( 2 ^ 3 ) / 3 ) - ( 3 x. 2 ) ) )
175		cu2	\|- ( 2 ^ 3 ) = 8
176	175	oveq1i	\|- ( ( 2 ^ 3 ) / 3 ) = ( 8 / 3 )
177		3t2e6	\|- ( 3 x. 2 ) = 6
178	176 177	oveq12i	\|- ( ( ( 2 ^ 3 ) / 3 ) - ( 3 x. 2 ) ) = ( ( 8 / 3 ) - 6 )
179		2cn	\|- 2 e. CC
180		6cn	\|- 6 e. CC
181	179 180 13 14	divdiri	\|- ( ( 2 + 6 ) / 3 ) = ( ( 2 / 3 ) + ( 6 / 3 ) )
182		6p2e8	\|- ( 6 + 2 ) = 8
183	180 179 182	addcomli	\|- ( 2 + 6 ) = 8
184	183	oveq1i	\|- ( ( 2 + 6 ) / 3 ) = ( 8 / 3 )
185	180 13 179 14	divmuli	\|- ( ( 6 / 3 ) = 2 <-> ( 3 x. 2 ) = 6 )
186	177 185	mpbir	\|- ( 6 / 3 ) = 2
187	186	oveq2i	\|- ( ( 2 / 3 ) + ( 6 / 3 ) ) = ( ( 2 / 3 ) + 2 )
188	181 184 187	3eqtr3i	\|- ( 8 / 3 ) = ( ( 2 / 3 ) + 2 )
189	188	oveq1i	\|- ( ( 8 / 3 ) - 6 ) = ( ( ( 2 / 3 ) + 2 ) - 6 )
190	179 13 14	divcli	\|- ( 2 / 3 ) e. CC
191		subsub3	\|- ( ( ( 2 / 3 ) e. CC /\ 6 e. CC /\ 2 e. CC ) -> ( ( 2 / 3 ) - ( 6 - 2 ) ) = ( ( ( 2 / 3 ) + 2 ) - 6 ) )
192	190 180 179 191	mp3an	\|- ( ( 2 / 3 ) - ( 6 - 2 ) ) = ( ( ( 2 / 3 ) + 2 ) - 6 )
193	189 192	eqtr4i	\|- ( ( 8 / 3 ) - 6 ) = ( ( 2 / 3 ) - ( 6 - 2 ) )
194		4cn	\|- 4 e. CC
195		4p2e6	\|- ( 4 + 2 ) = 6
196	194 179 195	addcomli	\|- ( 2 + 4 ) = 6
197	180 179 194 196	subaddrii	\|- ( 6 - 2 ) = 4
198	197	oveq2i	\|- ( ( 2 / 3 ) - ( 6 - 2 ) ) = ( ( 2 / 3 ) - 4 )
199	178 193 198	3eqtri	\|- ( ( ( 2 ^ 3 ) / 3 ) - ( 3 x. 2 ) ) = ( ( 2 / 3 ) - 4 )
200	174 199	eqtrdi	\|- ( y = 2 -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) = ( ( 2 / 3 ) - 4 ) )
201		eqid	\|- ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) = ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) )
202		ovex	\|- ( ( 2 / 3 ) - 4 ) e. _V
203	200 201 202	fvmpt	\|- ( 2 e. ( 1 [,] 2 ) -> ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) = ( ( 2 / 3 ) - 4 ) )
204	170 203	ax-mp	\|- ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) = ( ( 2 / 3 ) - 4 )
205	88	leidi	\|- 1 <_ 1
206	88 2	elicc2i	\|- ( 1 e. ( 1 [,] 2 ) <-> ( 1 e. RR /\ 1 <_ 1 /\ 1 <_ 2 ) )
207	88 205 4 206	mpbir3an	\|- 1 e. ( 1 [,] 2 )
208		oveq1	\|- ( y = 1 -> ( y ^ 3 ) = ( 1 ^ 3 ) )
209	208	oveq1d	\|- ( y = 1 -> ( ( y ^ 3 ) / 3 ) = ( ( 1 ^ 3 ) / 3 ) )
210		oveq2	\|- ( y = 1 -> ( 3 x. y ) = ( 3 x. 1 ) )
211	209 210	oveq12d	\|- ( y = 1 -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) = ( ( ( 1 ^ 3 ) / 3 ) - ( 3 x. 1 ) ) )
212		3z	\|- 3 e. ZZ
213		1exp	\|- ( 3 e. ZZ -> ( 1 ^ 3 ) = 1 )
214	212 213	ax-mp	\|- ( 1 ^ 3 ) = 1
215	214	oveq1i	\|- ( ( 1 ^ 3 ) / 3 ) = ( 1 / 3 )
216	215 84	oveq12i	\|- ( ( ( 1 ^ 3 ) / 3 ) - ( 3 x. 1 ) ) = ( ( 1 / 3 ) - 3 )
217	211 216	eqtrdi	\|- ( y = 1 -> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) = ( ( 1 / 3 ) - 3 ) )
218		ovex	\|- ( ( 1 / 3 ) - 3 ) e. _V
219	217 201 218	fvmpt	\|- ( 1 e. ( 1 [,] 2 ) -> ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) = ( ( 1 / 3 ) - 3 ) )
220	207 219	ax-mp	\|- ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) = ( ( 1 / 3 ) - 3 )
221	204 220	oveq12i	\|- ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) = ( ( ( 2 / 3 ) - 4 ) - ( ( 1 / 3 ) - 3 ) )
222		sub4	\|- ( ( ( ( 2 / 3 ) e. CC /\ 4 e. CC ) /\ ( ( 1 / 3 ) e. CC /\ 3 e. CC ) ) -> ( ( ( 2 / 3 ) - 4 ) - ( ( 1 / 3 ) - 3 ) ) = ( ( ( 2 / 3 ) - ( 1 / 3 ) ) - ( 4 - 3 ) ) )
223	190 194 59 13 222	mp4an	\|- ( ( ( 2 / 3 ) - 4 ) - ( ( 1 / 3 ) - 3 ) ) = ( ( ( 2 / 3 ) - ( 1 / 3 ) ) - ( 4 - 3 ) )
224	13 14	pm3.2i	\|- ( 3 e. CC /\ 3 =/= 0 )
225		divsubdir	\|- ( ( 2 e. CC /\ 1 e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 2 - 1 ) / 3 ) = ( ( 2 / 3 ) - ( 1 / 3 ) ) )
226	179 58 224 225	mp3an	\|- ( ( 2 - 1 ) / 3 ) = ( ( 2 / 3 ) - ( 1 / 3 ) )
227		2m1e1	\|- ( 2 - 1 ) = 1
228	227	oveq1i	\|- ( ( 2 - 1 ) / 3 ) = ( 1 / 3 )
229	226 228	eqtr3i	\|- ( ( 2 / 3 ) - ( 1 / 3 ) ) = ( 1 / 3 )
230		3p1e4	\|- ( 3 + 1 ) = 4
231	194 13 58 230	subaddrii	\|- ( 4 - 3 ) = 1
232	229 231	oveq12i	\|- ( ( ( 2 / 3 ) - ( 1 / 3 ) ) - ( 4 - 3 ) ) = ( ( 1 / 3 ) - 1 )
233	221 223 232	3eqtri	\|- ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) = ( ( 1 / 3 ) - 1 )
234	13 14	dividi	\|- ( 3 / 3 ) = 1
235	234	oveq2i	\|- ( ( 1 / 3 ) - ( 3 / 3 ) ) = ( ( 1 / 3 ) - 1 )
236	233 235	eqtr4i	\|- ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) = ( ( 1 / 3 ) - ( 3 / 3 ) )
237		divsubdir	\|- ( ( 1 e. CC /\ 3 e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 1 - 3 ) / 3 ) = ( ( 1 / 3 ) - ( 3 / 3 ) ) )
238	58 13 224 237	mp3an	\|- ( ( 1 - 3 ) / 3 ) = ( ( 1 / 3 ) - ( 3 / 3 ) )
239	236 238	eqtr4i	\|- ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) = ( ( 1 - 3 ) / 3 )
240		divneg	\|- ( ( 2 e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> -u ( 2 / 3 ) = ( -u 2 / 3 ) )
241	179 13 14 240	mp3an	\|- -u ( 2 / 3 ) = ( -u 2 / 3 )
242	13 58	negsubdi2i	\|- -u ( 3 - 1 ) = ( 1 - 3 )
243	40	negeqi	\|- -u ( 3 - 1 ) = -u 2
244	242 243	eqtr3i	\|- ( 1 - 3 ) = -u 2
245	244	oveq1i	\|- ( ( 1 - 3 ) / 3 ) = ( -u 2 / 3 )
246	241 245	eqtr4i	\|- -u ( 2 / 3 ) = ( ( 1 - 3 ) / 3 )
247	239 246	eqtr4i	\|- ( ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 2 ) - ( ( y e. ( 1 [,] 2 ) \|-> ( ( ( y ^ 3 ) / 3 ) - ( 3 x. y ) ) ) ` 1 ) ) = -u ( 2 / 3 )
248	160 167 247	3eqtr3i	\|- S. ( 1 (,) 2 ) ( ( x ^ 2 ) - 3 ) _d x = -u ( 2 / 3 )

Metamath Proof Explorer

Theorem lhe4.4ex1a

Proof