Step | Hyp | Ref
| Expression |
1 | | vonioo.l |
. . . . 5
|
2 | | vonioo.a |
. . . . . . 7
|
3 | 2 | adantr 481 |
. . . . . 6
|
4 | | feq2 6027 |
. . . . . . 7
|
5 | 4 | adantl 482 |
. . . . . 6
|
6 | 3, 5 | mpbid 222 |
. . . . 5
|
7 | | vonioo.b |
. . . . . . 7
|
8 | 7 | adantr 481 |
. . . . . 6
|
9 | | feq2 6027 |
. . . . . . 7
|
10 | 9 | adantl 482 |
. . . . . 6
|
11 | 8, 10 | mpbid 222 |
. . . . 5
|
12 | 1, 6, 11 | hoidmv0val 40797 |
. . . 4
|
13 | 12 | eqcomd 2628 |
. . 3
|
14 | | fveq2 6191 |
. . . . . 6
voln voln |
15 | | vonioo.i |
. . . . . . . 8
|
16 | 15 | a1i 11 |
. . . . . . 7
|
17 | | ixpeq1 7919 |
. . . . . . 7
|
18 | 16, 17 | eqtrd 2656 |
. . . . . 6
|
19 | 14, 18 | fveq12d 6197 |
. . . . 5
voln voln |
20 | 19 | adantl 482 |
. . . 4
voln voln |
21 | | 0fin 8188 |
. . . . . . 7
|
22 | 21 | a1i 11 |
. . . . . 6
|
23 | | eqid 2622 |
. . . . . 6
voln
voln |
24 | | ressxr 10083 |
. . . . . . . 8
|
25 | 24 | a1i 11 |
. . . . . . 7
|
26 | 6, 25 | fssd 6057 |
. . . . . 6
|
27 | 11, 25 | fssd 6057 |
. . . . . 6
|
28 | 22, 23, 26, 27 | ioovonmbl 40891 |
. . . . 5
voln |
29 | 28 | von0val 40885 |
. . . 4
voln |
30 | 20, 29 | eqtrd 2656 |
. . 3
voln |
31 | | fveq2 6191 |
. . . . 5
|
32 | 31 | oveqd 6667 |
. . . 4
|
33 | 32 | adantl 482 |
. . 3
|
34 | 13, 30, 33 | 3eqtr4d 2666 |
. 2
voln |
35 | | neqne 2802 |
. . . 4
|
36 | 35 | adantl 482 |
. . 3
|
37 | | nfv 1843 |
. . . . . . . . 9
|
38 | | nfra1 2941 |
. . . . . . . . 9
|
39 | 37, 38 | nfan 1828 |
. . . . . . . 8
|
40 | 2 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
41 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
42 | | volico 40200 |
. . . . . . . . . . . 12
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . . . . 11
|
44 | 43 | ad4ant14 1293 |
. . . . . . . . . 10
|
45 | | rspa 2930 |
. . . . . . . . . . . 12
|
46 | 45 | iftrued 4094 |
. . . . . . . . . . 11
|
47 | 46 | adantll 750 |
. . . . . . . . . 10
|
48 | 44, 47 | eqtrd 2656 |
. . . . . . . . 9
|
49 | 48 | ex 450 |
. . . . . . . 8
|
50 | 39, 49 | ralrimi 2957 |
. . . . . . 7
|
51 | 50 | prodeq2d 14652 |
. . . . . 6
|
52 | 51 | eqcomd 2628 |
. . . . 5
|
53 | | fveq2 6191 |
. . . . . . . . . 10
|
54 | | fveq2 6191 |
. . . . . . . . . 10
|
55 | 53, 54 | breq12d 4666 |
. . . . . . . . 9
|
56 | 55 | cbvralv 3171 |
. . . . . . . 8
|
57 | 56 | biimpi 206 |
. . . . . . 7
|
58 | 57 | adantl 482 |
. . . . . 6
|
59 | | vonioo.x |
. . . . . . . . 9
|
60 | 59 | adantr 481 |
. . . . . . . 8
|
61 | 60 | adantr 481 |
. . . . . . 7
|
62 | 2 | adantr 481 |
. . . . . . . 8
|
63 | 62 | adantr 481 |
. . . . . . 7
|
64 | 7 | adantr 481 |
. . . . . . . 8
|
65 | 64 | adantr 481 |
. . . . . . 7
|
66 | | simpr 477 |
. . . . . . . 8
|
67 | 66 | adantr 481 |
. . . . . . 7
|
68 | 56, 45 | sylanbr 490 |
. . . . . . . 8
|
69 | 68 | adantll 750 |
. . . . . . 7
|
70 | | fveq2 6191 |
. . . . . . . . . . . 12
|
71 | 70 | oveq1d 6665 |
. . . . . . . . . . 11
|
72 | 71 | cbvmptv 4750 |
. . . . . . . . . 10
|
73 | 72 | a1i 11 |
. . . . . . . . 9
|
74 | | oveq2 6658 |
. . . . . . . . . . 11
|
75 | 74 | oveq2d 6666 |
. . . . . . . . . 10
|
76 | 75 | mpteq2dv 4745 |
. . . . . . . . 9
|
77 | 73, 76 | eqtrd 2656 |
. . . . . . . 8
|
78 | 77 | cbvmptv 4750 |
. . . . . . 7
|
79 | | nfcv 2764 |
. . . . . . . 8
|
80 | | nfcv 2764 |
. . . . . . . . 9
|
81 | | nffvmpt1 6199 |
. . . . . . . . . . 11
|
82 | | nfcv 2764 |
. . . . . . . . . . 11
|
83 | 81, 82 | nffv 6198 |
. . . . . . . . . 10
|
84 | | nfcv 2764 |
. . . . . . . . . 10
|
85 | | nfcv 2764 |
. . . . . . . . . 10
|
86 | 83, 84, 85 | nfov 6676 |
. . . . . . . . 9
|
87 | 80, 86 | nfixp 7927 |
. . . . . . . 8
|
88 | | fveq2 6191 |
. . . . . . . . . . 11
|
89 | 88 | fveq1d 6193 |
. . . . . . . . . 10
|
90 | 89 | oveq1d 6665 |
. . . . . . . . 9
|
91 | 90 | ixpeq2dv 7924 |
. . . . . . . 8
|
92 | 79, 87, 91 | cbvmpt 4749 |
. . . . . . 7
|
93 | 61, 63, 65, 67, 69, 15, 78, 92 | vonioolem2 40895 |
. . . . . 6
voln |
94 | 58, 93 | syldan 487 |
. . . . 5
voln |
95 | 1, 60, 66, 62, 64 | hoidmvn0val 40798 |
. . . . . 6
|
96 | 95 | adantr 481 |
. . . . 5
|
97 | 52, 94, 96 | 3eqtr4d 2666 |
. . . 4
voln |
98 | | rexnal 2995 |
. . . . . . . . . 10
|
99 | 98 | bicomi 214 |
. . . . . . . . 9
|
100 | 99 | biimpi 206 |
. . . . . . . 8
|
101 | 100 | adantl 482 |
. . . . . . 7
|
102 | | simpr 477 |
. . . . . . . . . . 11
|
103 | 41 | adantr 481 |
. . . . . . . . . . . 12
|
104 | 40 | adantr 481 |
. . . . . . . . . . . 12
|
105 | 103, 104 | lenltd 10183 |
. . . . . . . . . . 11
|
106 | 102, 105 | mpbird 247 |
. . . . . . . . . 10
|
107 | 106 | ex 450 |
. . . . . . . . 9
|
108 | 107 | reximdva 3017 |
. . . . . . . 8
|
109 | 108 | adantr 481 |
. . . . . . 7
|
110 | 101, 109 | mpd 15 |
. . . . . 6
|
111 | 110 | adantlr 751 |
. . . . 5
|
112 | | nfcv 2764 |
. . . . . . . . 9
voln |
113 | | nfixp1 7928 |
. . . . . . . . . 10
|
114 | 15, 113 | nfcxfr 2762 |
. . . . . . . . 9
|
115 | 112, 114 | nffv 6198 |
. . . . . . . 8
voln |
116 | | nfcv 2764 |
. . . . . . . 8
|
117 | 115, 116 | nfeq 2776 |
. . . . . . 7
voln |
118 | 59 | vonmea 40788 |
. . . . . . . . . . . 12
voln Meas |
119 | 118 | mea0 40671 |
. . . . . . . . . . 11
voln |
120 | 119 | 3ad2ant1 1082 |
. . . . . . . . . 10
voln |
121 | 15 | a1i 11 |
. . . . . . . . . . . 12
|
122 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
123 | | simp3 1063 |
. . . . . . . . . . . . . . 15
|
124 | 24, 40 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
125 | 124 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
126 | 24, 41 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
127 | 126 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
128 | | ioo0 12200 |
. . . . . . . . . . . . . . . 16
|
129 | 125, 127,
128 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
130 | 123, 129 | mpbird 247 |
. . . . . . . . . . . . . 14
|
131 | | rspe 3003 |
. . . . . . . . . . . . . 14
|
132 | 122, 130,
131 | syl2anc 693 |
. . . . . . . . . . . . 13
|
133 | | ixp0 7941 |
. . . . . . . . . . . . 13
|
134 | 132, 133 | syl 17 |
. . . . . . . . . . . 12
|
135 | 121, 134 | eqtrd 2656 |
. . . . . . . . . . 11
|
136 | 135 | fveq2d 6195 |
. . . . . . . . . 10
voln voln |
137 | | ne0i 3921 |
. . . . . . . . . . . . . 14
|
138 | 137 | adantl 482 |
. . . . . . . . . . . . 13
|
139 | 138, 95 | syldan 487 |
. . . . . . . . . . . 12
|
140 | 139 | 3adant3 1081 |
. . . . . . . . . . 11
|
141 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
142 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
143 | 142, 70 | breq12d 4666 |
. . . . . . . . . . . . . 14
|
144 | 141, 143 | 3anbi23d 1402 |
. . . . . . . . . . . . 13
|
145 | 144 | imbi1d 331 |
. . . . . . . . . . . 12
|
146 | | nfv 1843 |
. . . . . . . . . . . . 13
|
147 | 59 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
148 | | volicore 40795 |
. . . . . . . . . . . . . . . 16
|
149 | 40, 41, 148 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
150 | 149 | recnd 10068 |
. . . . . . . . . . . . . 14
|
151 | 150 | 3ad2antl1 1223 |
. . . . . . . . . . . . 13
|
152 | | simp2 1062 |
. . . . . . . . . . . . 13
|
153 | 53, 54 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
155 | 154 | adantl 482 |
. . . . . . . . . . . . . 14
|
156 | 2 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
157 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
158 | | volico 40200 |
. . . . . . . . . . . . . . . . . 18
|
159 | 156, 157,
158 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
160 | 159 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
161 | | simp3 1063 |
. . . . . . . . . . . . . . . . . 18
|
162 | 157, 156 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 162 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
|
164 | 161, 163 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
165 | 164 | iffalsed 4097 |
. . . . . . . . . . . . . . . 16
|
166 | 160, 165 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
167 | 166 | adantr 481 |
. . . . . . . . . . . . . 14
|
168 | 155, 167 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
169 | 146, 147,
151, 152, 168 | fprodeq0g 14725 |
. . . . . . . . . . . 12
|
170 | 145, 169 | chvarv 2263 |
. . . . . . . . . . 11
|
171 | 140, 170 | eqtrd 2656 |
. . . . . . . . . 10
|
172 | 120, 136,
171 | 3eqtr4d 2666 |
. . . . . . . . 9
voln |
173 | 172 | 3exp 1264 |
. . . . . . . 8
voln |
174 | 173 | adantr 481 |
. . . . . . 7
voln |
175 | 37, 117, 174 | rexlimd 3026 |
. . . . . 6
voln |
176 | 175 | imp 445 |
. . . . 5
voln |
177 | 111, 176 | syldan 487 |
. . . 4
voln |
178 | 97, 177 | pm2.61dan 832 |
. . 3
voln |
179 | 36, 178 | syldan 487 |
. 2
voln |
180 | 34, 179 | pm2.61dan 832 |
1
voln |