Metamath Proof Explorer


Theorem vonioolem1

Description: The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses vonioolem1.x φ X Fin
vonioolem1.a φ A : X
vonioolem1.b φ B : X
vonioolem1.u φ X
vonioolem1.t φ k X A k < B k
vonioolem1.c C = n k X A k + 1 n
vonioolem1.d D = n k X C n k B k
vonioolem1.s S = n voln X D n
vonioolem1.r T = n k X B k C n k
vonioolem1.e E = sup ran k X B k A k <
vonioolem1.n N = 1 E + 1
vonioolem1.z Z = N
Assertion vonioolem1 φ S k X B k A k

Proof

Step Hyp Ref Expression
1 vonioolem1.x φ X Fin
2 vonioolem1.a φ A : X
3 vonioolem1.b φ B : X
4 vonioolem1.u φ X
5 vonioolem1.t φ k X A k < B k
6 vonioolem1.c C = n k X A k + 1 n
7 vonioolem1.d D = n k X C n k B k
8 vonioolem1.s S = n voln X D n
9 vonioolem1.r T = n k X B k C n k
10 vonioolem1.e E = sup ran k X B k A k <
11 vonioolem1.n N = 1 E + 1
12 vonioolem1.z Z = N
13 9 a1i φ T = n k X B k C n k
14 6 a1i φ C = n k X A k + 1 n
15 1 mptexd φ k X A k + 1 n V
16 15 adantr φ n k X A k + 1 n V
17 14 16 fvmpt2d φ n C n = k X A k + 1 n
18 ovexd φ n k X A k + 1 n V
19 17 18 fvmpt2d φ n k X C n k = A k + 1 n
20 19 oveq2d φ n k X B k C n k = B k A k + 1 n
21 3 ffvelrnda φ k X B k
22 21 adantlr φ n k X B k
23 22 recnd φ n k X B k
24 2 adantr φ n A : X
25 24 ffvelrnda φ n k X A k
26 25 recnd φ n k X A k
27 nnrecre n 1 n
28 27 ad2antlr φ n k X 1 n
29 28 recnd φ n k X 1 n
30 23 26 29 subsub4d φ n k X B k - A k - 1 n = B k A k + 1 n
31 20 30 eqtr4d φ n k X B k C n k = B k - A k - 1 n
32 31 prodeq2dv φ n k X B k C n k = k X B k - A k - 1 n
33 32 mpteq2dva φ n k X B k C n k = n k X B k - A k - 1 n
34 13 33 eqtrd φ T = n k X B k - A k - 1 n
35 nfv k φ
36 rpssre +
37 2 ffvelrnda φ k X A k
38 difrp A k B k A k < B k B k A k +
39 37 21 38 syl2anc φ k X A k < B k B k A k +
40 5 39 mpbid φ k X B k A k +
41 36 40 sselid φ k X B k A k
42 41 recnd φ k X B k A k
43 eqid n k X B k - A k - 1 n = n k X B k - A k - 1 n
44 35 1 42 43 fprodsubrecnncnv φ n k X B k - A k - 1 n k X B k A k
45 34 44 eqbrtrd φ T k X B k A k
46 nnex V
47 46 mptex n k X B k C n k V
48 47 a1i φ n k X B k C n k V
49 9 48 eqeltrid φ T V
50 46 mptex n voln X D n V
51 50 a1i φ n voln X D n V
52 8 51 eqeltrid φ S V
53 1rp 1 +
54 53 a1i φ 1 +
55 eqid k X B k A k = k X B k A k
56 35 55 40 rnmptssd φ ran k X B k A k +
57 ltso < Or
58 57 a1i φ < Or
59 55 rnmptfi X Fin ran k X B k A k Fin
60 1 59 syl φ ran k X B k A k Fin
61 35 40 55 4 rnmptn0 φ ran k X B k A k
62 36 a1i φ +
63 56 62 sstrd φ ran k X B k A k
64 fiinfcl < Or ran k X B k A k Fin ran k X B k A k ran k X B k A k sup ran k X B k A k < ran k X B k A k
65 58 60 61 63 64 syl13anc φ sup ran k X B k A k < ran k X B k A k
66 10 65 eqeltrid φ E ran k X B k A k
67 56 66 sseldd φ E +
68 54 67 rpdivcld φ 1 E +
69 68 rpred φ 1 E
70 68 rpge0d φ 0 1 E
71 flge0nn0 1 E 0 1 E 1 E 0
72 69 70 71 syl2anc φ 1 E 0
73 nn0p1nn 1 E 0 1 E + 1
74 72 73 syl φ 1 E + 1
75 74 nnzd φ 1 E + 1
76 11 75 eqeltrid φ N
77 11 recnnltrp E + N 1 N < E
78 67 77 syl φ N 1 N < E
79 78 simpld φ N
80 uznnssnn N N
81 79 80 syl φ N
82 12 81 eqsstrid φ Z
83 82 adantr φ n Z Z
84 simpr φ n Z n Z
85 83 84 sseldd φ n Z n
86 7 a1i φ D = n k X C n k B k
87 1 adantr φ n X Fin
88 eqid dom voln X = dom voln X
89 25 28 readdcld φ n k X A k + 1 n
90 89 fmpttd φ n k X A k + 1 n : X
91 17 feq1d φ n C n : X k X A k + 1 n : X
92 90 91 mpbird φ n C n : X
93 3 adantr φ n B : X
94 87 88 92 93 hoimbl φ n k X C n k B k dom voln X
95 94 elexd φ n k X C n k B k V
96 86 95 fvmpt2d φ n D n = k X C n k B k
97 85 96 syldan φ n Z D n = k X C n k B k
98 97 fveq2d φ n Z voln X D n = voln X k X C n k B k
99 1 adantr φ n Z X Fin
100 4 adantr φ n Z X
101 85 92 syldan φ n Z C n : X
102 3 adantr φ n Z B : X
103 eqid k X C n k B k = k X C n k B k
104 99 100 101 102 103 vonn0hoi φ n Z voln X k X C n k B k = k X vol C n k B k
105 101 ffvelrnda φ n Z k X C n k
106 85 22 syldanl φ n Z k X B k
107 volico C n k B k vol C n k B k = if C n k < B k B k C n k 0
108 105 106 107 syl2anc φ n Z k X vol C n k B k = if C n k < B k B k C n k 0
109 85 19 syldanl φ n Z k X C n k = A k + 1 n
110 85 28 syldanl φ n Z k X 1 n
111 79 nnrecred φ 1 N
112 111 ad2antrr φ n Z k X 1 N
113 41 adantlr φ n Z k X B k A k
114 12 eleq2i n Z n N
115 114 biimpi n Z n N
116 eluzle n N N n
117 115 116 syl n Z N n
118 117 adantl φ n Z N n
119 79 nnrpd φ N +
120 119 adantr φ n Z N +
121 nnrp n n +
122 85 121 syl φ n Z n +
123 120 122 lerecd φ n Z N n 1 n 1 N
124 118 123 mpbid φ n Z 1 n 1 N
125 124 adantr φ n Z k X 1 n 1 N
126 111 adantr φ k X 1 N
127 36 67 sselid φ E
128 127 adantr φ k X E
129 78 simprd φ 1 N < E
130 129 adantr φ k X 1 N < E
131 63 adantr φ k X ran k X B k A k
132 60 adantr φ k X ran k X B k A k Fin
133 id k X k X
134 ovexd k X B k A k V
135 55 elrnmpt1 k X B k A k V B k A k ran k X B k A k
136 133 134 135 syl2anc k X B k A k ran k X B k A k
137 136 adantl φ k X B k A k ran k X B k A k
138 infrefilb ran k X B k A k ran k X B k A k Fin B k A k ran k X B k A k sup ran k X B k A k < B k A k
139 131 132 137 138 syl3anc φ k X sup ran k X B k A k < B k A k
140 10 139 eqbrtrid φ k X E B k A k
141 126 128 41 130 140 ltletrd φ k X 1 N < B k A k
142 141 adantlr φ n Z k X 1 N < B k A k
143 110 112 113 125 142 lelttrd φ n Z k X 1 n < B k A k
144 85 25 syldanl φ n Z k X A k
145 144 110 106 ltaddsub2d φ n Z k X A k + 1 n < B k 1 n < B k A k
146 143 145 mpbird φ n Z k X A k + 1 n < B k
147 109 146 eqbrtrd φ n Z k X C n k < B k
148 147 iftrued φ n Z k X if C n k < B k B k C n k 0 = B k C n k
149 108 148 eqtrd φ n Z k X vol C n k B k = B k C n k
150 149 prodeq2dv φ n Z k X vol C n k B k = k X B k C n k
151 98 104 150 3eqtrd φ n Z voln X D n = k X B k C n k
152 fvexd φ n Z voln X D n V
153 8 fvmpt2 n voln X D n V S n = voln X D n
154 85 152 153 syl2anc φ n Z S n = voln X D n
155 prodex k X B k C n k V
156 155 a1i φ n Z k X B k C n k V
157 9 fvmpt2 n k X B k C n k V T n = k X B k C n k
158 85 156 157 syl2anc φ n Z T n = k X B k C n k
159 151 154 158 3eqtr4rd φ n Z T n = S n
160 12 49 52 76 159 climeq φ T k X B k A k S k X B k A k
161 45 160 mpbid φ S k X B k A k