Metamath Proof Explorer


Theorem uniioovol

Description: A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) Lemma 565Ca of Fremlin5 p. 213. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
Assertion uniioovol φ vol * ran . F = sup ran S * <

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 ioof . : * × * 𝒫
5 inss2 2 2
6 rexpssxrxp 2 * × *
7 5 6 sstri 2 * × *
8 fss F : 2 2 * × * F : * × *
9 1 7 8 sylancl φ F : * × *
10 fco . : * × * 𝒫 F : * × * . F : 𝒫
11 4 9 10 sylancr φ . F : 𝒫
12 11 frnd φ ran . F 𝒫
13 sspwuni ran . F 𝒫 ran . F
14 12 13 sylib φ ran . F
15 ovolcl ran . F vol * ran . F *
16 14 15 syl φ vol * ran . F *
17 eqid abs F = abs F
18 17 3 ovolsf F : 2 S : 0 +∞
19 frn S : 0 +∞ ran S 0 +∞
20 1 18 19 3syl φ ran S 0 +∞
21 icossxr 0 +∞ *
22 20 21 sstrdi φ ran S *
23 supxrcl ran S * sup ran S * < *
24 22 23 syl φ sup ran S * < *
25 ssid ran . F ran . F
26 3 ovollb F : 2 ran . F ran . F vol * ran . F sup ran S * <
27 1 25 26 sylancl φ vol * ran . F sup ran S * <
28 1 adantr φ n F : 2
29 elfznn x 1 n x
30 17 ovolfsval F : 2 x abs F x = 2 nd F x 1 st F x
31 28 29 30 syl2an φ n x 1 n abs F x = 2 nd F x 1 st F x
32 fvco3 F : 2 x . F x = . F x
33 28 29 32 syl2an φ n x 1 n . F x = . F x
34 ffvelrn F : 2 x F x 2
35 28 29 34 syl2an φ n x 1 n F x 2
36 35 elin2d φ n x 1 n F x 2
37 1st2nd2 F x 2 F x = 1 st F x 2 nd F x
38 36 37 syl φ n x 1 n F x = 1 st F x 2 nd F x
39 38 fveq2d φ n x 1 n . F x = . 1 st F x 2 nd F x
40 df-ov 1 st F x 2 nd F x = . 1 st F x 2 nd F x
41 39 40 syl6eqr φ n x 1 n . F x = 1 st F x 2 nd F x
42 33 41 eqtrd φ n x 1 n . F x = 1 st F x 2 nd F x
43 ioombl 1 st F x 2 nd F x dom vol
44 42 43 eqeltrdi φ n x 1 n . F x dom vol
45 mblvol . F x dom vol vol . F x = vol * . F x
46 44 45 syl φ n x 1 n vol . F x = vol * . F x
47 42 fveq2d φ n x 1 n vol * . F x = vol * 1 st F x 2 nd F x
48 ovolfcl F : 2 x 1 st F x 2 nd F x 1 st F x 2 nd F x
49 28 29 48 syl2an φ n x 1 n 1 st F x 2 nd F x 1 st F x 2 nd F x
50 ovolioo 1 st F x 2 nd F x 1 st F x 2 nd F x vol * 1 st F x 2 nd F x = 2 nd F x 1 st F x
51 49 50 syl φ n x 1 n vol * 1 st F x 2 nd F x = 2 nd F x 1 st F x
52 46 47 51 3eqtrd φ n x 1 n vol . F x = 2 nd F x 1 st F x
53 31 52 eqtr4d φ n x 1 n abs F x = vol . F x
54 simpr φ n n
55 nnuz = 1
56 54 55 eleqtrdi φ n n 1
57 49 simp2d φ n x 1 n 2 nd F x
58 49 simp1d φ n x 1 n 1 st F x
59 57 58 resubcld φ n x 1 n 2 nd F x 1 st F x
60 52 59 eqeltrd φ n x 1 n vol . F x
61 60 recnd φ n x 1 n vol . F x
62 53 56 61 fsumser φ n x = 1 n vol . F x = seq 1 + abs F n
63 3 fveq1i S n = seq 1 + abs F n
64 62 63 syl6reqr φ n S n = x = 1 n vol . F x
65 fzfid φ n 1 n Fin
66 44 60 jca φ n x 1 n . F x dom vol vol . F x
67 66 ralrimiva φ n x 1 n . F x dom vol vol . F x
68 fz1ssnn 1 n
69 1 32 sylan φ x . F x = . F x
70 69 disjeq2dv φ Disj x . F x Disj x . F x
71 2 70 mpbird φ Disj x . F x
72 71 adantr φ n Disj x . F x
73 disjss1 1 n Disj x . F x Disj x = 1 n . F x
74 68 72 73 mpsyl φ n Disj x = 1 n . F x
75 volfiniun 1 n Fin x 1 n . F x dom vol vol . F x Disj x = 1 n . F x vol x = 1 n . F x = x = 1 n vol . F x
76 65 67 74 75 syl3anc φ n vol x = 1 n . F x = x = 1 n vol . F x
77 44 ralrimiva φ n x 1 n . F x dom vol
78 finiunmbl 1 n Fin x 1 n . F x dom vol x = 1 n . F x dom vol
79 65 77 78 syl2anc φ n x = 1 n . F x dom vol
80 mblvol x = 1 n . F x dom vol vol x = 1 n . F x = vol * x = 1 n . F x
81 79 80 syl φ n vol x = 1 n . F x = vol * x = 1 n . F x
82 64 76 81 3eqtr2d φ n S n = vol * x = 1 n . F x
83 iunss1 1 n x = 1 n . F x x . F x
84 68 83 mp1i φ n x = 1 n . F x x . F x
85 11 adantr φ n . F : 𝒫
86 ffn . F : 𝒫 . F Fn
87 fniunfv . F Fn x . F x = ran . F
88 85 86 87 3syl φ n x . F x = ran . F
89 84 88 sseqtrd φ n x = 1 n . F x ran . F
90 14 adantr φ n ran . F
91 ovolss x = 1 n . F x ran . F ran . F vol * x = 1 n . F x vol * ran . F
92 89 90 91 syl2anc φ n vol * x = 1 n . F x vol * ran . F
93 82 92 eqbrtrd φ n S n vol * ran . F
94 93 ralrimiva φ n S n vol * ran . F
95 1 18 syl φ S : 0 +∞
96 ffn S : 0 +∞ S Fn
97 breq1 y = S n y vol * ran . F S n vol * ran . F
98 97 ralrn S Fn y ran S y vol * ran . F n S n vol * ran . F
99 95 96 98 3syl φ y ran S y vol * ran . F n S n vol * ran . F
100 94 99 mpbird φ y ran S y vol * ran . F
101 supxrleub ran S * vol * ran . F * sup ran S * < vol * ran . F y ran S y vol * ran . F
102 22 16 101 syl2anc φ sup ran S * < vol * ran . F y ran S y vol * ran . F
103 100 102 mpbird φ sup ran S * < vol * ran . F
104 16 24 27 103 xrletrid φ vol * ran . F = sup ran S * <