Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
2 | 1 | ad2ant2r 783 |
. . . . . . . . . 10
|
3 | | fzofi 12773 |
. . . . . . . . . . 11
..^ |
4 | | simpll 790 |
. . . . . . . . . . . . 13
|
5 | | elfzouz 12474 |
. . . . . . . . . . . . . 14
..^
|
6 | | nnuz 11723 |
. . . . . . . . . . . . . 14
|
7 | 5, 6 | syl6eleqr 2712 |
. . . . . . . . . . . . 13
..^
|
8 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
9 | 4, 7, 8 | syl2an 494 |
. . . . . . . . . . . 12
..^ |
10 | 9 | ralrimiva 2966 |
. . . . . . . . . . 11
..^ |
11 | | finiunmbl 23312 |
. . . . . . . . . . 11
..^
..^ ..^ |
12 | 3, 10, 11 | sylancr 695 |
. . . . . . . . . 10
..^ |
13 | | difmbl 23311 |
. . . . . . . . . 10
..^
..^ |
14 | 2, 12, 13 | syl2anc 693 |
. . . . . . . . 9
..^ |
15 | | mblvol 23298 |
. . . . . . . . . . 11
..^
..^
..^ |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
..^
..^ |
17 | | difssd 3738 |
. . . . . . . . . . 11
..^ |
18 | | mblss 23299 |
. . . . . . . . . . . 12
|
19 | 2, 18 | syl 17 |
. . . . . . . . . . 11
|
20 | | mblvol 23298 |
. . . . . . . . . . . . 13
|
21 | 2, 20 | syl 17 |
. . . . . . . . . . . 12
|
22 | | simprr 796 |
. . . . . . . . . . . 12
|
23 | 21, 22 | eqeltrrd 2702 |
. . . . . . . . . . 11
|
24 | | ovolsscl 23254 |
. . . . . . . . . . 11
..^ ..^ |
25 | 17, 19, 23, 24 | syl3anc 1326 |
. . . . . . . . . 10
..^ |
26 | 16, 25 | eqeltrd 2701 |
. . . . . . . . 9
..^ |
27 | 14, 26 | jca 554 |
. . . . . . . 8
..^
..^ |
28 | 27 | expr 643 |
. . . . . . 7
..^ ..^ |
29 | 28 | ralimdva 2962 |
. . . . . 6
..^ ..^ |
30 | 29 | imp 445 |
. . . . 5
..^
..^ |
31 | | fveq2 6191 |
. . . . . 6
|
32 | 31 | iundisj2 23317 |
. . . . 5
Disj
..^ |
33 | | eqid 2622 |
. . . . . 6
..^
..^ |
34 | | eqid 2622 |
. . . . . 6
..^ ..^ |
35 | 33, 34 | voliun 23322 |
. . . . 5
..^
..^ Disj
..^
..^
..^
|
36 | 30, 32, 35 | sylancl 694 |
. . . 4
..^
..^
|
37 | 31 | iundisj 23316 |
. . . . . 6
..^ |
38 | | ffn 6045 |
. . . . . . . 8
|
39 | 38 | ad2antrr 762 |
. . . . . . 7
|
40 | | fniunfv 6505 |
. . . . . . 7
|
41 | 39, 40 | syl 17 |
. . . . . 6
|
42 | 37, 41 | syl5eqr 2670 |
. . . . 5
..^ |
43 | 42 | fveq2d 6195 |
. . . 4
..^ |
44 | | 1z 11407 |
. . . . . . . . . . 11
|
45 | | seqfn 12813 |
. . . . . . . . . . 11
..^ |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . 10
..^ |
47 | 6 | fneq2i 5986 |
. . . . . . . . . 10
..^
..^ |
48 | 46, 47 | mpbir 221 |
. . . . . . . . 9
..^ |
49 | 48 | a1i 11 |
. . . . . . . 8
..^ |
50 | | volf 23297 |
. . . . . . . . . 10
|
51 | | simpll 790 |
. . . . . . . . . 10
|
52 | | fco 6058 |
. . . . . . . . . 10
|
53 | 50, 51, 52 | sylancr 695 |
. . . . . . . . 9
|
54 | | ffn 6045 |
. . . . . . . . 9
|
55 | 53, 54 | syl 17 |
. . . . . . . 8
|
56 | | fveq2 6191 |
. . . . . . . . . . . . 13
..^
..^ |
57 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
58 | 57 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
59 | 56, 58 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ |
60 | 59 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^ |
61 | | fveq2 6191 |
. . . . . . . . . . . . 13
..^
..^ |
62 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
63 | 62 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
64 | 61, 63 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ |
65 | 64 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^ |
66 | | fveq2 6191 |
. . . . . . . . . . . . 13
..^
..^ |
67 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
69 | 66, 68 | eqeq12d 2637 |
. . . . . . . . . . . 12
..^ ..^ |
70 | 69 | imbi2d 330 |
. . . . . . . . . . 11
..^
..^ |
71 | | seq1 12814 |
. . . . . . . . . . . . . 14
..^
..^ |
72 | 44, 71 | ax-mp 5 |
. . . . . . . . . . . . 13
..^
..^ |
73 | | 1nn 11031 |
. . . . . . . . . . . . . 14
|
74 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
75 | | fzo0 12492 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
76 | 74, 75 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
77 | 76 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
78 | | 0iun 4577 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 77, 78 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
..^ |
80 | 79 | difeq2d 3728 |
. . . . . . . . . . . . . . . . . 18
..^
|
81 | | dif0 3950 |
. . . . . . . . . . . . . . . . . 18
|
82 | 80, 81 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
..^ |
83 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
84 | 82, 83 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
..^ |
85 | 84 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
..^ |
86 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
87 | 85, 34, 86 | fvmpt 6282 |
. . . . . . . . . . . . . 14
..^ |
88 | 73, 87 | ax-mp 5 |
. . . . . . . . . . . . 13
..^ |
89 | 72, 88 | eqtri 2644 |
. . . . . . . . . . . 12
..^ |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
..^ |
91 | | oveq1 6657 |
. . . . . . . . . . . . . 14
..^
..^
..^ ..^ |
92 | | seqp1 12816 |
. . . . . . . . . . . . . . . . 17
..^ ..^
..^ |
93 | 92, 6 | eleq2s 2719 |
. . . . . . . . . . . . . . . 16
..^ ..^
..^ |
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ ..^
..^ |
95 | | undif2 4044 |
. . . . . . . . . . . . . . . . . 18
|
96 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
99 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 98, 100 | sseq12d 3634 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 101 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 96, 97, 102 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
|
104 | | ssequn1 3783 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 103, 104 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
|
106 | 95, 105 | syl5req 2669 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
108 | | simplll 798 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108, 96 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
110 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . . 20
|
111 | 110 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 108, 111 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
|
113 | | difmbl 23311 |
. . . . . . . . . . . . . . . . . 18
|
114 | 112, 109,
113 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
115 | | disjdif 4040 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
117 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
|
118 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 119 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 120 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
|
122 | 96, 117, 121 | sylc 65 |
. . . . . . . . . . . . . . . . 17
|
123 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 114, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
125 | | difssd 3738 |
. . . . . . . . . . . . . . . . . . 19
|
126 | | mblss 23299 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 112, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
128 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . 21
|
129 | 112, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
130 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
131 | 130 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
132 | 131 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
|
133 | 132 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | 111, 117,
133 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 129, 134 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . 19
|
136 | | ovolsscl 23254 |
. . . . . . . . . . . . . . . . . . 19
|
137 | 125, 127,
135, 136 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
138 | 124, 137 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
139 | | volun 23313 |
. . . . . . . . . . . . . . . . 17
|
140 | 109, 114,
116, 122, 138, 139 | syl32anc 1334 |
. . . . . . . . . . . . . . . 16
|
141 | 97 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
142 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
143 | 142 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
144 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
145 | 144 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
146 | | volsuplem 23323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
147 | 141, 143,
145, 146 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 147 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | | iunss 4561 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | 148, 149 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 96, 6 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
152 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
154 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
155 | 154 | ssiun2s 4564 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
156 | 153, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | 150, 156 | eqssd 3620 |
. . . . . . . . . . . . . . . . . . . . 21
|
158 | 96 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
159 | | fzval3 12536 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
161 | 160 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
162 | 157, 161 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
163 | 162 | difeq2d 3728 |
. . . . . . . . . . . . . . . . . . 19
..^ |
164 | 163 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
..^ |
165 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ |
166 | 165 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
167 | 130, 166 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
168 | 167 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
169 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
170 | 168, 34, 169 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
171 | 111, 170 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
172 | 164, 171 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
..^ |
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
..^ |
174 | 107, 140,
173 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
..^ |
175 | 94, 174 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
..^ ..^
..^ ..^ |
176 | 91, 175 | syl5ibr 236 |
. . . . . . . . . . . . 13
..^
..^ |
177 | 176 | expcom 451 |
. . . . . . . . . . . 12
..^
..^ |
178 | 177 | a2d 29 |
. . . . . . . . . . 11
..^
..^ |
179 | 60, 65, 70, 65, 90, 178 | nnind 11038 |
. . . . . . . . . 10
..^ |
180 | 179 | impcom 446 |
. . . . . . . . 9
..^ |
181 | | fvco3 6275 |
. . . . . . . . . 10
|
182 | 51, 181 | sylan 488 |
. . . . . . . . 9
|
183 | 180, 182 | eqtr4d 2659 |
. . . . . . . 8
..^ |
184 | 49, 55, 183 | eqfnfvd 6314 |
. . . . . . 7
..^ |
185 | 184 | rneqd 5353 |
. . . . . 6
..^ |
186 | | rnco2 5642 |
. . . . . 6
|
187 | 185, 186 | syl6eq 2672 |
. . . . 5
..^ |
188 | 187 | supeq1d 8352 |
. . . 4
..^
|
189 | 36, 43, 188 | 3eqtr3d 2664 |
. . 3
|
190 | 189 | ex 450 |
. 2
|
191 | | rexnal 2995 |
. . 3
|
192 | | fniunfv 6505 |
. . . . . . . . . . . 12
|
193 | 38, 192 | syl 17 |
. . . . . . . . . . 11
|
194 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
195 | 194 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
196 | | iunmbl 23321 |
. . . . . . . . . . . 12
|
197 | 195, 196 | syl 17 |
. . . . . . . . . . 11
|
198 | 193, 197 | eqeltrrd 2702 |
. . . . . . . . . 10
|
199 | 198 | ad2antrr 762 |
. . . . . . . . 9
|
200 | | mblss 23299 |
. . . . . . . . 9
|
201 | 199, 200 | syl 17 |
. . . . . . . 8
|
202 | | ovolcl 23246 |
. . . . . . . 8
|
203 | 201, 202 | syl 17 |
. . . . . . 7
|
204 | | pnfge 11964 |
. . . . . . 7
|
205 | 203, 204 | syl 17 |
. . . . . 6
|
206 | | simprr 796 |
. . . . . . . . 9
|
207 | 1 | ad2ant2r 783 |
. . . . . . . . . . . . 13
|
208 | 207, 18 | syl 17 |
. . . . . . . . . . . 12
|
209 | | ovolcl 23246 |
. . . . . . . . . . . 12
|
210 | 208, 209 | syl 17 |
. . . . . . . . . . 11
|
211 | | xrrebnd 11999 |
. . . . . . . . . . 11
|
212 | 210, 211 | syl 17 |
. . . . . . . . . 10
|
213 | 207, 20 | syl 17 |
. . . . . . . . . . 11
|
214 | 213 | eleq1d 2686 |
. . . . . . . . . 10
|
215 | | ovolge0 23249 |
. . . . . . . . . . . . 13
|
216 | | mnflt0 11959 |
. . . . . . . . . . . . . 14
|
217 | | mnfxr 10096 |
. . . . . . . . . . . . . . 15
|
218 | | 0xr 10086 |
. . . . . . . . . . . . . . 15
|
219 | | xrltletr 11988 |
. . . . . . . . . . . . . . 15
|
220 | 217, 218,
219 | mp3an12 1414 |
. . . . . . . . . . . . . 14
|
221 | 216, 220 | mpani 712 |
. . . . . . . . . . . . 13
|
222 | 209, 215,
221 | sylc 65 |
. . . . . . . . . . . 12
|
223 | 208, 222 | syl 17 |
. . . . . . . . . . 11
|
224 | 223 | biantrurd 529 |
. . . . . . . . . 10
|
225 | 212, 214,
224 | 3bitr4d 300 |
. . . . . . . . 9
|
226 | 206, 225 | mtbid 314 |
. . . . . . . 8
|
227 | | nltpnft 11995 |
. . . . . . . . 9
|
228 | 210, 227 | syl 17 |
. . . . . . . 8
|
229 | 226, 228 | mpbird 247 |
. . . . . . 7
|
230 | 38 | ad2antrr 762 |
. . . . . . . . . 10
|
231 | | simprl 794 |
. . . . . . . . . 10
|
232 | | fnfvelrn 6356 |
. . . . . . . . . 10
|
233 | 230, 231,
232 | syl2anc 693 |
. . . . . . . . 9
|
234 | | elssuni 4467 |
. . . . . . . . 9
|
235 | 233, 234 | syl 17 |
. . . . . . . 8
|
236 | | ovolss 23253 |
. . . . . . . 8
|
237 | 235, 201,
236 | syl2anc 693 |
. . . . . . 7
|
238 | 229, 237 | eqbrtrrd 4677 |
. . . . . 6
|
239 | | pnfxr 10092 |
. . . . . . 7
|
240 | | xrletri3 11985 |
. . . . . . 7
|
241 | 203, 239,
240 | sylancl 694 |
. . . . . 6
|
242 | 205, 238,
241 | mpbir2and 957 |
. . . . 5
|
243 | | mblvol 23298 |
. . . . . 6
|
244 | 199, 243 | syl 17 |
. . . . 5
|
245 | | imassrn 5477 |
. . . . . . 7
|
246 | | frn 6053 |
. . . . . . . . 9
|
247 | 50, 246 | ax-mp 5 |
. . . . . . . 8
|
248 | | iccssxr 12256 |
. . . . . . . 8
|
249 | 247, 248 | sstri 3612 |
. . . . . . 7
|
250 | 245, 249 | sstri 3612 |
. . . . . 6
|
251 | 213, 229 | eqtrd 2656 |
. . . . . . 7
|
252 | | simpll 790 |
. . . . . . . 8
|
253 | | ffun 6048 |
. . . . . . . . . 10
|
254 | 50, 253 | ax-mp 5 |
. . . . . . . . 9
|
255 | | frn 6053 |
. . . . . . . . 9
|
256 | | funfvima2 6493 |
. . . . . . . . 9
|
257 | 254, 255,
256 | sylancr 695 |
. . . . . . . 8
|
258 | 252, 233,
257 | sylc 65 |
. . . . . . 7
|
259 | 251, 258 | eqeltrrd 2702 |
. . . . . 6
|
260 | | supxrpnf 12148 |
. . . . . 6
|
261 | 250, 259,
260 | sylancr 695 |
. . . . 5
|
262 | 242, 244,
261 | 3eqtr4d 2666 |
. . . 4
|
263 | 262 | rexlimdvaa 3032 |
. . 3
|
264 | 191, 263 | syl5bir 233 |
. 2
|
265 | 190, 264 | pm2.61d 170 |
1
|