# Metamath Proof Explorer

## Theorem ovoliunlem3

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t ${⊢}{T}=seq1\left(+,{G}\right)$
ovoliun.g ${⊢}{G}=\left({n}\in ℕ⟼{vol}^{*}\left({A}\right)\right)$
ovoliun.a ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq ℝ$
ovoliun.v ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)\in ℝ$
ovoliun.r ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
ovoliun.b ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
Assertion ovoliunlem3 ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$

### Proof

Step Hyp Ref Expression
1 ovoliun.t ${⊢}{T}=seq1\left(+,{G}\right)$
2 ovoliun.g ${⊢}{G}=\left({n}\in ℕ⟼{vol}^{*}\left({A}\right)\right)$
3 ovoliun.a ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq ℝ$
4 ovoliun.v ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)\in ℝ$
5 ovoliun.r ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
6 ovoliun.b ${⊢}{\phi }\to {B}\in {ℝ}^{+}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{A}$
8 nfcsb1v
9 csbeq1a
10 7 8 9 cbviun
11 10 fveq2i
12 2nn ${⊢}2\in ℕ$
13 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
14 nnexpcl ${⊢}\left(2\in ℕ\wedge {n}\in {ℕ}_{0}\right)\to {2}^{{n}}\in ℕ$
15 12 13 14 sylancr ${⊢}{n}\in ℕ\to {2}^{{n}}\in ℕ$
16 15 nnrpd ${⊢}{n}\in ℕ\to {2}^{{n}}\in {ℝ}^{+}$
17 rpdivcl ${⊢}\left({B}\in {ℝ}^{+}\wedge {2}^{{n}}\in {ℝ}^{+}\right)\to \frac{{B}}{{2}^{{n}}}\in {ℝ}^{+}$
18 6 16 17 syl2an ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{B}}{{2}^{{n}}}\in {ℝ}^{+}$
19 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)$
20 19 ovolgelb ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge \frac{{B}}{{2}^{{n}}}\in {ℝ}^{+}\right)\to \exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
21 3 4 18 20 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
22 21 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
23 ovex ${⊢}{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\in \mathrm{V}$
24 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
25 coeq2 ${⊢}{f}={g}\left({n}\right)\to \left(.\right)\circ {f}=\left(.\right)\circ {g}\left({n}\right)$
26 25 rneqd ${⊢}{f}={g}\left({n}\right)\to \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)$
27 26 unieqd ${⊢}{f}={g}\left({n}\right)\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)$
28 27 sseq2d ${⊢}{f}={g}\left({n}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)↔{A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\right)$
29 coeq2 ${⊢}{f}={g}\left({n}\right)\to \left(\mathrm{abs}\circ -\right)\circ {f}=\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)$
30 29 seqeq3d ${⊢}{f}={g}\left({n}\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right)$
31 30 rneqd ${⊢}{f}={g}\left({n}\right)\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right)=\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right)$
32 31 supeq1d ${⊢}{f}={g}\left({n}\right)\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)$
33 32 breq1d ${⊢}{f}={g}\left({n}\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)↔sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
34 28 33 anbi12d ${⊢}{f}={g}\left({n}\right)\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)$
35 23 24 34 axcc4 ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {f}\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {f}\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)$
36 22 35 syl ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)$
37 xpnnen ${⊢}\left(ℕ×ℕ\right)\approx ℕ$
38 37 ensymi ${⊢}ℕ\approx \left(ℕ×ℕ\right)$
39 bren ${⊢}ℕ\approx \left(ℕ×ℕ\right)↔\exists {j}\phantom{\rule{.4em}{0ex}}{j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
40 38 39 mpbi ${⊢}\exists {j}\phantom{\rule{.4em}{0ex}}{j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
41 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)$
42 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{vol}^{*}$
43 42 8 nffv
44 9 fveq2d
45 41 43 44 cbvmpt
46 2 45 eqtri
47 3 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
48 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{A}\subseteq ℝ$
49 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}ℝ$
50 8 49 nfss
51 9 sseq1d
52 48 50 51 cbvralw
53 47 52 sylib
54 53 r19.21bi
56 4 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\in ℝ$
57 41 nfel1 ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\in ℝ$
58 43 nfel1
59 44 eleq1d
60 57 58 59 cbvralw
61 56 60 sylib
62 61 r19.21bi
64 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\right)\wedge \left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
65 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\right)\wedge \left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)\right)\to {B}\in {ℝ}^{+}$
66 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right)$
67 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({k}\in ℕ⟼{g}\left({1}^{st}\left({j}\left({k}\right)\right)\right)\left({2}^{nd}\left({j}\left({k}\right)\right)\right)\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({k}\in ℕ⟼{g}\left({1}^{st}\left({j}\left({k}\right)\right)\right)\left({2}^{nd}\left({j}\left({k}\right)\right)\right)\right)\right)\right)$
68 eqid ${⊢}\left({k}\in ℕ⟼{g}\left({1}^{st}\left({j}\left({k}\right)\right)\right)\left({2}^{nd}\left({j}\left({k}\right)\right)\right)\right)=\left({k}\in ℕ⟼{g}\left({1}^{st}\left({j}\left({k}\right)\right)\right)\left({2}^{nd}\left({j}\left({k}\right)\right)\right)\right)$
69 simplr ${⊢}\left(\left({\phi }\wedge {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\right)\wedge \left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)\right)\to {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
70 simprl ${⊢}\left(\left({\phi }\wedge {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\right)\wedge \left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)\right)\to {g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
71 simprr ${⊢}\left(\left({\phi }\wedge {j}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\right)\wedge \left({g}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
72 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)\wedge sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
73 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({m}\right)\right)$
74 8 73 nfss
75 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right),{ℝ}^{*},<\right)$
76 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\le$
77 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}+$
78 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(\frac{{B}}{{2}^{{m}}}\right)$
79 43 77 78 nfov
80 75 76 79 nfbr
81 74 80 nfan
82 fveq2 ${⊢}{n}={m}\to {g}\left({n}\right)={g}\left({m}\right)$
83 82 coeq2d ${⊢}{n}={m}\to \left(.\right)\circ {g}\left({n}\right)=\left(.\right)\circ {g}\left({m}\right)$
84 83 rneqd ${⊢}{n}={m}\to \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)=\mathrm{ran}\left(\left(.\right)\circ {g}\left({m}\right)\right)$
85 84 unieqd ${⊢}{n}={m}\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({n}\right)\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\left({m}\right)\right)$
86 9 85 sseq12d
87 82 coeq2d ${⊢}{n}={m}\to \left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)=\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)$
88 87 seqeq3d ${⊢}{n}={m}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right)$
89 88 rneqd ${⊢}{n}={m}\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right)=\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right)$
90 89 supeq1d ${⊢}{n}={m}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({n}\right)\right)\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\left({m}\right)\right)\right),{ℝ}^{*},<\right)$
91 oveq2 ${⊢}{n}={m}\to {2}^{{n}}={2}^{{m}}$
92 91 oveq2d ${⊢}{n}={m}\to \frac{{B}}{{2}^{{n}}}=\frac{{B}}{{2}^{{m}}}$
93 44 92 oveq12d
94 90 93 breq12d
95 86 94 anbi12d
96 72 81 95 cbvralw
97 71 96 sylib
98 97 r19.21bi
99 98 simpld
100 98 simprd
101 1 46 55 63 64 65 66 67 68 69 70 99 100 ovoliunlem2
102 101 exp31
103 102 exlimdv
104 40 103 mpi
105 104 exlimdv
106 36 105 mpd
107 11 106 eqbrtrid ${⊢}{\phi }\to {vol}^{*}\left(\bigcup _{{n}\in ℕ}{A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$