Proof of Theorem ftc1cnnclem
Step | Hyp | Ref
| Expression |
1 | | ftc1cnnc.a |
. . . . . . . . . . . . . 14
|
2 | | ftc1cnnc.b |
. . . . . . . . . . . . . 14
|
3 | | iccssre 12255 |
. . . . . . . . . . . . . 14
|
4 | 1, 2, 3 | syl2anc 693 |
. . . . . . . . . . . . 13
|
5 | | ftc1cnnclem.x1 |
. . . . . . . . . . . . 13
|
6 | 4, 5 | sseldd 3604 |
. . . . . . . . . . . 12
|
7 | | ftc1cnnclem.y1 |
. . . . . . . . . . . . 13
|
8 | 4, 7 | sseldd 3604 |
. . . . . . . . . . . 12
|
9 | | ltle 10126 |
. . . . . . . . . . . 12
|
10 | 6, 8, 9 | syl2anc 693 |
. . . . . . . . . . 11
|
11 | 10 | imp 445 |
. . . . . . . . . 10
|
12 | | ftc1cnnc.g |
. . . . . . . . . . 11
|
13 | | ftc1cnnc.le |
. . . . . . . . . . 11
|
14 | | ssid 3624 |
. . . . . . . . . . . 12
|
15 | 14 | a1i 11 |
. . . . . . . . . . 11
|
16 | | ioossre 12235 |
. . . . . . . . . . . 12
|
17 | 16 | a1i 11 |
. . . . . . . . . . 11
|
18 | | ftc1cnnc.i |
. . . . . . . . . . 11
|
19 | | ftc1cnnc.f |
. . . . . . . . . . . 12
|
20 | | cncff 22696 |
. . . . . . . . . . . 12
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
|
22 | 12, 1, 2, 13, 15, 17, 18, 21, 5, 7 | ftc1lem1 23798 |
. . . . . . . . . 10
|
23 | 11, 22 | syldan 487 |
. . . . . . . . 9
|
24 | 1 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
|
25 | 2 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
|
26 | | elicc1 12219 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 26 | biimpa 501 |
. . . . . . . . . . . . . . . . . 18
|
28 | 27 | simp2d 1074 |
. . . . . . . . . . . . . . . . 17
|
29 | 24, 25, 5, 28 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
|
30 | | iccleub 12229 |
. . . . . . . . . . . . . . . . 17
|
31 | 24, 25, 7, 30 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
32 | | ioossioo 12265 |
. . . . . . . . . . . . . . . 16
|
33 | 24, 25, 29, 31, 32 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
|
34 | 33 | sselda 3603 |
. . . . . . . . . . . . . 14
|
35 | 21 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
36 | 34, 35 | syldan 487 |
. . . . . . . . . . . . 13
|
37 | | ftc1cnnclem.c |
. . . . . . . . . . . . . . 15
|
38 | 21, 37 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
39 | 38 | adantr 481 |
. . . . . . . . . . . . 13
|
40 | 36, 39 | npcand 10396 |
. . . . . . . . . . . 12
|
41 | 40 | itgeq2dv 23548 |
. . . . . . . . . . 11
|
42 | 36, 39 | subcld 10392 |
. . . . . . . . . . . 12
|
43 | | ioombl 23333 |
. . . . . . . . . . . . . . 15
|
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
|
45 | | fvexd 6203 |
. . . . . . . . . . . . . 14
|
46 | 21 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
|
47 | 46, 18 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
|
48 | 33, 44, 45, 47 | iblss 23571 |
. . . . . . . . . . . . 13
|
49 | | fconstmpt 5163 |
. . . . . . . . . . . . . 14
|
50 | | mblvol 23298 |
. . . . . . . . . . . . . . . . 17
|
51 | 43, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
52 | | ioossicc 12259 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
54 | | iccmbl 23334 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 6, 8, 54 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
56 | | mblss 23299 |
. . . . . . . . . . . . . . . . . 18
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
58 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 55, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
60 | | iccvolcl 23335 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 6, 8, 60 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
62 | 59, 61 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
63 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . 17
|
64 | 53, 57, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
65 | 51, 64 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
|
66 | | iblconst 23584 |
. . . . . . . . . . . . . . 15
|
67 | 44, 65, 38, 66 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
68 | 49, 67 | syl5eqelr 2706 |
. . . . . . . . . . . . 13
|
69 | | eqid 2622 |
. . . . . . . . . . . . . . 15
ℂfld ℂfld |
70 | 69 | subcn 22669 |
. . . . . . . . . . . . . . . 16
ℂfld ℂfld ℂfld |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . 15
ℂfld
ℂfld ℂfld |
72 | 21, 33 | feqresmpt 6250 |
. . . . . . . . . . . . . . . 16
|
73 | | rescncf 22700 |
. . . . . . . . . . . . . . . . 17
|
74 | 33, 19, 73 | sylc 65 |
. . . . . . . . . . . . . . . 16
|
75 | 72, 74 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
76 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . 18
|
77 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . 18
|
78 | 76, 77 | sstri 3612 |
. . . . . . . . . . . . . . . . 17
|
79 | | ssid 3624 |
. . . . . . . . . . . . . . . . 17
|
80 | | cncfmptc 22714 |
. . . . . . . . . . . . . . . . 17
|
81 | 78, 79, 80 | mp3an23 1416 |
. . . . . . . . . . . . . . . 16
|
82 | 38, 81 | syl 17 |
. . . . . . . . . . . . . . 15
|
83 | 69, 71, 75, 82 | cncfmpt2f 22717 |
. . . . . . . . . . . . . 14
|
84 | | cnmbf 23426 |
. . . . . . . . . . . . . 14
MblFn |
85 | 43, 83, 84 | sylancr 695 |
. . . . . . . . . . . . 13
MblFn |
86 | 36, 48, 39, 68, 85 | iblsubnc 33471 |
. . . . . . . . . . . 12
|
87 | 40 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
|
88 | 87, 72 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
89 | | iblmbf 23534 |
. . . . . . . . . . . . . . 15
MblFn |
90 | 18, 89 | syl 17 |
. . . . . . . . . . . . . 14
MblFn |
91 | | mbfres 23411 |
. . . . . . . . . . . . . 14
MblFn
MblFn |
92 | 90, 43, 91 | sylancl 694 |
. . . . . . . . . . . . 13
MblFn |
93 | 88, 92 | eqeltrd 2701 |
. . . . . . . . . . . 12
MblFn |
94 | 42, 86, 39, 68, 93 | itgaddnc 33470 |
. . . . . . . . . . 11
|
95 | 41, 94 | eqtr3d 2658 |
. . . . . . . . . 10
|
96 | 95 | adantr 481 |
. . . . . . . . 9
|
97 | | itgconst 23585 |
. . . . . . . . . . . . 13
|
98 | 44, 65, 38, 97 | syl3anc 1326 |
. . . . . . . . . . . 12
|
99 | 98 | adantr 481 |
. . . . . . . . . . 11
|
100 | 6 | adantr 481 |
. . . . . . . . . . . . . 14
|
101 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
|
102 | | ovolioo 23336 |
. . . . . . . . . . . . . 14
|
103 | 100, 101,
11, 102 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
104 | 51, 103 | syl5eq 2668 |
. . . . . . . . . . . 12
|
105 | 104 | oveq2d 6666 |
. . . . . . . . . . 11
|
106 | 99, 105 | eqtrd 2656 |
. . . . . . . . . 10
|
107 | 106 | oveq2d 6666 |
. . . . . . . . 9
|
108 | 23, 96, 107 | 3eqtrd 2660 |
. . . . . . . 8
|
109 | 108 | oveq1d 6665 |
. . . . . . 7
|
110 | | ovexd 6680 |
. . . . . . . . . 10
|
111 | 110, 86 | itgcl 23550 |
. . . . . . . . 9
|
112 | 111 | adantr 481 |
. . . . . . . 8
|
113 | 38 | adantr 481 |
. . . . . . . . 9
|
114 | 8, 6 | resubcld 10458 |
. . . . . . . . . . 11
|
115 | 114 | recnd 10068 |
. . . . . . . . . 10
|
116 | 115 | adantr 481 |
. . . . . . . . 9
|
117 | 113, 116 | mulcld 10060 |
. . . . . . . 8
|
118 | 6, 8 | posdifd 10614 |
. . . . . . . . . 10
|
119 | 118 | biimpa 501 |
. . . . . . . . 9
|
120 | 119 | gt0ne0d 10592 |
. . . . . . . 8
|
121 | 112, 117,
116, 120 | divdird 10839 |
. . . . . . 7
|
122 | 113, 116,
120 | divcan4d 10807 |
. . . . . . . 8
|
123 | 122 | oveq2d 6666 |
. . . . . . 7
|
124 | 109, 121,
123 | 3eqtrd 2660 |
. . . . . 6
|
125 | 124 | oveq1d 6665 |
. . . . 5
|
126 | 112, 116,
120 | divcld 10801 |
. . . . . 6
|
127 | 126, 113 | pncand 10393 |
. . . . 5
|
128 | 125, 127 | eqtrd 2656 |
. . . 4
|
129 | 128 | fveq2d 6195 |
. . 3
|
130 | 112, 116,
120 | absdivd 14194 |
. . 3
|
131 | 114 | adantr 481 |
. . . . 5
|
132 | | 0re 10040 |
. . . . . . 7
|
133 | | ltle 10126 |
. . . . . . 7
|
134 | 132, 131,
133 | sylancr 695 |
. . . . . 6
|
135 | 119, 134 | mpd 15 |
. . . . 5
|
136 | 131, 135 | absidd 14161 |
. . . 4
|
137 | 136 | oveq2d 6666 |
. . 3
|
138 | 129, 130,
137 | 3eqtrd 2660 |
. 2
|
139 | 112 | abscld 14175 |
. . . 4
|
140 | 42 | abscld 14175 |
. . . . . 6
|
141 | | cncfss 22702 |
. . . . . . . . . . . 12
|
142 | 77, 79, 141 | mp2an 708 |
. . . . . . . . . . 11
|
143 | | abscncf 22704 |
. . . . . . . . . . 11
|
144 | 142, 143 | sselii 3600 |
. . . . . . . . . 10
|
145 | 144 | a1i 11 |
. . . . . . . . 9
|
146 | 145, 83 | cncfmpt1f 22716 |
. . . . . . . 8
|
147 | | cnmbf 23426 |
. . . . . . . 8
MblFn |
148 | 43, 146, 147 | sylancr 695 |
. . . . . . 7
MblFn |
149 | 110, 86, 148 | iblabsnc 33474 |
. . . . . 6
|
150 | 140, 149 | itgrecl 23564 |
. . . . 5
|
151 | 150 | adantr 481 |
. . . 4
|
152 | | ftc1cnnclem.e |
. . . . . . 7
|
153 | 152 | rpred 11872 |
. . . . . 6
|
154 | 114, 153 | remulcld 10070 |
. . . . 5
|
155 | 154 | adantr 481 |
. . . 4
|
156 | 111 | cjcld 13936 |
. . . . . . . . 9
|
157 | | cncfmptc 22714 |
. . . . . . . . . 10
|
158 | 78, 79, 157 | mp3an23 1416 |
. . . . . . . . 9
|
159 | 156, 158 | syl 17 |
. . . . . . . 8
|
160 | | nfcv 2764 |
. . . . . . . . . 10
|
161 | | nfcsb1v 3549 |
. . . . . . . . . 10
|
162 | | csbeq1a 3542 |
. . . . . . . . . 10
|
163 | 160, 161,
162 | cbvmpt 4749 |
. . . . . . . . 9
|
164 | 163, 83 | syl5eqelr 2706 |
. . . . . . . 8
|
165 | 159, 164 | mulcncf 23215 |
. . . . . . 7
|
166 | | cnmbf 23426 |
. . . . . . 7
MblFn |
167 | 43, 165, 166 | sylancr 695 |
. . . . . 6
MblFn |
168 | 42, 86, 148, 167 | itgabsnc 33479 |
. . . . 5
|
169 | 168 | adantr 481 |
. . . 4
|
170 | | simpr 477 |
. . . . . . 7
|
171 | 153 | adantr 481 |
. . . . . . . . 9
|
172 | | fconstmpt 5163 |
. . . . . . . . . 10
|
173 | 152 | rpcnd 11874 |
. . . . . . . . . . 11
|
174 | | iblconst 23584 |
. . . . . . . . . . 11
|
175 | 44, 65, 173, 174 | syl3anc 1326 |
. . . . . . . . . 10
|
176 | 172, 175 | syl5eqelr 2706 |
. . . . . . . . 9
|
177 | | cncfmptc 22714 |
. . . . . . . . . . . . 13
|
178 | 78, 79, 177 | mp3an23 1416 |
. . . . . . . . . . . 12
|
179 | 173, 178 | syl 17 |
. . . . . . . . . . 11
|
180 | 69, 71, 179, 146 | cncfmpt2f 22717 |
. . . . . . . . . 10
|
181 | | cnmbf 23426 |
. . . . . . . . . 10
MblFn |
182 | 43, 180, 181 | sylancr 695 |
. . . . . . . . 9
MblFn |
183 | 171, 176,
140, 149, 182 | iblsubnc 33471 |
. . . . . . . 8
|
184 | 183 | adantr 481 |
. . . . . . 7
|
185 | | ftc1cnnclem.fc |
. . . . . . . . . . . 12
|
186 | 185 | ralrimiva 2966 |
. . . . . . . . . . 11
|
187 | 186 | adantr 481 |
. . . . . . . . . 10
|
188 | 16, 37 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
189 | | ftc1cnnclem.r |
. . . . . . . . . . . . . . 15
|
190 | 189 | rpred 11872 |
. . . . . . . . . . . . . 14
|
191 | 188, 190 | resubcld 10458 |
. . . . . . . . . . . . 13
|
192 | 191 | adantr 481 |
. . . . . . . . . . . 12
|
193 | 6 | adantr 481 |
. . . . . . . . . . . 12
|
194 | | elioore 12205 |
. . . . . . . . . . . . 13
|
195 | 194 | adantl 482 |
. . . . . . . . . . . 12
|
196 | | ftc1cnnclem.x2 |
. . . . . . . . . . . . . . 15
|
197 | 6, 188, 190 | absdifltd 14172 |
. . . . . . . . . . . . . . 15
|
198 | 196, 197 | mpbid 222 |
. . . . . . . . . . . . . 14
|
199 | 198 | simpld 475 |
. . . . . . . . . . . . 13
|
200 | 199 | adantr 481 |
. . . . . . . . . . . 12
|
201 | | eliooord 12233 |
. . . . . . . . . . . . . 14
|
202 | 201 | adantl 482 |
. . . . . . . . . . . . 13
|
203 | 202 | simpld 475 |
. . . . . . . . . . . 12
|
204 | 192, 193,
195, 200, 203 | lttrd 10198 |
. . . . . . . . . . 11
|
205 | 8 | adantr 481 |
. . . . . . . . . . . 12
|
206 | 188, 190 | readdcld 10069 |
. . . . . . . . . . . . 13
|
207 | 206 | adantr 481 |
. . . . . . . . . . . 12
|
208 | 202 | simprd 479 |
. . . . . . . . . . . 12
|
209 | | ftc1cnnclem.y2 |
. . . . . . . . . . . . . . 15
|
210 | 8, 188, 190 | absdifltd 14172 |
. . . . . . . . . . . . . . 15
|
211 | 209, 210 | mpbid 222 |
. . . . . . . . . . . . . 14
|
212 | 211 | simprd 479 |
. . . . . . . . . . . . 13
|
213 | 212 | adantr 481 |
. . . . . . . . . . . 12
|
214 | 195, 205,
207, 208, 213 | lttrd 10198 |
. . . . . . . . . . 11
|
215 | 188 | adantr 481 |
. . . . . . . . . . . 12
|
216 | 190 | adantr 481 |
. . . . . . . . . . . 12
|
217 | 195, 215,
216 | absdifltd 14172 |
. . . . . . . . . . 11
|
218 | 204, 214,
217 | mpbir2and 957 |
. . . . . . . . . 10
|
219 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
220 | 219 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
221 | 220 | breq1d 4663 |
. . . . . . . . . . . 12
|
222 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
223 | 222 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
224 | 223 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
225 | 224 | breq1d 4663 |
. . . . . . . . . . . 12
|
226 | 221, 225 | imbi12d 334 |
. . . . . . . . . . 11
|
227 | 226 | rspcv 3305 |
. . . . . . . . . 10
|
228 | 34, 187, 218, 227 | syl3c 66 |
. . . . . . . . 9
|
229 | | difrp 11868 |
. . . . . . . . . 10
|
230 | 140, 171,
229 | syl2anc 693 |
. . . . . . . . 9
|
231 | 228, 230 | mpbid 222 |
. . . . . . . 8
|
232 | 231 | adantlr 751 |
. . . . . . 7
|
233 | 180 | adantr 481 |
. . . . . . 7
|
234 | 170, 184,
232, 233 | itggt0cn 33482 |
. . . . . 6
|
235 | 171, 176,
140, 149, 182 | itgsubnc 33472 |
. . . . . . . 8
|
236 | 235 | adantr 481 |
. . . . . . 7
|
237 | | itgconst 23585 |
. . . . . . . . . . 11
|
238 | 44, 65, 173, 237 | syl3anc 1326 |
. . . . . . . . . 10
|
239 | 238 | adantr 481 |
. . . . . . . . 9
|
240 | 104 | oveq2d 6666 |
. . . . . . . . 9
|
241 | 173, 115 | mulcomd 10061 |
. . . . . . . . . 10
|
242 | 241 | adantr 481 |
. . . . . . . . 9
|
243 | 239, 240,
242 | 3eqtrd 2660 |
. . . . . . . 8
|
244 | 243 | oveq1d 6665 |
. . . . . . 7
|
245 | 236, 244 | eqtrd 2656 |
. . . . . 6
|
246 | 234, 245 | breqtrd 4679 |
. . . . 5
|
247 | 150, 154 | posdifd 10614 |
. . . . . 6
|
248 | 247 | biimpar 502 |
. . . . 5
|
249 | 246, 248 | syldan 487 |
. . . 4
|
250 | 139, 151,
155, 169, 249 | lelttrd 10195 |
. . 3
|
251 | 153 | adantr 481 |
. . . 4
|
252 | | ltdivmul 10898 |
. . . 4
|
253 | 139, 251,
131, 119, 252 | syl112anc 1330 |
. . 3
|
254 | 250, 253 | mpbird 247 |
. 2
|
255 | 138, 254 | eqbrtrd 4675 |
1
|