Metamath Proof Explorer


Theorem vonioolem2

Description: The n-dimensional Lebesgue measure of open intervals. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonioolem2.x φ X Fin
vonioolem2.a φ A : X
vonioolem2.b φ B : X
vonioolem2.n φ X
vonioolem2.t φ k X A k < B k
vonioolem2.i I = k X A k B k
vonioolem2.c C = n k X A k + 1 n
vonioolem2.d D = n k X C n k B k
Assertion vonioolem2 φ voln X I = k X B k A k

Proof

Step Hyp Ref Expression
1 vonioolem2.x φ X Fin
2 vonioolem2.a φ A : X
3 vonioolem2.b φ B : X
4 vonioolem2.n φ X
5 vonioolem2.t φ k X A k < B k
6 vonioolem2.i I = k X A k B k
7 vonioolem2.c C = n k X A k + 1 n
8 vonioolem2.d D = n k X C n k B k
9 1 vonmea φ voln X Meas
10 1zzd φ 1
11 nnuz = 1
12 1 adantr φ n X Fin
13 eqid dom voln X = dom voln X
14 2 adantr φ n A : X
15 14 ffvelrnda φ n k X A k
16 nnrecre n 1 n
17 16 ad2antlr φ n k X 1 n
18 15 17 readdcld φ n k X A k + 1 n
19 18 fmpttd φ n k X A k + 1 n : X
20 7 a1i φ C = n k X A k + 1 n
21 1 mptexd φ k X A k + 1 n V
22 21 adantr φ n k X A k + 1 n V
23 20 22 fvmpt2d φ n C n = k X A k + 1 n
24 23 feq1d φ n C n : X k X A k + 1 n : X
25 19 24 mpbird φ n C n : X
26 3 adantr φ n B : X
27 12 13 25 26 hoimbl φ n k X C n k B k dom voln X
28 27 8 fmptd φ D : dom voln X
29 nfv k φ n
30 oveq2 n = m 1 n = 1 m
31 30 oveq2d n = m A k + 1 n = A k + 1 m
32 31 mpteq2dv n = m k X A k + 1 n = k X A k + 1 m
33 32 cbvmptv n k X A k + 1 n = m k X A k + 1 m
34 7 33 eqtri C = m k X A k + 1 m
35 oveq2 m = n + 1 1 m = 1 n + 1
36 35 oveq2d m = n + 1 A k + 1 m = A k + 1 n + 1
37 36 mpteq2dv m = n + 1 k X A k + 1 m = k X A k + 1 n + 1
38 simpr φ n n
39 38 peano2nnd φ n n + 1
40 12 mptexd φ n k X A k + 1 n + 1 V
41 34 37 39 40 fvmptd3 φ n C n + 1 = k X A k + 1 n + 1
42 ovexd φ n k X A k + 1 n + 1 V
43 41 42 fvmpt2d φ n k X C n + 1 k = A k + 1 n + 1
44 1red n 1
45 nnre n n
46 45 44 readdcld n n + 1
47 peano2nn n n + 1
48 nnne0 n + 1 n + 1 0
49 47 48 syl n n + 1 0
50 44 46 49 redivcld n 1 n + 1
51 50 ad2antlr φ n k X 1 n + 1
52 15 51 readdcld φ n k X A k + 1 n + 1
53 43 52 eqeltrd φ n k X C n + 1 k
54 53 rexrd φ n k X C n + 1 k *
55 ressxr *
56 3 ffvelrnda φ k X B k
57 55 56 sseldi φ k X B k *
58 57 adantlr φ n k X B k *
59 45 ltp1d n n < n + 1
60 nnrp n n +
61 47 nnrpd n n + 1 +
62 60 61 ltrecd n n < n + 1 1 n + 1 < 1 n
63 59 62 mpbid n 1 n + 1 < 1 n
64 50 16 63 ltled n 1 n + 1 1 n
65 64 ad2antlr φ n k X 1 n + 1 1 n
66 51 17 15 65 leadd2dd φ n k X A k + 1 n + 1 A k + 1 n
67 ovexd φ n k X A k + 1 n V
68 23 67 fvmpt2d φ n k X C n k = A k + 1 n
69 43 68 breq12d φ n k X C n + 1 k C n k A k + 1 n + 1 A k + 1 n
70 66 69 mpbird φ n k X C n + 1 k C n k
71 56 adantlr φ n k X B k
72 eqidd φ n k X B k = B k
73 71 72 eqled φ n k X B k B k
74 icossico C n + 1 k * B k * C n + 1 k C n k B k B k C n k B k C n + 1 k B k
75 54 58 70 73 74 syl22anc φ n k X C n k B k C n + 1 k B k
76 29 75 ixpssixp φ n k X C n k B k k X C n + 1 k B k
77 8 a1i φ D = n k X C n k B k
78 27 elexd φ n k X C n k B k V
79 77 78 fvmpt2d φ n D n = k X C n k B k
80 fveq2 n = m C n = C m
81 80 fveq1d n = m C n k = C m k
82 81 oveq1d n = m C n k B k = C m k B k
83 82 ixpeq2dv n = m k X C n k B k = k X C m k B k
84 83 cbvmptv n k X C n k B k = m k X C m k B k
85 8 84 eqtri D = m k X C m k B k
86 fveq2 m = n + 1 C m = C n + 1
87 86 fveq1d m = n + 1 C m k = C n + 1 k
88 87 oveq1d m = n + 1 C m k B k = C n + 1 k B k
89 88 ixpeq2dv m = n + 1 k X C m k B k = k X C n + 1 k B k
90 ovex C n + 1 k B k V
91 90 rgenw k X C n + 1 k B k V
92 ixpexg k X C n + 1 k B k V k X C n + 1 k B k V
93 91 92 ax-mp k X C n + 1 k B k V
94 93 a1i φ n k X C n + 1 k B k V
95 85 89 39 94 fvmptd3 φ n D n + 1 = k X C n + 1 k B k
96 79 95 sseq12d φ n D n D n + 1 k X C n k B k k X C n + 1 k B k
97 76 96 mpbird φ n D n D n + 1
98 1 13 2 3 hoimbl φ k X A k B k dom voln X
99 nfv k φ
100 2 ffvelrnda φ k X A k
101 99 1 100 56 vonhoire φ voln X k X A k B k
102 6 a1i φ I = k X A k B k
103 nftru k
104 ioossico A k B k A k B k
105 104 a1i k X A k B k A k B k
106 103 105 ixpssixp k X A k B k k X A k B k
107 106 mptru k X A k B k k X A k B k
108 107 a1i φ k X A k B k k X A k B k
109 102 108 eqsstrd φ I k X A k B k
110 55 a1i φ *
111 2 110 fssd φ A : X *
112 3 110 fssd φ B : X *
113 1 13 111 112 ioovonmbl φ k X A k B k dom voln X
114 6 113 eqeltrid φ I dom voln X
115 9 98 101 109 114 meassre φ voln X I
116 9 adantr φ n voln X Meas
117 79 27 eqeltrd φ n D n dom voln X
118 114 adantr φ n I dom voln X
119 55 100 sseldi φ k X A k *
120 119 adantlr φ n k X A k *
121 60 rpreccld n 1 n +
122 121 ad2antlr φ n k X 1 n +
123 15 122 ltaddrpd φ n k X A k < A k + 1 n
124 icossioo A k * B k * A k < A k + 1 n B k B k A k + 1 n B k A k B k
125 120 58 123 73 124 syl22anc φ n k X A k + 1 n B k A k B k
126 29 125 ixpssixp φ n k X A k + 1 n B k k X A k B k
127 68 oveq1d φ n k X C n k B k = A k + 1 n B k
128 127 ixpeq2dva φ n k X C n k B k = k X A k + 1 n B k
129 79 128 eqtrd φ n D n = k X A k + 1 n B k
130 6 a1i φ n I = k X A k B k
131 129 130 sseq12d φ n D n I k X A k + 1 n B k k X A k B k
132 126 131 mpbird φ n D n I
133 116 13 117 118 132 meassle φ n voln X D n voln X I
134 eqid n voln X D n = n voln X D n
135 9 10 11 28 97 115 133 134 meaiuninc2 φ n voln X D n voln X n D n
136 99 1 100 57 iunhoiioo φ n k X A k + 1 n B k = k X A k B k
137 129 iuneq2dv φ n D n = n k X A k + 1 n B k
138 136 137 102 3eqtr4d φ n D n = I
139 138 eqcomd φ I = n D n
140 139 fveq2d φ voln X I = voln X n D n
141 140 eqcomd φ voln X n D n = voln X I
142 135 141 breqtrd φ n voln X D n voln X I
143 2fveq3 n = m voln X D n = voln X D m
144 143 cbvmptv n voln X D n = m voln X D m
145 144 a1i φ n voln X D n = m voln X D m
146 144 eqcomi m voln X D m = n voln X D n
147 eqcom n = m m = n
148 147 imbi1i n = m C n k = C m k m = n C n k = C m k
149 eqcom C n k = C m k C m k = C n k
150 149 imbi2i m = n C n k = C m k m = n C m k = C n k
151 148 150 bitri n = m C n k = C m k m = n C m k = C n k
152 81 151 mpbi m = n C m k = C n k
153 152 oveq2d m = n B k C m k = B k C n k
154 153 prodeq2ad m = n k X B k C m k = k X B k C n k
155 154 cbvmptv m k X B k C m k = n k X B k C n k
156 eqid sup ran k X B k A k < = sup ran k X B k A k <
157 eqid 1 sup ran k X B k A k < + 1 = 1 sup ran k X B k A k < + 1
158 fveq2 j = k B j = B k
159 fveq2 j = k A j = A k
160 158 159 oveq12d j = k B j A j = B k A k
161 160 cbvmptv j X B j A j = k X B k A k
162 161 rneqi ran j X B j A j = ran k X B k A k
163 162 infeq1i sup ran j X B j A j < = sup ran k X B k A k <
164 163 oveq2i 1 sup ran j X B j A j < = 1 sup ran k X B k A k <
165 164 fveq2i 1 sup ran j X B j A j < = 1 sup ran k X B k A k <
166 165 oveq1i 1 sup ran j X B j A j < + 1 = 1 sup ran k X B k A k < + 1
167 166 fveq2i 1 sup ran j X B j A j < + 1 = 1 sup ran k X B k A k < + 1
168 1 2 3 4 5 7 8 146 155 156 157 167 vonioolem1 φ m voln X D m k X B k A k
169 145 168 eqbrtrd φ n voln X D n k X B k A k
170 climuni n voln X D n voln X I n voln X D n k X B k A k voln X I = k X B k A k
171 142 169 170 syl2anc φ voln X I = k X B k A k