# Metamath Proof Explorer

## Theorem ovollb2

Description: It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb ). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypothesis ovollb2.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
Assertion ovollb2 ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 ovollb2.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
2 simpr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
3 ovolficcss ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
4 3 adantr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\subseteq ℝ$
5 2 4 sstrd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {A}\subseteq ℝ$
6 ovolcl ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
7 5 6 syl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
8 7 adantr ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
9 pnfge ${⊢}{vol}^{*}\left({A}\right)\in {ℝ}^{*}\to {vol}^{*}\left({A}\right)\le \mathrm{+\infty }$
10 8 9 syl ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({A}\right)\le \mathrm{+\infty }$
11 simpr ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=\mathrm{+\infty }$
12 10 11 breqtrrd ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
13 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {F}=\left(\mathrm{abs}\circ -\right)\circ {F}$
14 13 1 ovolsf ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
15 14 adantr ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
16 15 frnd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
17 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
18 16 17 sstrdi ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \mathrm{ran}{S}\subseteq ℝ$
19 1nn ${⊢}1\in ℕ$
20 15 fdmd ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \mathrm{dom}{S}=ℕ$
21 19 20 eleqtrrid ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to 1\in \mathrm{dom}{S}$
22 21 ne0d ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \mathrm{dom}{S}\ne \varnothing$
23 dm0rn0 ${⊢}\mathrm{dom}{S}=\varnothing ↔\mathrm{ran}{S}=\varnothing$
24 23 necon3bii ${⊢}\mathrm{dom}{S}\ne \varnothing ↔\mathrm{ran}{S}\ne \varnothing$
25 22 24 sylib ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \mathrm{ran}{S}\ne \varnothing$
26 supxrre2 ${⊢}\left(\mathrm{ran}{S}\subseteq ℝ\wedge \mathrm{ran}{S}\ne \varnothing \right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ↔sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
27 18 25 26 syl2anc ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ↔sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
28 27 biimpar ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ$
29 2fveq3 ${⊢}{m}={n}\to {1}^{st}\left({F}\left({m}\right)\right)={1}^{st}\left({F}\left({n}\right)\right)$
30 oveq2 ${⊢}{m}={n}\to {2}^{{m}}={2}^{{n}}$
31 30 oveq2d ${⊢}{m}={n}\to \frac{\frac{{x}}{2}}{{2}^{{m}}}=\frac{\frac{{x}}{2}}{{2}^{{n}}}$
32 29 31 oveq12d ${⊢}{m}={n}\to {1}^{st}\left({F}\left({m}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)={1}^{st}\left({F}\left({n}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right)$
33 2fveq3 ${⊢}{m}={n}\to {2}^{nd}\left({F}\left({m}\right)\right)={2}^{nd}\left({F}\left({n}\right)\right)$
34 33 31 oveq12d ${⊢}{m}={n}\to {2}^{nd}\left({F}\left({m}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)={2}^{nd}\left({F}\left({n}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right)$
35 32 34 opeq12d ${⊢}{m}={n}\to ⟨{1}^{st}\left({F}\left({m}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right),{2}^{nd}\left({F}\left({m}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)⟩=⟨{1}^{st}\left({F}\left({n}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right),{2}^{nd}\left({F}\left({n}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right)⟩$
36 35 cbvmptv ${⊢}\left({m}\in ℕ⟼⟨{1}^{st}\left({F}\left({m}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right),{2}^{nd}\left({F}\left({m}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)⟩\right)=\left({n}\in ℕ⟼⟨{1}^{st}\left({F}\left({n}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right),{2}^{nd}\left({F}\left({n}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{n}}}\right)⟩\right)$
37 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({m}\in ℕ⟼⟨{1}^{st}\left({F}\left({m}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right),{2}^{nd}\left({F}\left({m}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)⟩\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({m}\in ℕ⟼⟨{1}^{st}\left({F}\left({m}\right)\right)-\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right),{2}^{nd}\left({F}\left({m}\right)\right)+\left(\frac{\frac{{x}}{2}}{{2}^{{m}}}\right)⟩\right)\right)\right)$
38 simplll ${⊢}\left(\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
39 simpllr ${⊢}\left(\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)$
40 simpr ${⊢}\left(\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
41 simplr ${⊢}\left(\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ$
42 1 36 37 38 39 40 41 ovollb2lem ${⊢}\left(\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)+{x}$
43 42 ralrimiva ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)+{x}$
44 xralrple ${⊢}\left({vol}^{*}\left({A}\right)\in {ℝ}^{*}\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\to \left({vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)+{x}\right)$
45 7 44 sylan ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\to \left({vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)+{x}\right)$
46 43 45 mpbird ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
47 28 46 syldan ${⊢}\left(\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
48 12 47 pm2.61dane ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {F}\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$