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 | |
|
iccvonmbllem.s | |
||
iccvonmbllem.a | |
||
iccvonmbllem.b | |
||
iccvonmbllem.c | |
||
iccvonmbllem.d | |
||
Assertion | iccvonmbllem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccvonmbllem.x | |
|
2 | iccvonmbllem.s | |
|
3 | iccvonmbllem.a | |
|
4 | iccvonmbllem.b | |
|
5 | iccvonmbllem.c | |
|
6 | iccvonmbllem.d | |
|
7 | 5 | a1i | |
8 | 1 | adantr | |
9 | 8 | mptexd | |
10 | 7 9 | fvmpt2d | |
11 | 3 | ffvelrnda | |
12 | 11 | adantlr | |
13 | nnrecre | |
|
14 | 13 | ad2antlr | |
15 | 12 14 | resubcld | |
16 | 10 15 | fvmpt2d | |
17 | 16 | an32s | |
18 | 6 | a1i | |
19 | 8 | mptexd | |
20 | 18 19 | fvmpt2d | |
21 | 4 | ffvelrnda | |
22 | 21 | adantlr | |
23 | 22 14 | readdcld | |
24 | 20 23 | fvmpt2d | |
25 | 24 | an32s | |
26 | 17 25 | oveq12d | |
27 | 26 | iineq2dv | |
28 | 11 21 | iooiinicc | |
29 | 27 28 | eqtrd | |
30 | 29 | ixpeq2dva | |
31 | 30 | eqcomd | |
32 | eqidd | |
|
33 | nnn0 | |
|
34 | 33 | a1i | |
35 | ixpiin | |
|
36 | 34 35 | syl | |
37 | 31 32 36 | 3eqtr3d | |
38 | 1 2 | dmovnsal | |
39 | nnct | |
|
40 | 39 | a1i | |
41 | 15 | fmpttd | |
42 | ressxr | |
|
43 | 42 | a1i | |
44 | 41 43 | fssd | |
45 | 10 | feq1d | |
46 | 44 45 | mpbird | |
47 | 23 | fmpttd | |
48 | 47 43 | fssd | |
49 | 20 | feq1d | |
50 | 48 49 | mpbird | |
51 | 8 2 46 50 | ioovonmbl | |
52 | 38 40 34 51 | saliincl | |
53 | 37 52 | eqeltrd | |