Proof of Theorem ftc1anclem7
Step | Hyp | Ref
| Expression |
1 | | i1ff 23443 |
. . . . . . . . . . 11
|
2 | 1 | ffvelrnda 6359 |
. . . . . . . . . 10
|
3 | 2 | recnd 10068 |
. . . . . . . . 9
|
4 | | ax-icn 9995 |
. . . . . . . . . 10
|
5 | | i1ff 23443 |
. . . . . . . . . . . 12
|
6 | 5 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
7 | 6 | recnd 10068 |
. . . . . . . . . 10
|
8 | | mulcl 10020 |
. . . . . . . . . 10
|
9 | 4, 7, 8 | sylancr 695 |
. . . . . . . . 9
|
10 | | addcl 10018 |
. . . . . . . . 9
|
11 | 3, 9, 10 | syl2an 494 |
. . . . . . . 8
|
12 | 11 | anandirs 874 |
. . . . . . 7
|
13 | | reex 10027 |
. . . . . . . . 9
|
14 | 13 | a1i 11 |
. . . . . . . 8
|
15 | 2 | adantlr 751 |
. . . . . . . 8
|
16 | | ovexd 6680 |
. . . . . . . 8
|
17 | 1 | feqmptd 6249 |
. . . . . . . . 9
|
18 | 17 | adantr 481 |
. . . . . . . 8
|
19 | 13 | a1i 11 |
. . . . . . . . . 10
|
20 | 4 | a1i 11 |
. . . . . . . . . 10
|
21 | | fconstmpt 5163 |
. . . . . . . . . . 11
|
22 | 21 | a1i 11 |
. . . . . . . . . 10
|
23 | 5 | feqmptd 6249 |
. . . . . . . . . 10
|
24 | 19, 20, 6, 22, 23 | offval2 6914 |
. . . . . . . . 9
|
25 | 24 | adantl 482 |
. . . . . . . 8
|
26 | 14, 15, 16, 18, 25 | offval2 6914 |
. . . . . . 7
|
27 | | absf 14077 |
. . . . . . . . 9
|
28 | 27 | a1i 11 |
. . . . . . . 8
|
29 | 28 | feqmptd 6249 |
. . . . . . 7
|
30 | | fveq2 6191 |
. . . . . . 7
|
31 | 12, 26, 29, 30 | fmptco 6396 |
. . . . . 6
|
32 | | ftc1anclem3 33487 |
. . . . . 6
|
33 | 31, 32 | eqeltrrd 2702 |
. . . . 5
|
34 | | ioombl 23333 |
. . . . 5
|
35 | | fveq2 6191 |
. . . . . . . . . . . 12
|
36 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . 12
|
38 | 35, 37 | oveq12d 6668 |
. . . . . . . . . . 11
|
39 | 38 | fveq2d 6195 |
. . . . . . . . . 10
|
40 | | eqid 2622 |
. . . . . . . . . 10
|
41 | | fvex 6201 |
. . . . . . . . . 10
|
42 | 39, 40, 41 | fvmpt 6282 |
. . . . . . . . 9
|
43 | 42 | eqcomd 2628 |
. . . . . . . 8
|
44 | 43 | ifeq1d 4104 |
. . . . . . 7
|
45 | 44 | mpteq2ia 4740 |
. . . . . 6
|
46 | 45 | i1fres 23472 |
. . . . 5
|
47 | 33, 34, 46 | sylancl 694 |
. . . 4
|
48 | | breq2 4657 |
. . . . . . 7
|
49 | | breq2 4657 |
. . . . . . 7
|
50 | | elioore 12205 |
. . . . . . . 8
|
51 | | eleq1 2689 |
. . . . . . . . . . . 12
|
52 | 51 | anbi2d 740 |
. . . . . . . . . . 11
|
53 | 38 | eleq1d 2686 |
. . . . . . . . . . 11
|
54 | 52, 53 | imbi12d 334 |
. . . . . . . . . 10
|
55 | 54, 12 | chvarv 2263 |
. . . . . . . . 9
|
56 | 55 | absge0d 14183 |
. . . . . . . 8
|
57 | 50, 56 | sylan2 491 |
. . . . . . 7
|
58 | | 0le0 11110 |
. . . . . . . 8
|
59 | 58 | a1i 11 |
. . . . . . 7
|
60 | 48, 49, 57, 59 | ifbothda 4123 |
. . . . . 6
|
61 | 60 | ralrimivw 2967 |
. . . . 5
|
62 | | ax-resscn 9993 |
. . . . . . . 8
|
63 | 62 | a1i 11 |
. . . . . . 7
|
64 | | c0ex 10034 |
. . . . . . . . . 10
|
65 | 41, 64 | ifex 4156 |
. . . . . . . . 9
|
66 | | eqid 2622 |
. . . . . . . . 9
|
67 | 65, 66 | fnmpti 6022 |
. . . . . . . 8
|
68 | 67 | a1i 11 |
. . . . . . 7
|
69 | 63, 68 | 0pledm 23440 |
. . . . . 6
|
70 | 64 | a1i 11 |
. . . . . . 7
|
71 | 65 | a1i 11 |
. . . . . . 7
|
72 | | fconstmpt 5163 |
. . . . . . . 8
|
73 | 72 | a1i 11 |
. . . . . . 7
|
74 | | eqidd 2623 |
. . . . . . 7
|
75 | 14, 70, 71, 73, 74 | ofrfval2 6915 |
. . . . . 6
|
76 | 69, 75 | bitrd 268 |
. . . . 5
|
77 | 61, 76 | mpbird 247 |
. . . 4
|
78 | | itg2itg1 23503 |
. . . . 5
|
79 | | itg1cl 23452 |
. . . . . 6
|
80 | 79 | adantr 481 |
. . . . 5
|
81 | 78, 80 | eqeltrd 2701 |
. . . 4
|
82 | 47, 77, 81 | syl2anc 693 |
. . 3
|
83 | 82 | ad6antlr 773 |
. 2
|
84 | | simplll 798 |
. . . . 5
|
85 | | ftc1anc.a |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 85 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
87 | | ftc1anc.b |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 87 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 86, 88 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
90 | | df-icc 12182 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | 90 | elixx3g 12188 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 91 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 92 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 90 | elixx3g 12188 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 94 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 95 | simprd 479 |
. . . . . . . . . . . . . . . . . . 19
|
97 | 93, 96 | anim12i 590 |
. . . . . . . . . . . . . . . . . 18
|
98 | | ioossioo 12265 |
. . . . . . . . . . . . . . . . . 18
|
99 | 89, 97, 98 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
100 | | ftc1anc.s |
. . . . . . . . . . . . . . . . . 18
|
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
102 | 99, 101 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
103 | 102 | 3adantr3 1222 |
. . . . . . . . . . . . . . 15
|
104 | 103 | sselda 3603 |
. . . . . . . . . . . . . 14
|
105 | | ftc1anc.f |
. . . . . . . . . . . . . . . 16
|
106 | 105 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
107 | 106 | adantlr 751 |
. . . . . . . . . . . . . 14
|
108 | 104, 107 | syldan 487 |
. . . . . . . . . . . . 13
|
109 | 108 | adantllr 755 |
. . . . . . . . . . . 12
|
110 | 55 | adantll 750 |
. . . . . . . . . . . . . 14
|
111 | 50, 110 | sylan2 491 |
. . . . . . . . . . . . 13
|
112 | 111 | adantlr 751 |
. . . . . . . . . . . 12
|
113 | 109, 112 | subcld 10392 |
. . . . . . . . . . 11
|
114 | 113 | abscld 14175 |
. . . . . . . . . 10
|
115 | 114 | rexrd 10089 |
. . . . . . . . 9
|
116 | 113 | absge0d 14183 |
. . . . . . . . 9
|
117 | | elxrge0 12281 |
. . . . . . . . 9
|
118 | 115, 116,
117 | sylanbrc 698 |
. . . . . . . 8
|
119 | | 0e0iccpnf 12283 |
. . . . . . . . 9
|
120 | 119 | a1i 11 |
. . . . . . . 8
|
121 | 118, 120 | ifclda 4120 |
. . . . . . 7
|
122 | 121 | adantr 481 |
. . . . . 6
|
123 | | eqid 2622 |
. . . . . 6
|
124 | 122, 123 | fmptd 6385 |
. . . . 5
|
125 | 84, 124 | sylan 488 |
. . . 4
|
126 | | rpre 11839 |
. . . . . 6
|
127 | 126 | rehalfcld 11279 |
. . . . 5
|
128 | 127 | ad2antlr 763 |
. . . 4
|
129 | | simpll 790 |
. . . . . . . . 9
|
130 | 102 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
131 | 130 | adantllr 755 |
. . . . . . . . . . . . . . 15
|
132 | 106 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
133 | | ftc1anc.d |
. . . . . . . . . . . . . . . . . . . . . 22
|
134 | 133 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . 21
|
135 | 134 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
136 | 135, 110 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
|
137 | 132, 136 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
|
138 | 137 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
139 | 138 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
|
140 | 139 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
141 | 131, 140 | syldan 487 |
. . . . . . . . . . . . . 14
|
142 | 137 | absge0d 14183 |
. . . . . . . . . . . . . . . 16
|
143 | 142 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
144 | 131, 143 | syldan 487 |
. . . . . . . . . . . . . 14
|
145 | 141, 144,
117 | sylanbrc 698 |
. . . . . . . . . . . . 13
|
146 | 119 | a1i 11 |
. . . . . . . . . . . . 13
|
147 | 145, 146 | ifclda 4120 |
. . . . . . . . . . . 12
|
148 | 147 | adantr 481 |
. . . . . . . . . . 11
|
149 | 148, 123 | fmptd 6385 |
. . . . . . . . . 10
|
150 | | itg2cl 23499 |
. . . . . . . . . 10
|
151 | 149, 150 | syl 17 |
. . . . . . . . 9
|
152 | 129, 151 | sylan 488 |
. . . . . . . 8
|
153 | | 0cnd 10033 |
. . . . . . . . . . . . . . . . 17
|
154 | 106, 153 | ifclda 4120 |
. . . . . . . . . . . . . . . 16
|
155 | | subcl 10280 |
. . . . . . . . . . . . . . . 16
|
156 | 154, 55, 155 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
157 | 156 | anassrs 680 |
. . . . . . . . . . . . . 14
|
158 | 157 | abscld 14175 |
. . . . . . . . . . . . 13
|
159 | 158 | rexrd 10089 |
. . . . . . . . . . . 12
|
160 | 157 | absge0d 14183 |
. . . . . . . . . . . 12
|
161 | | elxrge0 12281 |
. . . . . . . . . . . 12
|
162 | 159, 160,
161 | sylanbrc 698 |
. . . . . . . . . . 11
|
163 | | eqid 2622 |
. . . . . . . . . . 11
|
164 | 162, 163 | fmptd 6385 |
. . . . . . . . . 10
|
165 | | itg2cl 23499 |
. . . . . . . . . 10
|
166 | 164, 165 | syl 17 |
. . . . . . . . 9
|
167 | 166 | ad3antrrr 766 |
. . . . . . . 8
|
168 | | rphalfcl 11858 |
. . . . . . . . . 10
|
169 | 168 | rpxrd 11873 |
. . . . . . . . 9
|
170 | 169 | ad2antlr 763 |
. . . . . . . 8
|
171 | 164 | adantr 481 |
. . . . . . . . . 10
|
172 | | breq1 4656 |
. . . . . . . . . . . . 13
|
173 | | breq1 4656 |
. . . . . . . . . . . . 13
|
174 | 138 | leidd 10594 |
. . . . . . . . . . . . . . . . 17
|
175 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . 20
|
176 | 175 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
177 | 176 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
178 | 177 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
179 | 174, 178 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
|
180 | 179 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
181 | 131, 180 | syldan 487 |
. . . . . . . . . . . . . 14
|
182 | 181 | adantlr 751 |
. . . . . . . . . . . . 13
|
183 | 160 | adantlr 751 |
. . . . . . . . . . . . . 14
|
184 | 183 | adantr 481 |
. . . . . . . . . . . . 13
|
185 | 172, 173,
182, 184 | ifbothda 4123 |
. . . . . . . . . . . 12
|
186 | 185 | ralrimiva 2966 |
. . . . . . . . . . 11
|
187 | 13 | a1i 11 |
. . . . . . . . . . . . 13
|
188 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
189 | 188, 64 | ifex 4156 |
. . . . . . . . . . . . . 14
|
190 | 189 | a1i 11 |
. . . . . . . . . . . . 13
|
191 | | fvexd 6203 |
. . . . . . . . . . . . 13
|
192 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
193 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
194 | 187, 190,
191, 192, 193 | ofrfval2 6915 |
. . . . . . . . . . . 12
|
195 | 194 | ad2antrr 762 |
. . . . . . . . . . 11
|
196 | 186, 195 | mpbird 247 |
. . . . . . . . . 10
|
197 | | itg2le 23506 |
. . . . . . . . . 10
|
198 | 149, 171,
196, 197 | syl3anc 1326 |
. . . . . . . . 9
|
199 | 129, 198 | sylan 488 |
. . . . . . . 8
|
200 | | simpllr 799 |
. . . . . . . 8
|
201 | 152, 167,
170, 199, 200 | xrlelttrd 11991 |
. . . . . . 7
|
202 | | xrltle 11982 |
. . . . . . . 8
|
203 | 152, 170,
202 | syl2anc 693 |
. . . . . . 7
|
204 | 201, 203 | mpd 15 |
. . . . . 6
|
205 | 204 | adantllr 755 |
. . . . 5
|
206 | 205 | 3adantr3 1222 |
. . . 4
|
207 | | itg2lecl 23505 |
. . . 4
|
208 | 125, 128,
206, 207 | syl3anc 1326 |
. . 3
|
209 | 208 | adantr 481 |
. 2
|
210 | 127 | ad3antlr 767 |
. 2
|
211 | 82 | adantr 481 |
. . . . . . . 8
|
212 | | 2rp 11837 |
. . . . . . . . 9
|
213 | | imassrn 5477 |
. . . . . . . . . . . . . . . 16
|
214 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
215 | 27, 214 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
216 | 213, 215 | sstri 3612 |
. . . . . . . . . . . . . . 15
|
217 | 216 | a1i 11 |
. . . . . . . . . . . . . 14
|
218 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 1, 218 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
220 | 219 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
221 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . 20
|
222 | 5, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
223 | 222 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
224 | 220, 223 | unssd 3789 |
. . . . . . . . . . . . . . . . 17
|
225 | 224, 62 | syl6ss 3615 |
. . . . . . . . . . . . . . . 16
|
226 | | i1f0rn 23449 |
. . . . . . . . . . . . . . . . . 18
|
227 | | elun1 3780 |
. . . . . . . . . . . . . . . . . 18
|
228 | 226, 227 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
229 | 228 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
230 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
|
231 | 27, 230 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
232 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . 17
|
233 | 231, 232 | mp3an1 1411 |
. . . . . . . . . . . . . . . 16
|
234 | 225, 229,
233 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
235 | | ne0i 3921 |
. . . . . . . . . . . . . . 15
|
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . 14
|
237 | | ffun 6048 |
. . . . . . . . . . . . . . . . 17
|
238 | 27, 237 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
239 | | i1frn 23444 |
. . . . . . . . . . . . . . . . 17
|
240 | | i1frn 23444 |
. . . . . . . . . . . . . . . . 17
|
241 | | unfi 8227 |
. . . . . . . . . . . . . . . . 17
|
242 | 239, 240,
241 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
243 | | imafi 8259 |
. . . . . . . . . . . . . . . 16
|
244 | 238, 242,
243 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
245 | | fimaxre2 10969 |
. . . . . . . . . . . . . . 15
|
246 | 216, 244,
245 | sylancr 695 |
. . . . . . . . . . . . . 14
|
247 | | suprcl 10983 |
. . . . . . . . . . . . . 14
|
248 | 217, 236,
246, 247 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
249 | 248 | adantr 481 |
. . . . . . . . . . . 12
|
250 | | 0red 10041 |
. . . . . . . . . . . . 13
|
251 | 225 | sselda 3603 |
. . . . . . . . . . . . . . 15
|
252 | 251 | abscld 14175 |
. . . . . . . . . . . . . 14
|
253 | 252 | adantrr 753 |
. . . . . . . . . . . . 13
|
254 | | absgt0 14064 |
. . . . . . . . . . . . . . . 16
|
255 | 251, 254 | syl 17 |
. . . . . . . . . . . . . . 15
|
256 | 255 | biimpa 501 |
. . . . . . . . . . . . . 14
|
257 | 256 | anasss 679 |
. . . . . . . . . . . . 13
|
258 | 217, 236,
246 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
|
259 | 258 | adantr 481 |
. . . . . . . . . . . . . . 15
|
260 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . 17
|
261 | 231, 260 | mp3an1 1411 |
. . . . . . . . . . . . . . . 16
|
262 | 225, 261 | sylan 488 |
. . . . . . . . . . . . . . 15
|
263 | | suprub 10984 |
. . . . . . . . . . . . . . 15
|
264 | 259, 262,
263 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
265 | 264 | adantrr 753 |
. . . . . . . . . . . . 13
|
266 | 250, 253,
249, 257, 265 | ltletrd 10197 |
. . . . . . . . . . . 12
|
267 | 249, 266 | elrpd 11869 |
. . . . . . . . . . 11
|
268 | 267 | rexlimdvaa 3032 |
. . . . . . . . . 10
|
269 | 268 | imp 445 |
. . . . . . . . 9
|
270 | | rpmulcl 11855 |
. . . . . . . . 9
|
271 | 212, 269,
270 | sylancr 695 |
. . . . . . . 8
|
272 | 211, 271 | rerpdivcld 11903 |
. . . . . . 7
|
273 | 272 | adantll 750 |
. . . . . 6
|
274 | 273 | adantlr 751 |
. . . . 5
|
275 | 274 | ad3antrrr 766 |
. . . 4
|
276 | | simp-4l 806 |
. . . . . 6
|
277 | | iccssre 12255 |
. . . . . . . . . . . . 13
|
278 | 85, 87, 277 | syl2anc 693 |
. . . . . . . . . . . 12
|
279 | 278, 62 | syl6ss 3615 |
. . . . . . . . . . 11
|
280 | 279 | sselda 3603 |
. . . . . . . . . 10
|
281 | 279 | sselda 3603 |
. . . . . . . . . 10
|
282 | | subcl 10280 |
. . . . . . . . . 10
|
283 | 280, 281,
282 | syl2anr 495 |
. . . . . . . . 9
|
284 | 283 | anandis 873 |
. . . . . . . 8
|
285 | 284 | abscld 14175 |
. . . . . . 7
|
286 | 285 | 3adantr3 1222 |
. . . . . 6
|
287 | 276, 286 | sylan 488 |
. . . . 5
|
288 | 287 | adantr 481 |
. . . 4
|
289 | | rpdivcl 11856 |
. . . . . . . . 9
|
290 | 168, 271,
289 | syl2anr 495 |
. . . . . . . 8
|
291 | 290 | rpred 11872 |
. . . . . . 7
|
292 | 291 | adantlll 754 |
. . . . . 6
|
293 | 292 | adantllr 755 |
. . . . 5
|
294 | 293 | ad2antrr 762 |
. . . 4
|
295 | 278 | sseld 3602 |
. . . . . . . . . . 11
|
296 | 278 | sseld 3602 |
. . . . . . . . . . 11
|
297 | | idd 24 |
. . . . . . . . . . 11
|
298 | 295, 296,
297 | 3anim123d 1406 |
. . . . . . . . . 10
|
299 | 298 | ad2antrr 762 |
. . . . . . . . 9
|
300 | 299 | imp 445 |
. . . . . . . 8
|
301 | 55 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
302 | 301 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
303 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . 18
|
304 | 302, 56, 303 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
305 | | ifcl 4130 |
. . . . . . . . . . . . . . . . 17
|
306 | 304, 119,
305 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
307 | 306, 66 | fmptd 6385 |
. . . . . . . . . . . . . . 15
|
308 | 248 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
309 | 308 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . . 19
|
310 | 248, 248 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . 21
|
311 | 310 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
312 | | abs0 14025 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
313 | 312, 234 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . . . . . . 22
|
314 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . 22
|
315 | 258, 313,
314 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
316 | 248, 248,
315, 315 | addge0d 10603 |
. . . . . . . . . . . . . . . . . . . 20
|
317 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . . . 20
|
318 | 311, 316,
317 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . 19
|
319 | 309, 318 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
320 | | ifcl 4130 |
. . . . . . . . . . . . . . . . . 18
|
321 | 319, 119,
320 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
322 | 321 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
323 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
324 | 322, 323 | fmptd 6385 |
. . . . . . . . . . . . . . 15
|
325 | 1 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
326 | 325 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
327 | 326 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
328 | 5 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
329 | 328 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
330 | 329 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
331 | | readdcl 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
332 | 327, 330,
331 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
333 | 332 | anandirs 874 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
334 | 310 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
335 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
336 | 4, 329, 335 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
337 | | abstri 14070 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
338 | 326, 336,
337 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
339 | 338 | anandirs 874 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
340 | | absmul 14034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
341 | 4, 329, 340 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
342 | | absi 14026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
343 | 342 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
344 | 341, 343 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
345 | 330 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
346 | 345 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
347 | 344, 346 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
348 | 347 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
349 | 348 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
350 | 339, 349 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
351 | 327 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
352 | 330 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
353 | 248 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
354 | 258 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
355 | 225 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
356 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
357 | 1, 356 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
358 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
359 | 357, 358 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
360 | | elun1 3780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
361 | 359, 360 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
362 | 361 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
363 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
364 | 231, 363 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
365 | 355, 362,
364 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
366 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
367 | 354, 365,
366 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
368 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
369 | 5, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
370 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
371 | 369, 370 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
372 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
373 | 371, 372 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
374 | 373 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
375 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
376 | 231, 375 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
377 | 355, 374,
376 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
378 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
379 | 354, 377,
378 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
380 | 351, 352,
353, 353, 367, 379 | le2addd 10646 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
381 | 301, 333,
334, 350, 380 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
382 | 309 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
383 | 381, 382 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . 21
|
384 | 50, 383 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
|
385 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . 21
|
386 | 385 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
387 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . 21
|
388 | 387 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
389 | 384, 386,
388 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . . . 19
|
390 | 389 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
391 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
392 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . 19
|
393 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . 19
|
394 | 391, 392,
393 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . . 18
|
395 | 390, 394 | pm2.61d1 171 |
. . . . . . . . . . . . . . . . 17
|
396 | 395 | ralrimivw 2967 |
. . . . . . . . . . . . . . . 16
|
397 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
|
398 | 397, 64 | ifex 4156 |
. . . . . . . . . . . . . . . . . 18
|
399 | 398 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
400 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
401 | 14, 71, 399, 74, 400 | ofrfval2 6915 |
. . . . . . . . . . . . . . . 16
|
402 | 396, 401 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
403 | | itg2le 23506 |
. . . . . . . . . . . . . . 15
|
404 | 307, 324,
402, 403 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
405 | 404 | adantr 481 |
. . . . . . . . . . . . 13
|
406 | | mblvol 23298 |
. . . . . . . . . . . . . . . . 17
|
407 | 34, 406 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
408 | | ovolioo 23336 |
. . . . . . . . . . . . . . . 16
|
409 | 407, 408 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
|
410 | | resubcl 10345 |
. . . . . . . . . . . . . . . . 17
|
411 | 410 | ancoms 469 |
. . . . . . . . . . . . . . . 16
|
412 | 411 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
413 | 409, 412 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
414 | | elrege0 12278 |
. . . . . . . . . . . . . . . . 17
|
415 | 248, 315,
414 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
|
416 | | ge0addcl 12284 |
. . . . . . . . . . . . . . . 16
|
417 | 415, 415,
416 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
418 | 309, 417 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
419 | | itg2const 23507 |
. . . . . . . . . . . . . . 15
|
420 | 34, 419 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
421 | 413, 418,
420 | syl2anr 495 |
. . . . . . . . . . . . 13
|
422 | 405, 421 | breqtrd 4679 |
. . . . . . . . . . . 12
|
423 | 422 | adantll 750 |
. . . . . . . . . . 11
|
424 | 423 | adantlr 751 |
. . . . . . . . . 10
|
425 | 82 | ad3antlr 767 |
. . . . . . . . . . 11
|
426 | 413 | adantl 482 |
. . . . . . . . . . 11
|
427 | 271 | adantll 750 |
. . . . . . . . . . . 12
|
428 | 427 | adantr 481 |
. . . . . . . . . . 11
|
429 | 425, 426,
428 | ledivmuld 11925 |
. . . . . . . . . 10
|
430 | 424, 429 | mpbird 247 |
. . . . . . . . 9
|
431 | | abssubge0 14067 |
. . . . . . . . . . . 12
|
432 | 408, 431 | eqtr4d 2659 |
. . . . . . . . . . 11
|
433 | 407, 432 | syl5eq 2668 |
. . . . . . . . . 10
|
434 | 433 | adantl 482 |
. . . . . . . . 9
|
435 | 430, 434 | breqtrd 4679 |
. . . . . . . 8
|
436 | 300, 435 | syldan 487 |
. . . . . . 7
|
437 | 436 | adantllr 755 |
. . . . . 6
|
438 | 437 | adantlr 751 |
. . . . 5
|
439 | 438 | adantr 481 |
. . . 4
|
440 | | simpr 477 |
. . . 4
|
441 | 275, 288,
294, 439, 440 | lelttrd 10195 |
. . 3
|
442 | 82 | adantl 482 |
. . . . . 6
|
443 | 442 | ad3antrrr 766 |
. . . . 5
|
444 | 127 | adantl 482 |
. . . . 5
|
445 | 427 | adantlr 751 |
. . . . . 6
|
446 | 445 | adantr 481 |
. . . . 5
|
447 | 443, 444,
446 | ltdiv1d 11917 |
. . . 4
|
448 | 447 | ad2antrr 762 |
. . 3
|
449 | 441, 448 | mpbird 247 |
. 2
|
450 | 201 | adantllr 755 |
. . . 4
|
451 | 450 | 3adantr3 1222 |
. . 3
|
452 | 451 | adantr 481 |
. 2
|
453 | 83, 209, 210, 210, 449, 452 | lt2addd 10650 |
1
|