# Metamath Proof Explorer

## Theorem ovolgelb

Description: The outer volume is the greatest lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovolgelb.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right)$
Assertion ovolgelb ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)$

### Proof

Step Hyp Ref Expression
1 ovolgelb.1 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right)$
2 simp2 ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)\in ℝ$
3 simp3 ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in {ℝ}^{+}$
4 2 3 ltaddrpd ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)<{vol}^{*}\left({A}\right)+{B}$
5 3 rpred ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℝ$
6 2 5 readdcld ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)+{B}\in ℝ$
7 2 6 ltnled ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({vol}^{*}\left({A}\right)<{vol}^{*}\left({A}\right)+{B}↔¬{vol}^{*}\left({A}\right)+{B}\le {vol}^{*}\left({A}\right)\right)$
8 4 7 mpbid ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ¬{vol}^{*}\left({A}\right)+{B}\le {vol}^{*}\left({A}\right)$
9 eqid ${⊢}\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}=\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}$
10 9 ovolval ${⊢}{A}\subseteq ℝ\to {vol}^{*}\left({A}\right)=sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)$
11 10 3ad2ant1 ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)=sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)$
12 11 breq2d ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({vol}^{*}\left({A}\right)+{B}\le {vol}^{*}\left({A}\right)↔{vol}^{*}\left({A}\right)+{B}\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\right)$
13 ssrab2 ${⊢}\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}$
14 6 rexrd ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\right)+{B}\in {ℝ}^{*}$
15 infxrgelb ${⊢}\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{B}\in {ℝ}^{*}\right)\to \left({vol}^{*}\left({A}\right)+{B}\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)↔\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)+{B}\le {x}\right)$
16 13 14 15 sylancr ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({vol}^{*}\left({A}\right)+{B}\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)↔\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)+{B}\le {x}\right)$
17 eqeq1 ${⊢}{y}={x}\to \left({y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)↔{x}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)$
18 1 rneqi ${⊢}\mathrm{ran}{S}=\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right)$
19 18 supeq1i ${⊢}sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)$
20 19 eqeq2i ${⊢}{x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)↔{x}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)$
21 17 20 syl6bbr ${⊢}{y}={x}\to \left({y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)↔{x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
22 21 anbi2d ${⊢}{y}={x}\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
23 22 rexbidv ${⊢}{y}={x}\to \left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)↔\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
24 23 ralrab ${⊢}\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)+{B}\le {x}↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)$
25 ralcom ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)$
26 r19.23v ${⊢}\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)$
27 26 ralbii ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)$
28 ancomst ${⊢}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left(\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)$
29 impexp ${⊢}\left(\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)\right)$
30 28 29 bitri ${⊢}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)\right)$
31 30 ralbii ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)\right)$
32 elovolmlem ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{g}:ℕ⟶\le \cap {ℝ}^{2}$
33 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {g}=\left(\mathrm{abs}\circ -\right)\circ {g}$
34 33 1 ovolsf ${⊢}{g}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
35 32 34 sylbi ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
36 35 frnd ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
37 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
38 36 37 sstrdi ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
39 supxrcl ${⊢}\mathrm{ran}{S}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
40 38 39 syl ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
41 breq2 ${⊢}{x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({vol}^{*}\left({A}\right)+{B}\le {x}↔{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
42 41 imbi2d ${⊢}{x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
43 42 ceqsralv ${⊢}sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
44 40 43 syl ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
45 31 44 syl5bb ${⊢}{g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\to \left(\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
46 45 ralbiia ${⊢}\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
47 25 27 46 3bitr3i ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {x}=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left({A}\right)+{B}\le {x}\right)↔\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
48 24 47 bitri ${⊢}\forall {x}\in \left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\right)+{B}\le {x}↔\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
49 16 48 syl6rbb ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)↔{vol}^{*}\left({A}\right)+{B}\le sup\left(\left\{{y}\in {ℝ}^{*}|\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge {y}=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {g}\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\right)$
50 12 49 bitr4d ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({vol}^{*}\left({A}\right)+{B}\le {vol}^{*}\left({A}\right)↔\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\right)$
51 8 50 mtbid ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to ¬\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
52 rexanali ${⊢}\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge ¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)↔¬\forall {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\to {vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
53 51 52 sylibr ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge ¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
54 xrltnle ${⊢}\left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{B}\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)<{vol}^{*}\left({A}\right)+{B}↔¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)$
55 xrltle ${⊢}\left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{B}\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)<{vol}^{*}\left({A}\right)+{B}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)$
56 54 55 sylbird ${⊢}\left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{B}\in {ℝ}^{*}\right)\to \left(¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)$
57 40 14 56 syl2anr ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\right)\to \left(¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)$
58 57 anim2d ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\right)\to \left(\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge ¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)\right)$
59 58 reximdva ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge ¬{vol}^{*}\left({A}\right)+{B}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)\right)$
60 53 59 mpd ${⊢}\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \exists {g}\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)\phantom{\rule{.4em}{0ex}}\left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {g}\right)\wedge sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{B}\right)$