Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . 4
|
2 | | 1zzd 11408 |
. . . 4
|
3 | | uniioombl.c |
. . . 4
|
4 | | eqidd 2623 |
. . . 4
|
5 | | uniioombl.t |
. . . . . 6
|
6 | | eqidd 2623 |
. . . . . 6
|
7 | | uniioombl.g |
. . . . . . . . . 10
|
8 | | eqid 2622 |
. . . . . . . . . . 11
|
9 | 8 | ovolfsf 23240 |
. . . . . . . . . 10
|
10 | 7, 9 | syl 17 |
. . . . . . . . 9
|
11 | 10 | ffvelrnda 6359 |
. . . . . . . 8
|
12 | | elrege0 12278 |
. . . . . . . 8
|
13 | 11, 12 | sylib 208 |
. . . . . . 7
|
14 | 13 | simpld 475 |
. . . . . 6
|
15 | 13 | simprd 479 |
. . . . . 6
|
16 | | uniioombl.1 |
. . . . . . . 8
|
17 | | uniioombl.2 |
. . . . . . . 8
Disj
|
18 | | uniioombl.3 |
. . . . . . . 8
|
19 | | uniioombl.a |
. . . . . . . 8
|
20 | | uniioombl.e |
. . . . . . . 8
|
21 | | uniioombl.s |
. . . . . . . 8
|
22 | | uniioombl.v |
. . . . . . . 8
|
23 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22 | uniioombllem1 23349 |
. . . . . . 7
|
24 | 8, 5 | ovolsf 23241 |
. . . . . . . . . . . . 13
|
25 | 7, 24 | syl 17 |
. . . . . . . . . . . 12
|
26 | | frn 6053 |
. . . . . . . . . . . 12
|
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
|
28 | | icossxr 12258 |
. . . . . . . . . . 11
|
29 | 27, 28 | syl6ss 3615 |
. . . . . . . . . 10
|
30 | | supxrub 12154 |
. . . . . . . . . 10
|
31 | 29, 30 | sylan 488 |
. . . . . . . . 9
|
32 | 31 | ralrimiva 2966 |
. . . . . . . 8
|
33 | | ffn 6045 |
. . . . . . . . . 10
|
34 | 25, 33 | syl 17 |
. . . . . . . . 9
|
35 | | breq1 4656 |
. . . . . . . . . 10
|
36 | 35 | ralrn 6362 |
. . . . . . . . 9
|
37 | 34, 36 | syl 17 |
. . . . . . . 8
|
38 | 32, 37 | mpbid 222 |
. . . . . . 7
|
39 | | breq2 4657 |
. . . . . . . . 9
|
40 | 39 | ralbidv 2986 |
. . . . . . . 8
|
41 | 40 | rspcev 3309 |
. . . . . . 7
|
42 | 23, 38, 41 | syl2anc 693 |
. . . . . 6
|
43 | 1, 5, 2, 6, 14, 15, 42 | isumsup2 14578 |
. . . . 5
|
44 | | rge0ssre 12280 |
. . . . . . 7
|
45 | 27, 44 | syl6ss 3615 |
. . . . . 6
|
46 | | 1nn 11031 |
. . . . . . . . 9
|
47 | | fdm 6051 |
. . . . . . . . . 10
|
48 | 25, 47 | syl 17 |
. . . . . . . . 9
|
49 | 46, 48 | syl5eleqr 2708 |
. . . . . . . 8
|
50 | | ne0i 3921 |
. . . . . . . 8
|
51 | 49, 50 | syl 17 |
. . . . . . 7
|
52 | | dm0rn0 5342 |
. . . . . . . 8
|
53 | 52 | necon3bii 2846 |
. . . . . . 7
|
54 | 51, 53 | sylib 208 |
. . . . . 6
|
55 | | breq2 4657 |
. . . . . . . . 9
|
56 | 55 | ralbidv 2986 |
. . . . . . . 8
|
57 | 56 | rspcev 3309 |
. . . . . . 7
|
58 | 23, 32, 57 | syl2anc 693 |
. . . . . 6
|
59 | | supxrre 12157 |
. . . . . 6
|
60 | 45, 54, 58, 59 | syl3anc 1326 |
. . . . 5
|
61 | 43, 60 | breqtrrd 4681 |
. . . 4
|
62 | 1, 2, 3, 4, 61 | climi2 14242 |
. . 3
|
63 | 1 | r19.2uz 14091 |
. . 3
|
64 | 62, 63 | syl 17 |
. 2
|
65 | | 1zzd 11408 |
. . . . . . . . 9
|
66 | 3 | ad2antrr 762 |
. . . . . . . . . 10
|
67 | | simplrl 800 |
. . . . . . . . . . 11
|
68 | 67 | nnrpd 11870 |
. . . . . . . . . 10
|
69 | 66, 68 | rpdivcld 11889 |
. . . . . . . . 9
|
70 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | inex1 4799 |
. . . . . . . . . . . . . . 15
|
72 | 71 | rgenw 2924 |
. . . . . . . . . . . . . 14
|
73 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
74 | 73 | fnmpt 6020 |
. . . . . . . . . . . . . 14
|
75 | 72, 74 | mp1i 13 |
. . . . . . . . . . . . 13
|
76 | | elfznn 12370 |
. . . . . . . . . . . . 13
|
77 | | fvco2 6273 |
. . . . . . . . . . . . 13
|
78 | 75, 76, 77 | syl2an 494 |
. . . . . . . . . . . 12
|
79 | 76 | adantl 482 |
. . . . . . . . . . . . . 14
|
80 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | ineq1d 3813 |
. . . . . . . . . . . . . . 15
|
83 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
84 | 83 | inex1 4799 |
. . . . . . . . . . . . . . 15
|
85 | 82, 73, 84 | fvmpt 6282 |
. . . . . . . . . . . . . 14
|
86 | 79, 85 | syl 17 |
. . . . . . . . . . . . 13
|
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . 12
|
88 | 78, 87 | eqtrd 2656 |
. . . . . . . . . . 11
|
89 | | simpr 477 |
. . . . . . . . . . . 12
|
90 | 89, 1 | syl6eleq 2711 |
. . . . . . . . . . 11
|
91 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
|
93 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 94, 95, 96 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 93, 97 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
99 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . 18
|
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
102 | | df-ov 6653 |
. . . . . . . . . . . . . . . 16
|
103 | 101, 102 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
104 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
|
105 | 103, 104 | syl6eqss 3655 |
. . . . . . . . . . . . . 14
|
106 | 105 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
107 | 103 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
108 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . 18
|
109 | 94, 95, 108 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
110 | | ovolioo 23336 |
. . . . . . . . . . . . . . . . 17
|
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
|
112 | 107, 111 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
113 | 109 | simp2d 1074 |
. . . . . . . . . . . . . . . 16
|
114 | 109 | simp1d 1073 |
. . . . . . . . . . . . . . . 16
|
115 | 113, 114 | resubcld 10458 |
. . . . . . . . . . . . . . 15
|
116 | 112, 115 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
117 | 116 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
118 | | ovolsscl 23254 |
. . . . . . . . . . . . 13
|
119 | 92, 106, 117, 118 | syl3anc 1326 |
. . . . . . . . . . . 12
|
120 | 119 | recnd 10068 |
. . . . . . . . . . 11
|
121 | 88, 90, 120 | fsumser 14461 |
. . . . . . . . . 10
|
122 | 121 | eqcomd 2628 |
. . . . . . . . 9
|
123 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
125 | 124 | ineq1d 3813 |
. . . . . . . . . . . . 13
|
126 | 125 | cbvmptv 4750 |
. . . . . . . . . . . 12
|
127 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
|
128 | | infeq1 8382 |
. . . . . . . . . . . . . . 15
inf inf |
129 | | supeq1 8351 |
. . . . . . . . . . . . . . 15
|
130 | 128, 129 | opeq12d 4410 |
. . . . . . . . . . . . . 14
inf
inf
|
131 | 127, 130 | ifbieq2d 4111 |
. . . . . . . . . . . . 13
inf
inf |
132 | 131 | cbvmptv 4750 |
. . . . . . . . . . . 12
inf
inf
|
133 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22, 126, 132 | uniioombllem2 23351 |
. . . . . . . . . . 11
|
134 | 95, 133 | sylan2 491 |
. . . . . . . . . 10
|
135 | 134 | adantlr 751 |
. . . . . . . . 9
|
136 | 1, 65, 69, 122, 135 | climi2 14242 |
. . . . . . . 8
|
137 | | 1z 11407 |
. . . . . . . . 9
|
138 | 1 | rexuz3 14088 |
. . . . . . . . 9
|
139 | 137, 138 | ax-mp 5 |
. . . . . . . 8
|
140 | 136, 139 | sylib 208 |
. . . . . . 7
|
141 | 140 | ralrimiva 2966 |
. . . . . 6
|
142 | | fzfi 12771 |
. . . . . . 7
|
143 | | rexfiuz 14087 |
. . . . . . 7
|
144 | 142, 143 | ax-mp 5 |
. . . . . 6
|
145 | 141, 144 | sylibr 224 |
. . . . 5
|
146 | 1 | rexuz3 14088 |
. . . . . 6
|
147 | 137, 146 | ax-mp 5 |
. . . . 5
|
148 | 145, 147 | sylibr 224 |
. . . 4
|
149 | 1 | r19.2uz 14091 |
. . . 4
|
150 | 148, 149 | syl 17 |
. . 3
|
151 | 16 | adantr 481 |
. . . . 5
|
152 | 17 | adantr 481 |
. . . . 5
Disj |
153 | 20 | adantr 481 |
. . . . 5
|
154 | 3 | adantr 481 |
. . . . 5
|
155 | 7 | adantr 481 |
. . . . 5
|
156 | 21 | adantr 481 |
. . . . 5
|
157 | 22 | adantr 481 |
. . . . 5
|
158 | | simprll 802 |
. . . . 5
|
159 | | simprlr 803 |
. . . . 5
|
160 | | eqid 2622 |
. . . . 5
|
161 | | simprrl 804 |
. . . . 5
|
162 | | simprrr 805 |
. . . . . 6
|
163 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
164 | 163 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
165 | 164 | ineq1d 3813 |
. . . . . . . . . . . . 13
|
166 | 165 | fveq2d 6195 |
. . . . . . . . . . . 12
|
167 | 166 | cbvsumv 14426 |
. . . . . . . . . . 11
|
168 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
169 | 168 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
170 | 169 | ineq2d 3814 |
. . . . . . . . . . . . 13
|
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . 12
|
172 | 171 | sumeq2sdv 14435 |
. . . . . . . . . . 11
|
173 | 167, 172 | syl5eq 2668 |
. . . . . . . . . 10
|
174 | 169 | ineq1d 3813 |
. . . . . . . . . . 11
|
175 | 174 | fveq2d 6195 |
. . . . . . . . . 10
|
176 | 173, 175 | oveq12d 6668 |
. . . . . . . . 9
|
177 | 176 | fveq2d 6195 |
. . . . . . . 8
|
178 | 177 | breq1d 4663 |
. . . . . . 7
|
179 | 178 | cbvralv 3171 |
. . . . . 6
|
180 | 162, 179 | sylib 208 |
. . . . 5
|
181 | | eqid 2622 |
. . . . 5
|
182 | 151, 152,
18, 19, 153, 154, 155, 156, 5, 157, 158, 159, 160, 161, 180, 181 | uniioombllem5 23355 |
. . . 4
|
183 | 182 | anassrs 680 |
. . 3
|
184 | 150, 183 | rexlimddv 3035 |
. 2
|
185 | 64, 184 | rexlimddv 3035 |
1
|