Step | Hyp | Ref
| Expression |
1 | | itg2addnc.f2 |
. . . . . . . . . . 11
|
2 | | rge0ssre 12280 |
. . . . . . . . . . 11
|
3 | | fss 6056 |
. . . . . . . . . . 11
|
4 | 1, 2, 3 | sylancl 694 |
. . . . . . . . . 10
|
5 | 4 | ad2antrr 762 |
. . . . . . . . 9
|
6 | 5 | ffvelrnda 6359 |
. . . . . . . 8
|
7 | | rpre 11839 |
. . . . . . . . . 10
|
8 | | 3re 11094 |
. . . . . . . . . . 11
|
9 | | 3ne0 11115 |
. . . . . . . . . . 11
|
10 | 8, 9 | pm3.2i 471 |
. . . . . . . . . 10
|
11 | | redivcl 10744 |
. . . . . . . . . . 11
|
12 | 11 | 3expb 1266 |
. . . . . . . . . 10
|
13 | 7, 10, 12 | sylancl 694 |
. . . . . . . . 9
|
14 | 13 | ad2antlr 763 |
. . . . . . . 8
|
15 | | rpcnne0 11850 |
. . . . . . . . . 10
|
16 | | 3cn 11095 |
. . . . . . . . . . 11
|
17 | 16, 9 | pm3.2i 471 |
. . . . . . . . . 10
|
18 | | divne0 10697 |
. . . . . . . . . 10
|
19 | 15, 17, 18 | sylancl 694 |
. . . . . . . . 9
|
20 | 19 | ad2antlr 763 |
. . . . . . . 8
|
21 | 6, 14, 20 | redivcld 10853 |
. . . . . . 7
|
22 | | reflcl 12597 |
. . . . . . 7
|
23 | 21, 22 | syl 17 |
. . . . . 6
|
24 | | peano2rem 10348 |
. . . . . 6
|
25 | 23, 24 | syl 17 |
. . . . 5
|
26 | 25, 14 | remulcld 10070 |
. . . 4
|
27 | | i1ff 23443 |
. . . . . 6
|
28 | 27 | ad2antlr 763 |
. . . . 5
|
29 | 28 | ffvelrnda 6359 |
. . . 4
|
30 | 26, 29 | ifcld 4131 |
. . 3
|
31 | | eqid 2622 |
. . 3
|
32 | 30, 31 | fmptd 6385 |
. 2
|
33 | | fzfi 12771 |
. . . . 5
|
34 | | ovex 6678 |
. . . . . . 7
|
35 | | eqid 2622 |
. . . . . . 7
|
36 | 34, 35 | fnmpti 6022 |
. . . . . 6
|
37 | | dffn4 6121 |
. . . . . 6
|
38 | 36, 37 | mpbi 220 |
. . . . 5
|
39 | | fofi 8252 |
. . . . 5
|
40 | 33, 38, 39 | mp2an 708 |
. . . 4
|
41 | | i1frn 23444 |
. . . . 5
|
42 | 41 | ad2antlr 763 |
. . . 4
|
43 | | unfi 8227 |
. . . 4
|
44 | 40, 42, 43 | sylancr 695 |
. . 3
|
45 | | 3nn 11186 |
. . . . . . . . . . . . . . . . 17
|
46 | | nnrp 11842 |
. . . . . . . . . . . . . . . . 17
|
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
48 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . 16
|
49 | 47, 48 | mpan2 707 |
. . . . . . . . . . . . . . 15
|
50 | 49 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
51 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
53 | | elrege0 12278 |
. . . . . . . . . . . . . . . 16
|
54 | 52, 53 | sylib 208 |
. . . . . . . . . . . . . . 15
|
55 | 54 | simprd 479 |
. . . . . . . . . . . . . 14
|
56 | 6, 50, 55 | divge0d 11912 |
. . . . . . . . . . . . 13
|
57 | | flge0nn0 12621 |
. . . . . . . . . . . . 13
|
58 | 21, 56, 57 | syl2anc 693 |
. . . . . . . . . . . 12
|
59 | 58 | nn0ge0d 11354 |
. . . . . . . . . . 11
|
60 | 59 | adantr 481 |
. . . . . . . . . 10
|
61 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
62 | 27, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
|
63 | | i1f0rn 23449 |
. . . . . . . . . . . . . . . . . 18
|
64 | | elex2 3216 |
. . . . . . . . . . . . . . . . . 18
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
66 | | n0 3931 |
. . . . . . . . . . . . . . . . 17
|
67 | 65, 66 | sylibr 224 |
. . . . . . . . . . . . . . . 16
|
68 | | fimaxre2 10969 |
. . . . . . . . . . . . . . . . 17
|
69 | 62, 41, 68 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
70 | 62, 67, 69 | 3jca 1242 |
. . . . . . . . . . . . . . 15
|
71 | 70 | ad3antlr 767 |
. . . . . . . . . . . . . 14
|
72 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
|
73 | 27, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
74 | | dffn3 6054 |
. . . . . . . . . . . . . . . . 17
|
75 | 73, 74 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
77 | 76 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
|
78 | | suprub 10984 |
. . . . . . . . . . . . . 14
|
79 | 71, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . 13
|
80 | | suprcl 10983 |
. . . . . . . . . . . . . . . . 17
|
81 | 62, 67, 69, 80 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
83 | | letr 10131 |
. . . . . . . . . . . . . . 15
|
84 | 26, 29, 82, 83 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
85 | 25, 82, 50 | lemuldivd 11921 |
. . . . . . . . . . . . . . . 16
|
86 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
87 | 82, 14, 20 | redivcld 10853 |
. . . . . . . . . . . . . . . . 17
|
88 | 23, 86, 87 | lesubaddd 10624 |
. . . . . . . . . . . . . . . 16
|
89 | 85, 88 | bitrd 268 |
. . . . . . . . . . . . . . 15
|
90 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . 18
|
91 | 87, 90 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
92 | | ceige 12644 |
. . . . . . . . . . . . . . . . 17
|
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
|
94 | | ceicl 12642 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 91, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
96 | 95 | zred 11482 |
. . . . . . . . . . . . . . . . 17
|
97 | | letr 10131 |
. . . . . . . . . . . . . . . . 17
|
98 | 23, 91, 96, 97 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
99 | 93, 98 | mpan2d 710 |
. . . . . . . . . . . . . . 15
|
100 | 89, 99 | sylbid 230 |
. . . . . . . . . . . . . 14
|
101 | 84, 100 | syld 47 |
. . . . . . . . . . . . 13
|
102 | 79, 101 | mpan2d 710 |
. . . . . . . . . . . 12
|
103 | 102 | adantrd 484 |
. . . . . . . . . . 11
|
104 | 103 | imp 445 |
. . . . . . . . . 10
|
105 | 21 | flcld 12599 |
. . . . . . . . . . . 12
|
106 | 105 | adantr 481 |
. . . . . . . . . . 11
|
107 | | 0zd 11389 |
. . . . . . . . . . 11
|
108 | 95 | adantr 481 |
. . . . . . . . . . 11
|
109 | | elfz 12332 |
. . . . . . . . . . 11
|
110 | 106, 107,
108, 109 | syl3anc 1326 |
. . . . . . . . . 10
|
111 | 60, 104, 110 | mpbir2and 957 |
. . . . . . . . 9
|
112 | | eqid 2622 |
. . . . . . . . 9
|
113 | | oveq1 6657 |
. . . . . . . . . . . 12
|
114 | 113 | oveq1d 6665 |
. . . . . . . . . . 11
|
115 | 114 | eqeq2d 2632 |
. . . . . . . . . 10
|
116 | 115 | rspcev 3309 |
. . . . . . . . 9
|
117 | 111, 112,
116 | sylancl 694 |
. . . . . . . 8
|
118 | | ovex 6678 |
. . . . . . . . 9
|
119 | 35 | elrnmpt 5372 |
. . . . . . . . 9
|
120 | 118, 119 | ax-mp 5 |
. . . . . . . 8
|
121 | 117, 120 | sylibr 224 |
. . . . . . 7
|
122 | | elun1 3780 |
. . . . . . 7
|
123 | 121, 122 | syl 17 |
. . . . . 6
|
124 | | elun2 3781 |
. . . . . . . 8
|
125 | 77, 124 | syl 17 |
. . . . . . 7
|
126 | 125 | adantr 481 |
. . . . . 6
|
127 | 123, 126 | ifclda 4120 |
. . . . 5
|
128 | 127, 31 | fmptd 6385 |
. . . 4
|
129 | | frn 6053 |
. . . 4
|
130 | 128, 129 | syl 17 |
. . 3
|
131 | | ssfi 8180 |
. . 3
|
132 | 44, 130, 131 | syl2anc 693 |
. 2
|
133 | 31 | mptpreima 5628 |
. . . 4
|
134 | | unrab 3898 |
. . . . 5
|
135 | | inrab 3899 |
. . . . . . . 8
|
136 | 135 | ineq1i 3810 |
. . . . . . 7
|
137 | | inrab 3899 |
. . . . . . 7
|
138 | 136, 137 | eqtri 2644 |
. . . . . 6
|
139 | | unrab 3898 |
. . . . . . . 8
|
140 | 139 | ineq1i 3810 |
. . . . . . 7
|
141 | | inrab 3899 |
. . . . . . 7
|
142 | 140, 141 | eqtri 2644 |
. . . . . 6
|
143 | 138, 142 | uneq12i 3765 |
. . . . 5
|
144 | | eqcom 2629 |
. . . . . . . 8
|
145 | | fvex 6201 |
. . . . . . . . . 10
|
146 | 118, 145 | ifex 4156 |
. . . . . . . . 9
|
147 | 146 | elsn 4192 |
. . . . . . . 8
|
148 | | ianor 509 |
. . . . . . . . . . . 12
|
149 | | nne 2798 |
. . . . . . . . . . . . 13
|
150 | 149 | orbi2i 541 |
. . . . . . . . . . . 12
|
151 | 148, 150 | bitr2i 265 |
. . . . . . . . . . 11
|
152 | 151 | anbi1i 731 |
. . . . . . . . . 10
|
153 | 152 | orbi2i 541 |
. . . . . . . . 9
|
154 | | eqif 4126 |
. . . . . . . . 9
|
155 | 153, 154 | bitr4i 267 |
. . . . . . . 8
|
156 | 144, 147,
155 | 3bitr4i 292 |
. . . . . . 7
|
157 | 156 | a1i 11 |
. . . . . 6
|
158 | 157 | rabbiia 3185 |
. . . . 5
|
159 | 134, 143,
158 | 3eqtr4ri 2655 |
. . . 4
|
160 | 133, 159 | eqtri 2644 |
. . 3
|
161 | | eldifi 3732 |
. . . . . 6
|
162 | | frn 6053 |
. . . . . . . 8
|
163 | 32, 162 | syl 17 |
. . . . . . 7
|
164 | 163 | sseld 3602 |
. . . . . 6
|
165 | 161, 164 | syl5 34 |
. . . . 5
|
166 | 165 | imdistani 726 |
. . . 4
|
167 | | rabiun 33382 |
. . . . . . . . . 10
|
168 | | cnvimarndm 5486 |
. . . . . . . . . . . . . 14
|
169 | | iunid 4575 |
. . . . . . . . . . . . . . . 16
|
170 | 169 | imaeq2i 5464 |
. . . . . . . . . . . . . . 15
|
171 | | imaiun 6503 |
. . . . . . . . . . . . . . 15
|
172 | 170, 171 | eqtr3i 2646 |
. . . . . . . . . . . . . 14
|
173 | 168, 172 | eqtr3i 2646 |
. . . . . . . . . . . . 13
|
174 | | fdm 6051 |
. . . . . . . . . . . . . 14
|
175 | 27, 174 | syl 17 |
. . . . . . . . . . . . 13
|
176 | 173, 175 | syl5eqr 2670 |
. . . . . . . . . . . 12
|
177 | 176 | ad2antlr 763 |
. . . . . . . . . . 11
|
178 | | rabeq 3192 |
. . . . . . . . . . 11
|
179 | 177, 178 | syl 17 |
. . . . . . . . . 10
|
180 | 167, 179 | syl5eqr 2670 |
. . . . . . . . 9
|
181 | | fniniseg 6338 |
. . . . . . . . . . . . . . . . . 18
|
182 | 27, 72, 181 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
183 | 182 | simplbda 654 |
. . . . . . . . . . . . . . . 16
|
184 | 183 | breq2d 4665 |
. . . . . . . . . . . . . . 15
|
185 | 184 | rabbidva 3188 |
. . . . . . . . . . . . . 14
|
186 | | inrab2 3900 |
. . . . . . . . . . . . . . 15
|
187 | | imassrn 5477 |
. . . . . . . . . . . . . . . . . 18
|
188 | | dfdm4 5316 |
. . . . . . . . . . . . . . . . . . 19
|
189 | 188, 175 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . 18
|
190 | 187, 189 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . 17
|
191 | | sseqin2 3817 |
. . . . . . . . . . . . . . . . 17
|
192 | 190, 191 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
193 | | rabeq 3192 |
. . . . . . . . . . . . . . . 16
|
194 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . 15
|
195 | 186, 194 | syl5eq 2668 |
. . . . . . . . . . . . . 14
|
196 | 185, 195 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
197 | 196 | ad3antlr 767 |
. . . . . . . . . . . 12
|
198 | 25 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
199 | 62 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
200 | 199 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
|
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
202 | 49 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . 18
|
203 | 198, 201,
202 | lemuldivd 11921 |
. . . . . . . . . . . . . . . . 17
|
204 | 23 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
205 | | 1red 10055 |
. . . . . . . . . . . . . . . . . 18
|
206 | 13 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . 19
|
207 | 19 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 201, 206,
207 | redivcld 10853 |
. . . . . . . . . . . . . . . . . 18
|
209 | 204, 205,
208 | lesubaddd 10624 |
. . . . . . . . . . . . . . . . 17
|
210 | 6 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
211 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . 22
|
212 | 208, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
213 | | reflcl 12597 |
. . . . . . . . . . . . . . . . . . . . 21
|
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
215 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . 20
|
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
217 | 210, 216,
202 | ltdivmuld 11923 |
. . . . . . . . . . . . . . . . . 18
|
218 | 21 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
219 | | flflp1 12608 |
. . . . . . . . . . . . . . . . . . 19
|
220 | 218, 212,
219 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
221 | 206, 216 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . 21
|
222 | 221 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
223 | | elioomnf 12268 |
. . . . . . . . . . . . . . . . . . . 20
|
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
225 | 210 | biantrurd 529 |
. . . . . . . . . . . . . . . . . . 19
|
226 | 224, 225 | bitr4d 271 |
. . . . . . . . . . . . . . . . . 18
|
227 | 217, 220,
226 | 3bitr4d 300 |
. . . . . . . . . . . . . . . . 17
|
228 | 203, 209,
227 | 3bitrd 294 |
. . . . . . . . . . . . . . . 16
|
229 | 228 | rabbidva 3188 |
. . . . . . . . . . . . . . 15
|
230 | 1 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 230 | cnveqd 5298 |
. . . . . . . . . . . . . . . . . 18
|
232 | 231 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . 17
|
233 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
234 | 233 | mptpreima 5628 |
. . . . . . . . . . . . . . . . 17
|
235 | 232, 234 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
236 | 235 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
237 | 229, 236 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
238 | | itg2addnc.f1 |
. . . . . . . . . . . . . . . 16
MblFn |
239 | | mbfima 23399 |
. . . . . . . . . . . . . . . 16
MblFn
|
240 | 238, 4, 239 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
241 | 240 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
242 | 237, 241 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
243 | 62 | sseld 3602 |
. . . . . . . . . . . . . . . 16
|
244 | 243 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
245 | 244 | imdistani 726 |
. . . . . . . . . . . . . 14
|
246 | | i1fmbf 23442 |
. . . . . . . . . . . . . . . . 17
MblFn |
247 | 246, 27 | jca 554 |
. . . . . . . . . . . . . . . 16
MblFn
|
248 | 247 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
MblFn
|
249 | | mbfimasn 23401 |
. . . . . . . . . . . . . . . 16
MblFn
|
250 | 249 | 3expa 1265 |
. . . . . . . . . . . . . . 15
MblFn
|
251 | 248, 250 | sylan 488 |
. . . . . . . . . . . . . 14
|
252 | 245, 251 | syl 17 |
. . . . . . . . . . . . 13
|
253 | | inmbl 23310 |
. . . . . . . . . . . . 13
|
254 | 242, 252,
253 | syl2anc 693 |
. . . . . . . . . . . 12
|
255 | 197, 254 | eqeltrd 2701 |
. . . . . . . . . . 11
|
256 | 255 | ralrimiva 2966 |
. . . . . . . . . 10
|
257 | | finiunmbl 23312 |
. . . . . . . . . 10
|
258 | 42, 256, 257 | syl2anc 693 |
. . . . . . . . 9
|
259 | 180, 258 | eqeltrrd 2702 |
. . . . . . . 8
|
260 | | unrab 3898 |
. . . . . . . . . . 11
|
261 | 27 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
|
262 | 261 | cnveqd 5298 |
. . . . . . . . . . . . . 14
|
263 | 262 | imaeq1d 5465 |
. . . . . . . . . . . . 13
|
264 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
265 | 264 | mptpreima 5628 |
. . . . . . . . . . . . 13
|
266 | 263, 265 | syl6eq 2672 |
. . . . . . . . . . . 12
|
267 | 262 | imaeq1d 5465 |
. . . . . . . . . . . . 13
|
268 | 264 | mptpreima 5628 |
. . . . . . . . . . . . 13
|
269 | 267, 268 | syl6eq 2672 |
. . . . . . . . . . . 12
|
270 | 266, 269 | uneq12d 3768 |
. . . . . . . . . . 11
|
271 | 27 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
272 | | 0re 10040 |
. . . . . . . . . . . . . . 15
|
273 | | lttri2 10120 |
. . . . . . . . . . . . . . 15
|
274 | 272, 273 | mpan2 707 |
. . . . . . . . . . . . . 14
|
275 | | ibar 525 |
. . . . . . . . . . . . . . 15
|
276 | | andi 911 |
. . . . . . . . . . . . . . . 16
|
277 | | 0xr 10086 |
. . . . . . . . . . . . . . . . 17
|
278 | | elioomnf 12268 |
. . . . . . . . . . . . . . . . . 18
|
279 | | elioopnf 12267 |
. . . . . . . . . . . . . . . . . 18
|
280 | 278, 279 | orbi12d 746 |
. . . . . . . . . . . . . . . . 17
|
281 | 277, 280 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
282 | 276, 281 | bitr4i 267 |
. . . . . . . . . . . . . . 15
|
283 | 275, 282 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
284 | 274, 283 | bitrd 268 |
. . . . . . . . . . . . 13
|
285 | 271, 284 | syl 17 |
. . . . . . . . . . . 12
|
286 | 285 | rabbidva 3188 |
. . . . . . . . . . 11
|
287 | 260, 270,
286 | 3eqtr4a 2682 |
. . . . . . . . . 10
|
288 | | i1fima 23445 |
. . . . . . . . . . 11
|
289 | | i1fima 23445 |
. . . . . . . . . . 11
|
290 | | unmbl 23305 |
. . . . . . . . . . 11
|
291 | 288, 289,
290 | syl2anc 693 |
. . . . . . . . . 10
|
292 | 287, 291 | eqeltrrd 2702 |
. . . . . . . . 9
|
293 | 292 | ad2antlr 763 |
. . . . . . . 8
|
294 | | inmbl 23310 |
. . . . . . . 8
|
295 | 259, 293,
294 | syl2anc 693 |
. . . . . . 7
|
296 | 295 | adantr 481 |
. . . . . 6
|
297 | 23 | recnd 10068 |
. . . . . . . . . . 11
|
298 | 297 | adantlr 751 |
. . . . . . . . . 10
|
299 | | 1cnd 10056 |
. . . . . . . . . 10
|
300 | | simplr 792 |
. . . . . . . . . . . 12
|
301 | 13 | ad3antlr 767 |
. . . . . . . . . . . 12
|
302 | 19 | ad3antlr 767 |
. . . . . . . . . . . 12
|
303 | 300, 301,
302 | redivcld 10853 |
. . . . . . . . . . 11
|
304 | 303 | recnd 10068 |
. . . . . . . . . 10
|
305 | 298, 299,
304 | subadd2d 10411 |
. . . . . . . . 9
|
306 | | eqcom 2629 |
. . . . . . . . . 10
|
307 | | recn 10026 |
. . . . . . . . . . . 12
|
308 | 307 | ad2antlr 763 |
. . . . . . . . . . 11
|
309 | 25 | recnd 10068 |
. . . . . . . . . . . 12
|
310 | 309 | adantlr 751 |
. . . . . . . . . . 11
|
311 | 13 | recnd 10068 |
. . . . . . . . . . . 12
|
312 | 311 | ad3antlr 767 |
. . . . . . . . . . 11
|
313 | 308, 310,
312, 302 | divmul3d 10835 |
. . . . . . . . . 10
|
314 | 306, 313 | syl5bb 272 |
. . . . . . . . 9
|
315 | 305, 314 | bitr3d 270 |
. . . . . . . 8
|
316 | 315 | rabbidva 3188 |
. . . . . . 7
|
317 | | imaundi 5545 |
. . . . . . . . . . 11
|
318 | 231 | ad4antr 768 |
. . . . . . . . . . . 12
|
319 | | zre 11381 |
. . . . . . . . . . . . . . . 16
|
320 | 319 | adantl 482 |
. . . . . . . . . . . . . . 15
|
321 | 13 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
322 | 320, 321 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
323 | 322 | rexrd 10089 |
. . . . . . . . . . . . 13
|
324 | | peano2z 11418 |
. . . . . . . . . . . . . . . . 17
|
325 | 324 | zred 11482 |
. . . . . . . . . . . . . . . 16
|
326 | 325 | adantl 482 |
. . . . . . . . . . . . . . 15
|
327 | 321, 326 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
328 | 327 | rexrd 10089 |
. . . . . . . . . . . . 13
|
329 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
|
330 | 329 | adantl 482 |
. . . . . . . . . . . . . . 15
|
331 | 311 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
332 | 330, 331 | mulcomd 10061 |
. . . . . . . . . . . . . 14
|
333 | 49 | ad3antlr 767 |
. . . . . . . . . . . . . . 15
|
334 | 319 | ltp1d 10954 |
. . . . . . . . . . . . . . . 16
|
335 | 334 | adantl 482 |
. . . . . . . . . . . . . . 15
|
336 | 320, 326,
333, 335 | ltmul2dd 11928 |
. . . . . . . . . . . . . 14
|
337 | 332, 336 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
338 | | snunioo 12298 |
. . . . . . . . . . . . 13
|
339 | 323, 328,
337, 338 | syl3anc 1326 |
. . . . . . . . . . . 12
|
340 | 318, 339 | imaeq12d 5467 |
. . . . . . . . . . 11
|
341 | 317, 340 | syl5eqr 2670 |
. . . . . . . . . 10
|
342 | 233 | mptpreima 5628 |
. . . . . . . . . . 11
|
343 | 4 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
|
344 | 343 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
|
345 | 344 | 3biant1d 1441 |
. . . . . . . . . . . . . . . 16
|
346 | 345 | adantr 481 |
. . . . . . . . . . . . . . 15
|
347 | 319 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
348 | 344 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
349 | 49 | ad4antlr 769 |
. . . . . . . . . . . . . . . . 17
|
350 | 347, 348,
349 | lemuldivd 11921 |
. . . . . . . . . . . . . . . 16
|
351 | 325 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
352 | 348, 351,
349 | ltdivmuld 11923 |
. . . . . . . . . . . . . . . . 17
|
353 | 352 | bicomd 213 |
. . . . . . . . . . . . . . . 16
|
354 | 350, 353 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
355 | 346, 354 | bitr3d 270 |
. . . . . . . . . . . . . 14
|
356 | | elico2 12237 |
. . . . . . . . . . . . . . . 16
|
357 | 322, 328,
356 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
358 | 357 | adantlr 751 |
. . . . . . . . . . . . . 14
|
359 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
|
360 | 21 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
361 | | flbi 12617 |
. . . . . . . . . . . . . . . 16
|
362 | 360, 361 | sylan 488 |
. . . . . . . . . . . . . . 15
|
363 | 359, 362 | syl5bb 272 |
. . . . . . . . . . . . . 14
|
364 | 355, 358,
363 | 3bitr4d 300 |
. . . . . . . . . . . . 13
|
365 | 364 | an32s 846 |
. . . . . . . . . . . 12
|
366 | 365 | rabbidva 3188 |
. . . . . . . . . . 11
|
367 | 342, 366 | syl5eq 2668 |
. . . . . . . . . 10
|
368 | 341, 367 | eqtrd 2656 |
. . . . . . . . 9
|
369 | 238 | ad4antr 768 |
. . . . . . . . . . 11
MblFn |
370 | 4 | ad4antr 768 |
. . . . . . . . . . 11
|
371 | | mbfimasn 23401 |
. . . . . . . . . . 11
MblFn
|
372 | 369, 370,
322, 371 | syl3anc 1326 |
. . . . . . . . . 10
|
373 | | mbfima 23399 |
. . . . . . . . . . . 12
MblFn
|
374 | 238, 4, 373 | syl2anc 693 |
. . . . . . . . . . 11
|
375 | 374 | ad4antr 768 |
. . . . . . . . . 10
|
376 | | unmbl 23305 |
. . . . . . . . . 10
|
377 | 372, 375,
376 | syl2anc 693 |
. . . . . . . . 9
|
378 | 368, 377 | eqeltrrd 2702 |
. . . . . . . 8
|
379 | | simpr 477 |
. . . . . . . . . . . . . 14
|
380 | 360 | flcld 12599 |
. . . . . . . . . . . . . . 15
|
381 | 380 | adantr 481 |
. . . . . . . . . . . . . 14
|
382 | 379, 381 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
383 | 382 | stoic1a 1697 |
. . . . . . . . . . . 12
|
384 | 383 | an32s 846 |
. . . . . . . . . . 11
|
385 | 384 | ralrimiva 2966 |
. . . . . . . . . 10
|
386 | | rabeq0 3957 |
. . . . . . . . . 10
|
387 | 385, 386 | sylibr 224 |
. . . . . . . . 9
|
388 | | 0mbl 23307 |
. . . . . . . . 9
|
389 | 387, 388 | syl6eqel 2709 |
. . . . . . . 8
|
390 | 378, 389 | pm2.61dan 832 |
. . . . . . 7
|
391 | 316, 390 | eqeltrrd 2702 |
. . . . . 6
|
392 | | inmbl 23310 |
. . . . . 6
|
393 | 296, 391,
392 | syl2anc 693 |
. . . . 5
|
394 | | rabiun 33382 |
. . . . . . . . . . 11
|
395 | | rabeq 3192 |
. . . . . . . . . . . 12
|
396 | 176, 395 | syl 17 |
. . . . . . . . . . 11
|
397 | 394, 396 | syl5eqr 2670 |
. . . . . . . . . 10
|
398 | 397 | ad2antlr 763 |
. . . . . . . . 9
|
399 | 184 | notbid 308 |
. . . . . . . . . . . . . . 15
|
400 | 399 | rabbidva 3188 |
. . . . . . . . . . . . . 14
|
401 | | inrab2 3900 |
. . . . . . . . . . . . . . 15
|
402 | | rabeq 3192 |
. . . . . . . . . . . . . . . 16
|
403 | 192, 402 | syl 17 |
. . . . . . . . . . . . . . 15
|
404 | 401, 403 | syl5eq 2668 |
. . . . . . . . . . . . . 14
|
405 | 400, 404 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
406 | 405 | ad3antlr 767 |
. . . . . . . . . . . 12
|
407 | | imaundi 5545 |
. . . . . . . . . . . . . . . . 17
|
408 | 13, 19 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
409 | | redivcl 10744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
410 | 409 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
411 | 408, 410 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
412 | 411 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
413 | 412 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
414 | 413, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
415 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . 22
|
416 | | reflcl 12597 |
. . . . . . . . . . . . . . . . . . . . . 22
|
417 | 414, 415,
416 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
|
418 | 13 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
|
419 | 417, 418 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
|
420 | 419 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
421 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . 20
|
422 | 421 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
423 | | ltpnf 11954 |
. . . . . . . . . . . . . . . . . . . 20
|
424 | 419, 423 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
425 | | snunioo 12298 |
. . . . . . . . . . . . . . . . . . 19
|
426 | 420, 422,
424, 425 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
427 | 426 | imaeq2d 5466 |
. . . . . . . . . . . . . . . . 17
|
428 | 407, 427 | syl5eqr 2670 |
. . . . . . . . . . . . . . . 16
|
429 | 231 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . 18
|
430 | 233 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . 18
|
431 | 429, 430 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
|
432 | 431 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
433 | 414, 415 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
434 | 433 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
435 | | flflp1 12608 |
. . . . . . . . . . . . . . . . . . . . 21
|
436 | 434, 360,
435 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
437 | 419 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
438 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . . . . . 22
|
439 | 437, 438 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
440 | 344 | biantrurd 529 |
. . . . . . . . . . . . . . . . . . . . 21
|
441 | 417 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
442 | 49 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . 22
|
443 | 441, 344,
442 | lemuldivd 11921 |
. . . . . . . . . . . . . . . . . . . . 21
|
444 | 439, 440,
443 | 3bitr2d 296 |
. . . . . . . . . . . . . . . . . . . 20
|
445 | 414 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
446 | 360, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
447 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . 21
|
448 | 445, 446,
447 | ltadd1d 10620 |
. . . . . . . . . . . . . . . . . . . 20
|
449 | 436, 444,
448 | 3bitr4d 300 |
. . . . . . . . . . . . . . . . . . 19
|
450 | 303, 447,
446 | ltaddsubd 10627 |
. . . . . . . . . . . . . . . . . . 19
|
451 | 449, 450 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
|
452 | 446, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
453 | 300, 452,
442 | ltdivmul2d 11924 |
. . . . . . . . . . . . . . . . . 18
|
454 | 452, 301 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . 19
|
455 | 300, 454 | ltnled 10184 |
. . . . . . . . . . . . . . . . . 18
|
456 | 451, 453,
455 | 3bitrd 294 |
. . . . . . . . . . . . . . . . 17
|
457 | 456 | rabbidva 3188 |
. . . . . . . . . . . . . . . 16
|
458 | 428, 432,
457 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
|
459 | 238 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
MblFn |
460 | | mbfimasn 23401 |
. . . . . . . . . . . . . . . . 17
MblFn
|
461 | 459, 343,
419, 460 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
462 | | mbfima 23399 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
463 | 238, 4, 462 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
464 | 463 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
|
465 | | unmbl 23305 |
. . . . . . . . . . . . . . . 16
|
466 | 461, 464,
465 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
467 | 458, 466 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
|
468 | 245, 467 | syl 17 |
. . . . . . . . . . . . 13
|
469 | | inmbl 23310 |
. . . . . . . . . . . . 13
|
470 | 468, 252,
469 | syl2anc 693 |
. . . . . . . . . . . 12
|
471 | 406, 470 | eqeltrd 2701 |
. . . . . . . . . . 11
|
472 | 471 | ralrimiva 2966 |
. . . . . . . . . 10
|
473 | | finiunmbl 23312 |
. . . . . . . . . 10
|
474 | 42, 472, 473 | syl2anc 693 |
. . . . . . . . 9
|
475 | 398, 474 | eqeltrrd 2702 |
. . . . . . . 8
|
476 | 262 | imaeq1d 5465 |
. . . . . . . . . . 11
|
477 | 264 | mptpreima 5628 |
. . . . . . . . . . . 12
|
478 | 145 | elsn 4192 |
. . . . . . . . . . . . . 14
|
479 | 478 | a1i 11 |
. . . . . . . . . . . . 13
|
480 | 479 | rabbiia 3185 |
. . . . . . . . . . . 12
|
481 | 477, 480 | eqtri 2644 |
. . . . . . . . . . 11
|
482 | 476, 481 | syl6eq 2672 |
. . . . . . . . . 10
|
483 | | i1fima 23445 |
. . . . . . . . . 10
|
484 | 482, 483 | eqeltrrd 2702 |
. . . . . . . . 9
|
485 | 484 | ad2antlr 763 |
. . . . . . . 8
|
486 | | unmbl 23305 |
. . . . . . . 8
|
487 | 475, 485,
486 | syl2anc 693 |
. . . . . . 7
|
488 | 487 | adantr 481 |
. . . . . 6
|
489 | 262 | imaeq1d 5465 |
. . . . . . . . 9
|
490 | 264 | mptpreima 5628 |
. . . . . . . . . 10
|
491 | 145 | elsn 4192 |
. . . . . . . . . . . . 13
|
492 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
493 | 491, 492 | bitri 264 |
. . . . . . . . . . . 12
|
494 | 493 | a1i 11 |
. . . . . . . . . . 11
|
495 | 494 | rabbiia 3185 |
. . . . . . . . . 10
|
496 | 490, 495 | eqtri 2644 |
. . . . . . . . 9
|
497 | 489, 496 | syl6eq 2672 |
. . . . . . . 8
|
498 | 497 | ad3antlr 767 |
. . . . . . 7
|
499 | 498, 251 | eqeltrrd 2702 |
. . . . . 6
|
500 | | inmbl 23310 |
. . . . . 6
|
501 | 488, 499,
500 | syl2anc 693 |
. . . . 5
|
502 | | unmbl 23305 |
. . . . 5
|
503 | 393, 501,
502 | syl2anc 693 |
. . . 4
|
504 | 166, 503 | syl 17 |
. . 3
|
505 | 160, 504 | syl5eqel 2705 |
. 2
|
506 | | mblvol 23298 |
. . . 4
|
507 | 505, 506 | syl 17 |
. . 3
|
508 | | eldifsn 4317 |
. . . . . 6
|
509 | 164 | anim1d 588 |
. . . . . 6
|
510 | 508, 509 | syl5bi 232 |
. . . . 5
|
511 | 510 | imdistani 726 |
. . . 4
|
512 | 133 | a1i 11 |
. . . . . . . . . . 11
|
513 | 476, 477 | syl6eq 2672 |
. . . . . . . . . . 11
|
514 | 512, 513 | ineq12d 3815 |
. . . . . . . . . 10
|
515 | | inrab 3899 |
. . . . . . . . . 10
|
516 | 514, 515 | syl6eq 2672 |
. . . . . . . . 9
|
517 | 516 | ad3antlr 767 |
. . . . . . . 8
|
518 | 149 | biimpri 218 |
. . . . . . . . . . . . . . . . . 18
|
519 | 518 | intnand 962 |
. . . . . . . . . . . . . . . . 17
|
520 | 519 | iffalsed 4097 |
. . . . . . . . . . . . . . . 16
|
521 | | eqtr 2641 |
. . . . . . . . . . . . . . . 16
|
522 | 520, 521 | mpancom 703 |
. . . . . . . . . . . . . . 15
|
523 | 522 | adantl 482 |
. . . . . . . . . . . . . 14
|
524 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
525 | 524 | necomd 2849 |
. . . . . . . . . . . . . 14
|
526 | 523, 525 | eqnetrd 2861 |
. . . . . . . . . . . . 13
|
527 | 526 | ex 450 |
. . . . . . . . . . . 12
|
528 | | orcom 402 |
. . . . . . . . . . . . . 14
|
529 | | ianor 509 |
. . . . . . . . . . . . . 14
|
530 | | imor 428 |
. . . . . . . . . . . . . 14
|
531 | 528, 529,
530 | 3bitr4i 292 |
. . . . . . . . . . . . 13
|
532 | 147 | necon3bbii 2841 |
. . . . . . . . . . . . . 14
|
533 | 478, 532 | imbi12i 340 |
. . . . . . . . . . . . 13
|
534 | 531, 533 | bitri 264 |
. . . . . . . . . . . 12
|
535 | 527, 534 | sylibr 224 |
. . . . . . . . . . 11
|
536 | 535 | ralrimiva 2966 |
. . . . . . . . . 10
|
537 | | rabeq0 3957 |
. . . . . . . . . 10
|
538 | 536, 537 | sylibr 224 |
. . . . . . . . 9
|
539 | 538 | ad2antll 765 |
. . . . . . . 8
|
540 | 517, 539 | eqtrd 2656 |
. . . . . . 7
|
541 | | imassrn 5477 |
. . . . . . . . 9
|
542 | | dfdm4 5316 |
. . . . . . . . . 10
|
543 | 146, 31 | dmmpti 6023 |
. . . . . . . . . 10
|
544 | 542, 543 | eqtr3i 2646 |
. . . . . . . . 9
|
545 | 541, 544 | sseqtri 3637 |
. . . . . . . 8
|
546 | | reldisj 4020 |
. . . . . . . 8
|
547 | 545, 546 | ax-mp 5 |
. . . . . . 7
|
548 | 540, 547 | sylib 208 |
. . . . . 6
|
549 | | ffun 6048 |
. . . . . . . . . 10
|
550 | | difpreima 6343 |
. . . . . . . . . 10
|
551 | 549, 550 | syl 17 |
. . . . . . . . 9
|
552 | 168, 174 | syl5eq 2668 |
. . . . . . . . . 10
|
553 | 552 | difeq1d 3727 |
. . . . . . . . 9
|
554 | 551, 553 | eqtrd 2656 |
. . . . . . . 8
|
555 | 27, 554 | syl 17 |
. . . . . . 7
|
556 | 555 | ad3antlr 767 |
. . . . . 6
|
557 | 548, 556 | sseqtr4d 3642 |
. . . . 5
|
558 | | imassrn 5477 |
. . . . . . 7
|
559 | 558, 189 | syl5sseq 3653 |
. . . . . 6
|
560 | 559 | ad3antlr 767 |
. . . . 5
|
561 | | i1fima 23445 |
. . . . . . . 8
|
562 | | mblvol 23298 |
. . . . . . . 8
|
563 | 561, 562 | syl 17 |
. . . . . . 7
|
564 | | neldifsn 4321 |
. . . . . . . 8
|
565 | | i1fima2 23446 |
. . . . . . . 8
|
566 | 564, 565 | mpan2 707 |
. . . . . . 7
|
567 | 563, 566 | eqeltrrd 2702 |
. . . . . 6
|
568 | 567 | ad3antlr 767 |
. . . . 5
|
569 | | ovolsscl 23254 |
. . . . 5
|
570 | 557, 560,
568, 569 | syl3anc 1326 |
. . . 4
|
571 | 511, 570 | syl 17 |
. . 3
|
572 | 507, 571 | eqeltrd 2701 |
. 2
|
573 | 32, 132, 505, 572 | i1fd 23448 |
1
|