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 |
. . . . . . . . . . . . . 14
|
24 | 23 | ex 450 |
. . . . . . . . . . . . 13
|
25 | 24 | imdistani 726 |
. . . . . . . . . . . 12
|
26 | 25 | ralimi 2952 |
. . . . . . . . . . 11
|
27 | 22, 26 | sylbi 207 |
. . . . . . . . . 10
|
28 | 27 | ancoms 469 |
. . . . . . . . 9
|
29 | | foima 6120 |
. . . . . . . . . . . 12
|
30 | 29 | raleqdv 3144 |
. . . . . . . . . . 11
|
31 | | fofn 6117 |
. . . . . . . . . . . 12
|
32 | | ssid 3624 |
. . . . . . . . . . . 12
|
33 | | sseq1 3626 |
. . . . . . . . . . . . . 14
|
34 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
35 | 34 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
36 | 33, 35 | anbi12d 747 |
. . . . . . . . . . . . 13
|
37 | 36 | ralima 6498 |
. . . . . . . . . . . 12
|
38 | 31, 32, 37 | sylancl 694 |
. . . . . . . . . . 11
|
39 | 30, 38 | bitr3d 270 |
. . . . . . . . . 10
|
40 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
..^
|
41 | | ovolssnul 23255 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
42 | 40, 41 | mp3an1 1411 |
. . . . . . . . . . . . . . . . 17
..^ |
43 | | ssdifss 3741 |
. . . . . . . . . . . . . . . . . 18
..^
|
44 | | nulmbl 23303 |
. . . . . . . . . . . . . . . . . . 19
..^
..^
..^ |
45 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
..^
..^ |
46 | 45 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^
..^ |
47 | 46 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^
..^ |
48 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
49 | 47, 48 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^
..^ |
50 | 49 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
..^ |
51 | 50 | ancld 576 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^
..^
..^ |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^
..^
..^
..^
..^ |
53 | 44, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
..^
..^
..^
..^ |
54 | 43, 53 | sylan 488 |
. . . . . . . . . . . . . . . . 17
..^
..^
..^ |
55 | 42, 54 | syldan 487 |
. . . . . . . . . . . . . . . 16
..^
..^ |
56 | 55 | ralimi 2952 |
. . . . . . . . . . . . . . 15
..^
..^ |
57 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ |
59 | 58 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
60 | 57, 59 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
61 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
62 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
|
63 | | difexg 4808 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
65 | 60, 61, 64 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
66 | 65 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
67 | 65 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
68 | 67 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
69 | 66, 68 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
..^
..^
..^
..^ |
70 | 69 | ralbiia 2979 |
. . . . . . . . . . . . . . . 16
..^
..^
..^
..^ |
71 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
73 | 72 | iuneq1d 4545 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
74 | 71, 73 | difeq12d 3729 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
75 | 74 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
76 | 74 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
77 | 76 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
78 | 75, 77 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
..^
..^
..^
..^ |
79 | 78 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
..^ ..^
..^
..^ |
80 | 70, 79 | bitri 264 |
. . . . . . . . . . . . . . 15
..^
..^
..^
..^ |
81 | 56, 80 | sylibr 224 |
. . . . . . . . . . . . . 14
..^
..^ |
82 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | iundisj2 23317 |
. . . . . . . . . . . . . . 15
Disj
..^ |
84 | | disjeq2 4624 |
. . . . . . . . . . . . . . . 16
..^
..^
Disj ..^ Disj
..^ |
85 | 84, 65 | mprg 2926 |
. . . . . . . . . . . . . . 15
Disj ..^ Disj
..^ |
86 | 83, 85 | mpbir 221 |
. . . . . . . . . . . . . 14
Disj ..^ |
87 | | nnex 11026 |
. . . . . . . . . . . . . . . . 17
|
88 | 87 | mptex 6486 |
. . . . . . . . . . . . . . . 16
..^ |
89 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
90 | 89 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
91 | 89 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
92 | 91 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
93 | 90, 92 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
..^ |
94 | 93 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . 18
..^
..^
..^ |
95 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
96 | 95 | disjeq2dv 4625 |
. . . . . . . . . . . . . . . . . 18
..^ Disj
Disj
..^ |
97 | 94, 96 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
..^ Disj
..^
..^ Disj
..^ |
98 | 89 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
100 | | voliunnfl.1 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | | voliunnfl.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
102 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
104 | 100, 103 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
|
105 | 104 | rneqi 5352 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 105 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 91 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ |
108 | 107 | seqeq3d 12809 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
109 | 108 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
110 | 109 | supeq1d 8352 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
111 | 106, 110 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
112 | 99, 111 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
..^ ..^
..^ |
113 | 97, 112 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
..^ Disj
..^
..^ Disj
..^
..^
..^ |
114 | | voliunnfl.3 |
. . . . . . . . . . . . . . . 16
Disj
|
115 | 88, 113, 114 | vtocl 3259 |
. . . . . . . . . . . . . . 15
..^
..^ Disj
..^
..^
..^ |
116 | 65 | iuneq2i 4539 |
. . . . . . . . . . . . . . . 16
..^
..^ |
117 | 116 | fveq2i 6194 |
. . . . . . . . . . . . . . 15
..^
..^ |
118 | 67 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
119 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . 18
..^
..^
..^
..^ |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
121 | 120 | rneqi 5352 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
122 | 121 | supeq1i 8353 |
. . . . . . . . . . . . . . 15
..^
..^ |
123 | 115, 117,
122 | 3eqtr3g 2679 |
. . . . . . . . . . . . . 14
..^
..^ Disj
..^
..^
..^ |
124 | 81, 86, 123 | sylancl 694 |
. . . . . . . . . . . . 13
..^
..^
|
125 | 124 | adantl 482 |
. . . . . . . . . . . 12
..^
..^
|
126 | 82 | iundisj 23316 |
. . . . . . . . . . . . . . . 16
..^ |
127 | | fofun 6116 |
. . . . . . . . . . . . . . . . 17
|
128 | | funiunfv 6506 |
. . . . . . . . . . . . . . . . 17
|
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
|
130 | 126, 129 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
..^ |
131 | 29 | unieqd 4446 |
. . . . . . . . . . . . . . 15
|
132 | 130, 131 | eqtrd 2656 |
. . . . . . . . . . . . . 14
..^ |
133 | 132 | fveq2d 6195 |
. . . . . . . . . . . . 13
..^ |
134 | 133 | adantr 481 |
. . . . . . . . . . . 12
..^ |
135 | 57 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 57 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
137 | 136 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . 21
|
138 | 135, 137 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
|
139 | 138 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . 19
|
140 | | ssdifss 3741 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
142 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
143 | | ovolssnul 23255 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ ..^ |
144 | 142, 143 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
145 | 141, 144 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
146 | | nulmbl 23303 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
..^ |
147 | | mblvol 23298 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
..^ |
148 | 145, 146,
147 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
149 | 148, 144 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
..^ |
150 | 139, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^ |
151 | 150 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . 17
..^ |
152 | 151 | seqeq3d 12809 |
. . . . . . . . . . . . . . . 16
..^ |
153 | 152 | rneqd 5353 |
. . . . . . . . . . . . . . 15
..^ |
154 | 153 | supeq1d 8352 |
. . . . . . . . . . . . . 14
..^
|
155 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . 22
|
156 | | ser1const 12857 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | 155, 156 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
|
158 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . 22
|
159 | 158 | mul01d 10235 |
. . . . . . . . . . . . . . . . . . . . 21
|
160 | 157, 159 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 160 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . 19
|
162 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | | seqeq3 12806 |
. . . . . . . . . . . . . . . . . . . . 21
|
164 | 162, 163 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
165 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . 22
|
166 | | seqfn 12813 |
. . . . . . . . . . . . . . . . . . . . . 22
|
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
168 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
169 | 168 | fneq2i 5986 |
. . . . . . . . . . . . . . . . . . . . . 22
|
170 | | dffn5 6241 |
. . . . . . . . . . . . . . . . . . . . . 22
|
171 | 169, 170 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . . 21
|
172 | 167, 171 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
|
173 | 164, 172 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . 19
|
174 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . 19
|
175 | 161, 173,
174 | 3eqtr4i 2654 |
. . . . . . . . . . . . . . . . . 18
|
176 | 175 | rneqi 5352 |
. . . . . . . . . . . . . . . . 17
|
177 | | 1nn 11031 |
. . . . . . . . . . . . . . . . . 18
|
178 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . 18
|
179 | | rnxp 5564 |
. . . . . . . . . . . . . . . . . 18
|
180 | 177, 178,
179 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
|
181 | 176, 180 | eqtri 2644 |
. . . . . . . . . . . . . . . 16
|
182 | 181 | supeq1i 8353 |
. . . . . . . . . . . . . . 15
|
183 | | xrltso 11974 |
. . . . . . . . . . . . . . . 16
|
184 | | 0xr 10086 |
. . . . . . . . . . . . . . . 16
|
185 | | supsn 8378 |
. . . . . . . . . . . . . . . 16
|
186 | 183, 184,
185 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
187 | 182, 186 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
188 | 154, 187 | syl6eq 2672 |
. . . . . . . . . . . . 13
..^ |
189 | 188 | adantl 482 |
. . . . . . . . . . . 12
..^
|
190 | 125, 134,
189 | 3eqtr3rd 2665 |
. . . . . . . . . . 11
|
191 | 190 | ex 450 |
. . . . . . . . . 10
|
192 | 39, 191 | sylbid 230 |
. . . . . . . . 9
|
193 | 28, 192 | syl5 34 |
. . . . . . . 8
|
194 | 193 | exlimiv 1858 |
. . . . . . 7
|
195 | 18, 194 | syl 17 |
. . . . . 6
|
196 | 195 | expimpd 629 |
. . . . 5
|
197 | 11, 196 | pm2.61ine 2877 |
. . . 4
|
198 | | renepnf 10087 |
. . . . . . 7
|
199 | 48, 198 | mp1i 13 |
. . . . . 6
|
200 | | fveq2 6191 |
. . . . . . 7
|
201 | | rembl 23308 |
. . . . . . . . 9
|
202 | | mblvol 23298 |
. . . . . . . . 9
|
203 | 201, 202 | ax-mp 5 |
. . . . . . . 8
|
204 | | ovolre 23293 |
. . . . . . . 8
|
205 | 203, 204 | eqtri 2644 |
. . . . . . 7
|
206 | 200, 205 | syl6eq 2672 |
. . . . . 6
|
207 | 199, 206 | neeqtrrd 2868 |
. . . . 5
|
208 | 207 | necon2i 2828 |
. . . 4
|
209 | 197, 208 | syl 17 |
. . 3
|
210 | 209 | expr 643 |
. 2
|
211 | | eqimss 3657 |
. . 3
|
212 | 211 | necon3bi 2820 |
. 2
|
213 | 210, 212 | pm2.61d1 171 |
1
|