# Metamath Proof Explorer

## Theorem vitalilem4

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1
vitali.2
vitali.3 ${⊢}{\phi }\to {F}Fn{S}$
vitali.4 ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)$
vitali.5 ${⊢}{\phi }\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
vitali.6 ${⊢}{T}=\left({n}\in ℕ⟼\left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\right)$
vitali.7 ${⊢}{\phi }\to ¬\mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)$
Assertion vitalilem4 ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left({T}\left({m}\right)\right)=0$

### Proof

Step Hyp Ref Expression
1 vitali.1
2 vitali.2
3 vitali.3 ${⊢}{\phi }\to {F}Fn{S}$
4 vitali.4 ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)$
5 vitali.5 ${⊢}{\phi }\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
6 vitali.6 ${⊢}{T}=\left({n}\in ℕ⟼\left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\right)$
7 vitali.7 ${⊢}{\phi }\to ¬\mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)$
8 fveq2 ${⊢}{n}={m}\to {G}\left({n}\right)={G}\left({m}\right)$
9 8 oveq2d ${⊢}{n}={m}\to {s}-{G}\left({n}\right)={s}-{G}\left({m}\right)$
10 9 eleq1d ${⊢}{n}={m}\to \left({s}-{G}\left({n}\right)\in \mathrm{ran}{F}↔{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
11 10 rabbidv ${⊢}{n}={m}\to \left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
12 reex ${⊢}ℝ\in \mathrm{V}$
13 12 rabex ${⊢}\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{V}$
14 11 6 13 fvmpt ${⊢}{m}\in ℕ\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
15 14 adantl ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
16 15 fveq2d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left({T}\left({m}\right)\right)={vol}^{*}\left(\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\right)$
17 1 2 3 4 5 6 7 vitalilem2 ${⊢}{\phi }\to \left(\mathrm{ran}{F}\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq \bigcup _{{m}\in ℕ}{T}\left({m}\right)\wedge \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]\right)$
18 17 simp1d ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \left[0,1\right]$
19 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
20 18 19 sstrdi ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq ℝ$
21 20 adantr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \mathrm{ran}{F}\subseteq ℝ$
22 neg1rr ${⊢}-1\in ℝ$
23 1re ${⊢}1\in ℝ$
24 iccssre ${⊢}\left(-1\in ℝ\wedge 1\in ℝ\right)\to \left[-1,1\right]\subseteq ℝ$
25 22 23 24 mp2an ${⊢}\left[-1,1\right]\subseteq ℝ$
26 f1of ${⊢}{G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
27 5 26 syl ${⊢}{\phi }\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
28 27 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in \left(ℚ\cap \left[-1,1\right]\right)$
29 28 elin2d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in \left[-1,1\right]$
30 25 29 sseldi ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in ℝ$
31 eqidd ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
32 21 30 31 ovolshft ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)={vol}^{*}\left(\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\right)$
33 16 32 eqtr4d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left({T}\left({m}\right)\right)={vol}^{*}\left(\mathrm{ran}{F}\right)$
34 3re ${⊢}3\in ℝ$
35 34 rexri ${⊢}3\in {ℝ}^{*}$
36 35 a1i ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 3\in {ℝ}^{*}$
37 3rp ${⊢}3\in {ℝ}^{+}$
38 0re ${⊢}0\in ℝ$
39 0le1 ${⊢}0\le 1$
40 ovolicc ${⊢}\left(0\in ℝ\wedge 1\in ℝ\wedge 0\le 1\right)\to {vol}^{*}\left(\left[0,1\right]\right)=1-0$
41 38 23 39 40 mp3an ${⊢}{vol}^{*}\left(\left[0,1\right]\right)=1-0$
42 1m0e1 ${⊢}1-0=1$
43 41 42 eqtri ${⊢}{vol}^{*}\left(\left[0,1\right]\right)=1$
44 43 23 eqeltri ${⊢}{vol}^{*}\left(\left[0,1\right]\right)\in ℝ$
45 ovolsscl ${⊢}\left(\mathrm{ran}{F}\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq ℝ\wedge {vol}^{*}\left(\left[0,1\right]\right)\in ℝ\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
46 19 44 45 mp3an23 ${⊢}\mathrm{ran}{F}\subseteq \left[0,1\right]\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
47 18 46 syl ${⊢}{\phi }\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
48 47 adantr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
49 simpr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 0<{vol}^{*}\left(\mathrm{ran}{F}\right)$
50 48 49 elrpd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{+}$
51 rpdivcl ${⊢}\left(3\in {ℝ}^{+}\wedge {vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{+}\right)\to \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\in {ℝ}^{+}$
52 37 50 51 sylancr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\in {ℝ}^{+}$
53 52 rpred ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\in ℝ$
54 52 rpge0d ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 0\le \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}$
55 flge0nn0 ${⊢}\left(\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\in ℝ\wedge 0\le \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\right)\to ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋\in {ℕ}_{0}$
56 53 54 55 syl2anc ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋\in {ℕ}_{0}$
57 nn0p1nn ${⊢}⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋\in {ℕ}_{0}\to ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\in ℕ$
58 56 57 syl ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\in ℕ$
59 58 nnred ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\in ℝ$
60 59 48 remulcld ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
61 60 rexrd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{*}$
62 12 elpw2 ${⊢}\mathrm{ran}{F}\in 𝒫ℝ↔\mathrm{ran}{F}\subseteq ℝ$
63 20 62 sylibr ${⊢}{\phi }\to \mathrm{ran}{F}\in 𝒫ℝ$
64 63 anim1i ${⊢}\left({\phi }\wedge ¬\mathrm{ran}{F}\in \mathrm{dom}vol\right)\to \left(\mathrm{ran}{F}\in 𝒫ℝ\wedge ¬\mathrm{ran}{F}\in \mathrm{dom}vol\right)$
65 eldif ${⊢}\mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)↔\left(\mathrm{ran}{F}\in 𝒫ℝ\wedge ¬\mathrm{ran}{F}\in \mathrm{dom}vol\right)$
66 64 65 sylibr ${⊢}\left({\phi }\wedge ¬\mathrm{ran}{F}\in \mathrm{dom}vol\right)\to \mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)$
67 66 ex ${⊢}{\phi }\to \left(¬\mathrm{ran}{F}\in \mathrm{dom}vol\to \mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)\right)$
68 7 67 mt3d ${⊢}{\phi }\to \mathrm{ran}{F}\in \mathrm{dom}vol$
69 inss1 ${⊢}ℚ\cap \left[-1,1\right]\subseteq ℚ$
70 qssre ${⊢}ℚ\subseteq ℝ$
71 69 70 sstri ${⊢}ℚ\cap \left[-1,1\right]\subseteq ℝ$
72 fss ${⊢}\left({G}:ℕ⟶ℚ\cap \left[-1,1\right]\wedge ℚ\cap \left[-1,1\right]\subseteq ℝ\right)\to {G}:ℕ⟶ℝ$
73 27 71 72 sylancl ${⊢}{\phi }\to {G}:ℕ⟶ℝ$
74 73 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\left({n}\right)\in ℝ$
75 shftmbl ${⊢}\left(\mathrm{ran}{F}\in \mathrm{dom}vol\wedge {G}\left({n}\right)\in ℝ\right)\to \left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{dom}vol$
76 68 74 75 syl2an2r ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{dom}vol$
77 76 6 fmptd ${⊢}{\phi }\to {T}:ℕ⟶\mathrm{dom}vol$
78 77 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {T}\left({m}\right)\in \mathrm{dom}vol$
79 78 ralrimiva ${⊢}{\phi }\to \forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\in \mathrm{dom}vol$
80 iunmbl ${⊢}\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}{T}\left({m}\right)\in \mathrm{dom}vol\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\in \mathrm{dom}vol$
81 79 80 syl ${⊢}{\phi }\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\in \mathrm{dom}vol$
82 mblss ${⊢}\bigcup _{{m}\in ℕ}{T}\left({m}\right)\in \mathrm{dom}vol\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq ℝ$
83 ovolcl ${⊢}\bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq ℝ\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\in {ℝ}^{*}$
84 81 82 83 3syl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\in {ℝ}^{*}$
85 84 adantr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\in {ℝ}^{*}$
86 flltp1 ${⊢}\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}\in ℝ\to \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}<⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1$
87 53 86 syl ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}<⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1$
88 34 a1i ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 3\in ℝ$
89 88 59 50 ltdivmul2d ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}<⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1↔3<\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\right)$
90 87 89 mpbid ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 3<\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)$
91 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
92 1zzd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 1\in ℤ$
93 mblvol ${⊢}{T}\left({m}\right)\in \mathrm{dom}vol\to vol\left({T}\left({m}\right)\right)={vol}^{*}\left({T}\left({m}\right)\right)$
94 78 93 syl ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to vol\left({T}\left({m}\right)\right)={vol}^{*}\left({T}\left({m}\right)\right)$
95 94 33 eqtrd ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to vol\left({T}\left({m}\right)\right)={vol}^{*}\left(\mathrm{ran}{F}\right)$
96 47 adantr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℝ$
97 95 96 eqeltrd ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to vol\left({T}\left({m}\right)\right)\in ℝ$
98 97 adantlr ${⊢}\left(\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\wedge {m}\in ℕ\right)\to vol\left({T}\left({m}\right)\right)\in ℝ$
99 eqid ${⊢}\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)=\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)$
100 98 99 fmptd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right):ℕ⟶ℝ$
101 100 ffvelrnda ${⊢}\left(\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\wedge {k}\in ℕ\right)\to \left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\left({k}\right)\in ℝ$
102 91 92 101 serfre ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right):ℕ⟶ℝ$
103 102 frnd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\subseteq ℝ$
104 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
105 103 104 sstrdi ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\subseteq {ℝ}^{*}$
106 95 adantlr ${⊢}\left(\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\wedge {m}\in ℕ\right)\to vol\left({T}\left({m}\right)\right)={vol}^{*}\left(\mathrm{ran}{F}\right)$
107 106 mpteq2dva ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)=\left({m}\in ℕ⟼{vol}^{*}\left(\mathrm{ran}{F}\right)\right)$
108 fconstmpt ${⊢}ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}=\left({m}\in ℕ⟼{vol}^{*}\left(\mathrm{ran}{F}\right)\right)$
109 107 108 syl6eqr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)=ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}$
110 109 seqeq3d ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)=seq1\left(+,\left(ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}\right)\right)$
111 110 fveq1d ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)=seq1\left(+,\left(ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)$
112 48 recnd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in ℂ$
113 ser1const ${⊢}\left({vol}^{*}\left(\mathrm{ran}{F}\right)\in ℂ\wedge ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\in ℕ\right)\to seq1\left(+,\left(ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)=\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)$
114 112 58 113 syl2anc ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left(ℕ×\left\{{vol}^{*}\left(\mathrm{ran}{F}\right)\right\}\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)=\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)$
115 111 114 eqtrd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)=\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)$
116 102 ffnd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)Fnℕ$
117 fnfvelrn ${⊢}\left(seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)Fnℕ\wedge ⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\in ℕ\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)\in \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)$
118 116 58 117 syl2anc ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right)\in \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)$
119 115 118 eqeltrrd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\in \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)$
120 supxrub ${⊢}\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\subseteq {ℝ}^{*}\wedge \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\in \mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\le sup\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right),{ℝ}^{*},<\right)$
121 105 119 120 syl2anc ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\le sup\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right),{ℝ}^{*},<\right)$
122 81 adantr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\in \mathrm{dom}vol$
123 mblvol ${⊢}\bigcup _{{m}\in ℕ}{T}\left({m}\right)\in \mathrm{dom}vol\to vol\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)={vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
124 122 123 syl ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to vol\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)={vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
125 78 97 jca ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \left({T}\left({m}\right)\in \mathrm{dom}vol\wedge vol\left({T}\left({m}\right)\right)\in ℝ\right)$
126 125 ralrimiva ${⊢}{\phi }\to \forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({T}\left({m}\right)\in \mathrm{dom}vol\wedge vol\left({T}\left({m}\right)\right)\in ℝ\right)$
127 1 2 3 4 5 6 7 vitalilem3 ${⊢}{\phi }\to \underset{{m}\in ℕ}{Disj}{T}\left({m}\right)$
128 127 adantr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \underset{{m}\in ℕ}{Disj}{T}\left({m}\right)$
129 eqid ${⊢}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)=seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right)$
130 129 99 voliun ${⊢}\left(\forall {m}\in ℕ\phantom{\rule{.4em}{0ex}}\left({T}\left({m}\right)\in \mathrm{dom}vol\wedge vol\left({T}\left({m}\right)\right)\in ℝ\right)\wedge \underset{{m}\in ℕ}{Disj}{T}\left({m}\right)\right)\to vol\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)=sup\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right),{ℝ}^{*},<\right)$
131 126 128 130 syl2an2r ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to vol\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)=sup\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right),{ℝ}^{*},<\right)$
132 124 131 eqtr3d ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)=sup\left(\mathrm{ran}seq1\left(+,\left({m}\in ℕ⟼vol\left({T}\left({m}\right)\right)\right)\right),{ℝ}^{*},<\right)$
133 121 132 breqtrrd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left(⌊\frac{3}{{vol}^{*}\left(\mathrm{ran}{F}\right)}⌋+1\right){vol}^{*}\left(\mathrm{ran}{F}\right)\le {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
134 36 61 85 90 133 xrltletrd ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to 3<{vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
135 17 simp3d ${⊢}{\phi }\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]$
136 135 adantr ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]$
137 2re ${⊢}2\in ℝ$
138 iccssre ${⊢}\left(-1\in ℝ\wedge 2\in ℝ\right)\to \left[-1,2\right]\subseteq ℝ$
139 22 137 138 mp2an ${⊢}\left[-1,2\right]\subseteq ℝ$
140 ovolss ${⊢}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]\wedge \left[-1,2\right]\subseteq ℝ\right)\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\le {vol}^{*}\left(\left[-1,2\right]\right)$
141 136 139 140 sylancl ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\le {vol}^{*}\left(\left[-1,2\right]\right)$
142 2cn ${⊢}2\in ℂ$
143 ax-1cn ${⊢}1\in ℂ$
144 142 143 subnegi ${⊢}2--1=2+1$
145 neg1lt0 ${⊢}-1<0$
146 2pos ${⊢}0<2$
147 22 38 137 lttri ${⊢}\left(-1<0\wedge 0<2\right)\to -1<2$
148 145 146 147 mp2an ${⊢}-1<2$
149 22 137 148 ltleii ${⊢}-1\le 2$
150 ovolicc ${⊢}\left(-1\in ℝ\wedge 2\in ℝ\wedge -1\le 2\right)\to {vol}^{*}\left(\left[-1,2\right]\right)=2--1$
151 22 137 149 150 mp3an ${⊢}{vol}^{*}\left(\left[-1,2\right]\right)=2--1$
152 df-3 ${⊢}3=2+1$
153 144 151 152 3eqtr4i ${⊢}{vol}^{*}\left(\left[-1,2\right]\right)=3$
154 141 153 breqtrdi ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to {vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\le 3$
155 xrlenlt ${⊢}\left({vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\in {ℝ}^{*}\wedge 3\in {ℝ}^{*}\right)\to \left({vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\le 3↔¬3<{vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\right)$
156 85 35 155 sylancl ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to \left({vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\le 3↔¬3<{vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)\right)$
157 154 156 mpbid ${⊢}\left({\phi }\wedge 0<{vol}^{*}\left(\mathrm{ran}{F}\right)\right)\to ¬3<{vol}^{*}\left(\bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
158 134 157 pm2.65da ${⊢}{\phi }\to ¬0<{vol}^{*}\left(\mathrm{ran}{F}\right)$
159 ovolge0 ${⊢}\mathrm{ran}{F}\subseteq ℝ\to 0\le {vol}^{*}\left(\mathrm{ran}{F}\right)$
160 20 159 syl ${⊢}{\phi }\to 0\le {vol}^{*}\left(\mathrm{ran}{F}\right)$
161 0xr ${⊢}0\in {ℝ}^{*}$
162 ovolcl ${⊢}\mathrm{ran}{F}\subseteq ℝ\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{*}$
163 20 162 syl ${⊢}{\phi }\to {vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{*}$
164 xrleloe ${⊢}\left(0\in {ℝ}^{*}\wedge {vol}^{*}\left(\mathrm{ran}{F}\right)\in {ℝ}^{*}\right)\to \left(0\le {vol}^{*}\left(\mathrm{ran}{F}\right)↔\left(0<{vol}^{*}\left(\mathrm{ran}{F}\right)\vee 0={vol}^{*}\left(\mathrm{ran}{F}\right)\right)\right)$
165 161 163 164 sylancr ${⊢}{\phi }\to \left(0\le {vol}^{*}\left(\mathrm{ran}{F}\right)↔\left(0<{vol}^{*}\left(\mathrm{ran}{F}\right)\vee 0={vol}^{*}\left(\mathrm{ran}{F}\right)\right)\right)$
166 160 165 mpbid ${⊢}{\phi }\to \left(0<{vol}^{*}\left(\mathrm{ran}{F}\right)\vee 0={vol}^{*}\left(\mathrm{ran}{F}\right)\right)$
167 166 ord ${⊢}{\phi }\to \left(¬0<{vol}^{*}\left(\mathrm{ran}{F}\right)\to 0={vol}^{*}\left(\mathrm{ran}{F}\right)\right)$
168 158 167 mpd ${⊢}{\phi }\to 0={vol}^{*}\left(\mathrm{ran}{F}\right)$
169 168 adantr ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to 0={vol}^{*}\left(\mathrm{ran}{F}\right)$
170 33 169 eqtr4d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {vol}^{*}\left({T}\left({m}\right)\right)=0$