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 ) |