Step | Hyp | Ref
| Expression |
1 | | unieq 4444 |
. . . . . . . . 9
|
2 | | uni0 4465 |
. . . . . . . . 9
|
3 | 1, 2 | syl6eq 2672 |
. . . . . . . 8
|
4 | 3 | fveq2d 6195 |
. . . . . . 7
|
5 | | 0mbl 23307 |
. . . . . . . . 9
|
6 | | mblvol 23298 |
. . . . . . . . 9
|
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
|
8 | | ovol0 23261 |
. . . . . . . 8
|
9 | 7, 8 | eqtri 2644 |
. . . . . . 7
|
10 | 4, 9 | syl6req 2673 |
. . . . . 6
|
11 | 10 | a1d 25 |
. . . . 5
|
12 | | reldom 7961 |
. . . . . . . . . . 11
|
13 | 12 | brrelexi 5158 |
. . . . . . . . . 10
|
14 | | 0sdomg 8089 |
. . . . . . . . . 10
|
15 | 13, 14 | syl 17 |
. . . . . . . . 9
|
16 | 15 | biimparc 504 |
. . . . . . . 8
|
17 | | fodomr 8111 |
. . . . . . . 8
|
18 | 16, 17 | sylancom 701 |
. . . . . . 7
|
19 | | unissb 4469 |
. . . . . . . . . . . . 13
|
20 | 19 | anbi1i 731 |
. . . . . . . . . . . 12
|
21 | | r19.26 3064 |
. . . . . . . . . . . 12
|
22 | 20, 21 | bitr4i 267 |
. . . . . . . . . . 11
|
23 | | ovolctb2 23260 |
. . . . . . . . . . . . 13
|
24 | | nulmbl 23303 |
. . . . . . . . . . . . . 14
|
25 | | mblvol 23298 |
. . . . . . . . . . . . . . . 16
|
26 | | eqtr 2641 |
. . . . . . . . . . . . . . . . 17
|
27 | 26 | expcom 451 |
. . . . . . . . . . . . . . . 16
|
28 | 25, 27 | syl5 34 |
. . . . . . . . . . . . . . 15
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . 14
|
30 | 24, 29 | jcai 559 |
. . . . . . . . . . . . 13
|
31 | 23, 30 | syldan 487 |
. . . . . . . . . . . 12
|
32 | 31 | ralimi 2952 |
. . . . . . . . . . 11
|
33 | 22, 32 | sylbi 207 |
. . . . . . . . . 10
|
34 | 33 | ancoms 469 |
. . . . . . . . 9
|
35 | | fzfi 12771 |
. . . . . . . . . . . . . . 15
|
36 | | fzssuz 12382 |
. . . . . . . . . . . . . . . . 17
|
37 | | nnuz 11723 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | sseqtr4i 3638 |
. . . . . . . . . . . . . . . 16
|
39 | | fof 6115 |
. . . . . . . . . . . . . . . . . . . 20
|
40 | 39 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
41 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
42 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
43 | 42 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 41, 43 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 44 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | 45 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 40, 47 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | an32s 846 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
|
51 | | ssralv 3666 |
. . . . . . . . . . . . . . . 16
|
52 | 38, 50, 51 | mpsyl 68 |
. . . . . . . . . . . . . . 15
|
53 | | finiunmbl 23312 |
. . . . . . . . . . . . . . 15
|
54 | 35, 52, 53 | sylancr 695 |
. . . . . . . . . . . . . 14
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . 13
|
56 | | eqid 2622 |
. . . . . . . . . . . . 13
|
57 | 55, 56 | fmptd 6385 |
. . . . . . . . . . . 12
|
58 | | fzssp1 12384 |
. . . . . . . . . . . . . . 15
|
59 | | iunss1 4532 |
. . . . . . . . . . . . . . 15
|
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
61 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
62 | 61 | iuneq1d 4545 |
. . . . . . . . . . . . . . . 16
|
63 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
64 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
65 | 63, 64 | iunex 7147 |
. . . . . . . . . . . . . . . 16
|
66 | 62, 56, 65 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
67 | | peano2nn 11032 |
. . . . . . . . . . . . . . . 16
|
68 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . 17
|
70 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70, 64 | iunex 7147 |
. . . . . . . . . . . . . . . . 17
|
72 | 69, 56, 71 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
|
73 | 67, 72 | syl 17 |
. . . . . . . . . . . . . . 15
|
74 | 66, 73 | sseq12d 3634 |
. . . . . . . . . . . . . 14
|
75 | 60, 74 | mpbiri 248 |
. . . . . . . . . . . . 13
|
76 | 75 | rgen 2922 |
. . . . . . . . . . . 12
|
77 | | nnex 11026 |
. . . . . . . . . . . . . 14
|
78 | 77 | mptex 6486 |
. . . . . . . . . . . . 13
|
79 | | feq1 6026 |
. . . . . . . . . . . . . . 15
|
80 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
81 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
82 | 80, 81 | sseq12d 3634 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
|
84 | 79, 83 | anbi12d 747 |
. . . . . . . . . . . . . 14
|
85 | | rneq 5351 |
. . . . . . . . . . . . . . . . 17
|
86 | 85 | unieqd 4446 |
. . . . . . . . . . . . . . . 16
|
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
88 | 85 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
|
89 | 88 | supeq1d 8352 |
. . . . . . . . . . . . . . 15
|
90 | 87, 89 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
91 | 84, 90 | imbi12d 334 |
. . . . . . . . . . . . 13
|
92 | | volsupnfl.0 |
. . . . . . . . . . . . 13
|
93 | 78, 91, 92 | vtocl 3259 |
. . . . . . . . . . . 12
|
94 | 57, 76, 93 | sylancl 694 |
. . . . . . . . . . 11
|
95 | | df-iun 4522 |
. . . . . . . . . . . . . . . 16
|
96 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
97 | 96, 37 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . 22
|
98 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 99 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 97, 100 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 102 | rexeqdv 3145 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 103 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 101, 104 | syldan 487 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 105 | rexlimiva 3028 |
. . . . . . . . . . . . . . . . . . 19
|
107 | | ssrexv 3667 |
. . . . . . . . . . . . . . . . . . . . . 22
|
108 | 38, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
109 | 99 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . 21
|
110 | 108, 109 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
|
111 | 110 | rexlimivw 3029 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 106, 111 | impbii 199 |
. . . . . . . . . . . . . . . . . 18
|
113 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | rexbii 3041 |
. . . . . . . . . . . . . . . . . 18
|
115 | 112, 114 | bitr4i 267 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | abbii 2739 |
. . . . . . . . . . . . . . . 16
|
117 | 95, 116 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
118 | | df-iun 4522 |
. . . . . . . . . . . . . . 15
|
119 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
120 | 119, 64 | iunex 7147 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | dfiun3 5380 |
. . . . . . . . . . . . . . 15
|
122 | 117, 118,
121 | 3eqtr2i 2650 |
. . . . . . . . . . . . . 14
|
123 | | fofn 6117 |
. . . . . . . . . . . . . . . 16
|
124 | | fniunfv 6505 |
. . . . . . . . . . . . . . . 16
|
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . 15
|
126 | | forn 6118 |
. . . . . . . . . . . . . . . 16
|
127 | 126 | unieqd 4446 |
. . . . . . . . . . . . . . 15
|
128 | 125, 127 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
129 | 122, 128 | syl5eqr 2670 |
. . . . . . . . . . . . 13
|
130 | 129 | fveq2d 6195 |
. . . . . . . . . . . 12
|
131 | 130 | adantr 481 |
. . . . . . . . . . 11
|
132 | | rnco2 5642 |
. . . . . . . . . . . . . 14
|
133 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
134 | | volf 23297 |
. . . . . . . . . . . . . . . . . . 19
|
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
136 | 135 | feqmptd 6249 |
. . . . . . . . . . . . . . . . 17
|
137 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
138 | 55, 133, 136, 137 | fmptco 6396 |
. . . . . . . . . . . . . . . 16
|
139 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | 55, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
141 | | mblss 23299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
142 | 141 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
143 | 25 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
144 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
145 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
146 | 144, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
147 | 143, 146 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
148 | 147 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
149 | 142, 148 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
150 | 149 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | 150 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
152 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
153 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
154 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
155 | 154 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
156 | 153, 155 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
157 | 156 | ralima 6498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
158 | 123, 152,
157 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
159 | | foima 6120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
160 | 159 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
161 | 158, 160 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
163 | 151, 162 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
164 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
165 | 38, 163, 164 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
166 | 165 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
167 | | ovolfiniun 23269 |
. . . . . . . . . . . . . . . . . . . . . 22
|
168 | 35, 166, 167 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
169 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
170 | 49, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
171 | 45 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
172 | 40, 171 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
173 | 172 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
174 | 173 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
175 | 170, 174 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
176 | 175 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
177 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
178 | 38, 176, 177 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
179 | 178 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
180 | 179 | sumeq2d 14432 |
. . . . . . . . . . . . . . . . . . . . . 22
|
181 | 35 | olci 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
182 | | sumz 14453 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
183 | 181, 182 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
184 | 180, 183 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
|
185 | 168, 184 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
|
186 | | mblss 23299 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
187 | 186 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
188 | 52, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
189 | | iunss 4561 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
190 | 188, 189 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
|
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
192 | | ovolge0 23249 |
. . . . . . . . . . . . . . . . . . . . 21
|
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
194 | | ovolcl 23246 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
195 | 190, 194 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
196 | 195 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
197 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . . . 21
|
198 | | xrletri3 11985 |
. . . . . . . . . . . . . . . . . . . . 21
|
199 | 196, 197,
198 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
200 | 185, 193,
199 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . 19
|
201 | 140, 200 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
202 | 201 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . 17
|
203 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . 17
|
204 | 202, 203 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
|
205 | 138, 204 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
206 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
207 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 134, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
209 | 120, 56 | fnmpti 6022 |
. . . . . . . . . . . . . . . . . 18
|
210 | | fnco 5999 |
. . . . . . . . . . . . . . . . . 18
|
211 | 208, 209,
210 | mp3an12 1414 |
. . . . . . . . . . . . . . . . 17
|
212 | 57, 206, 211 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
213 | | 1nn 11031 |
. . . . . . . . . . . . . . . . 17
|
214 | 213 | ne0ii 3923 |
. . . . . . . . . . . . . . . 16
|
215 | | fconst5 6471 |
. . . . . . . . . . . . . . . 16
|
216 | 212, 214,
215 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
217 | 205, 216 | mpbid 222 |
. . . . . . . . . . . . . 14
|
218 | 132, 217 | syl5eqr 2670 |
. . . . . . . . . . . . 13
|
219 | 218 | supeq1d 8352 |
. . . . . . . . . . . 12
|
220 | | xrltso 11974 |
. . . . . . . . . . . . 13
|
221 | | supsn 8378 |
. . . . . . . . . . . . 13
|
222 | 220, 197,
221 | mp2an 708 |
. . . . . . . . . . . 12
|
223 | 219, 222 | syl6eq 2672 |
. . . . . . . . . . 11
|
224 | 94, 131, 223 | 3eqtr3rd 2665 |
. . . . . . . . . 10
|
225 | 224 | ex 450 |
. . . . . . . . 9
|
226 | 34, 225 | syl5 34 |
. . . . . . . 8
|
227 | 226 | exlimiv 1858 |
. . . . . . 7
|
228 | 18, 227 | syl 17 |
. . . . . 6
|
229 | 228 | expimpd 629 |
. . . . 5
|
230 | 11, 229 | pm2.61ine 2877 |
. . . 4
|
231 | | renepnf 10087 |
. . . . . . 7
|
232 | 144, 231 | mp1i 13 |
. . . . . 6
|
233 | | fveq2 6191 |
. . . . . . 7
|
234 | | rembl 23308 |
. . . . . . . . 9
|
235 | | mblvol 23298 |
. . . . . . . . 9
|
236 | 234, 235 | ax-mp 5 |
. . . . . . . 8
|
237 | | ovolre 23293 |
. . . . . . . 8
|
238 | 236, 237 | eqtri 2644 |
. . . . . . 7
|
239 | 233, 238 | syl6eq 2672 |
. . . . . 6
|
240 | 232, 239 | neeqtrrd 2868 |
. . . . 5
|
241 | 240 | necon2i 2828 |
. . . 4
|
242 | 230, 241 | syl 17 |
. . 3
|
243 | 242 | expr 643 |
. 2
|
244 | | eqimss 3657 |
. . 3
|
245 | 244 | necon3bi 2820 |
. 2
|
246 | 243, 245 | pm2.61d1 171 |
1
|