Metamath Proof Explorer


Theorem iccvonmbllem

Description: Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iccvonmbllem.x φXFin
iccvonmbllem.s S=domvolnX
iccvonmbllem.a φA:X
iccvonmbllem.b φB:X
iccvonmbllem.c C=niXAi1n
iccvonmbllem.d D=niXBi+1n
Assertion iccvonmbllem φiXAiBiS

Proof

Step Hyp Ref Expression
1 iccvonmbllem.x φXFin
2 iccvonmbllem.s S=domvolnX
3 iccvonmbllem.a φA:X
4 iccvonmbllem.b φB:X
5 iccvonmbllem.c C=niXAi1n
6 iccvonmbllem.d D=niXBi+1n
7 5 a1i φC=niXAi1n
8 1 adantr φnXFin
9 8 mptexd φniXAi1nV
10 7 9 fvmpt2d φnCn=iXAi1n
11 3 ffvelrnda φiXAi
12 11 adantlr φniXAi
13 nnrecre n1n
14 13 ad2antlr φniX1n
15 12 14 resubcld φniXAi1n
16 10 15 fvmpt2d φniXCni=Ai1n
17 16 an32s φiXnCni=Ai1n
18 6 a1i φD=niXBi+1n
19 8 mptexd φniXBi+1nV
20 18 19 fvmpt2d φnDn=iXBi+1n
21 4 ffvelrnda φiXBi
22 21 adantlr φniXBi
23 22 14 readdcld φniXBi+1n
24 20 23 fvmpt2d φniXDni=Bi+1n
25 24 an32s φiXnDni=Bi+1n
26 17 25 oveq12d φiXnCniDni=Ai1nBi+1n
27 26 iineq2dv φiXnCniDni=nAi1nBi+1n
28 11 21 iooiinicc φiXnAi1nBi+1n=AiBi
29 27 28 eqtrd φiXnCniDni=AiBi
30 29 ixpeq2dva φiXnCniDni=iXAiBi
31 30 eqcomd φiXAiBi=iXnCniDni
32 eqidd φiXAiBi=iXAiBi
33 nnn0
34 33 a1i φ
35 ixpiin iXnCniDni=niXCniDni
36 34 35 syl φiXnCniDni=niXCniDni
37 31 32 36 3eqtr3d φiXAiBi=niXCniDni
38 1 2 dmovnsal φSSAlg
39 nnct ω
40 39 a1i φω
41 15 fmpttd φniXAi1n:X
42 ressxr *
43 42 a1i φn*
44 41 43 fssd φniXAi1n:X*
45 10 feq1d φnCn:X*iXAi1n:X*
46 44 45 mpbird φnCn:X*
47 23 fmpttd φniXBi+1n:X
48 47 43 fssd φniXBi+1n:X*
49 20 feq1d φnDn:X*iXBi+1n:X*
50 48 49 mpbird φnDn:X*
51 8 2 46 50 ioovonmbl φniXCniDniS
52 38 40 34 51 saliincl φniXCniDniS
53 37 52 eqeltrd φiXAiBiS