Metamath Proof Explorer

Theorem ovolscalem1

Description: Lemma for ovolsca . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses ovolsca.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
ovolsca.2 ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
ovolsca.3 ${⊢}{\phi }\to {B}=\left\{{x}\in ℝ|{C}{x}\in {A}\right\}$
ovolsca.4 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)\in ℝ$
ovolsca.5 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
ovolsca.6 ${⊢}{G}=\left({n}\in ℕ⟼⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)$
ovolsca.7 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
ovolsca.8 ${⊢}{\phi }\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
ovolsca.9 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
ovolsca.10 ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{C}{R}$
Assertion ovolscalem1 ${⊢}{\phi }\to {vol}^{*}\left({B}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$

Proof

Step Hyp Ref Expression
1 ovolsca.1 ${⊢}{\phi }\to {A}\subseteq ℝ$
2 ovolsca.2 ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
3 ovolsca.3 ${⊢}{\phi }\to {B}=\left\{{x}\in ℝ|{C}{x}\in {A}\right\}$
4 ovolsca.4 ${⊢}{\phi }\to {vol}^{*}\left({A}\right)\in ℝ$
5 ovolsca.5 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
6 ovolsca.6 ${⊢}{G}=\left({n}\in ℕ⟼⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)$
7 ovolsca.7 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
8 ovolsca.8 ${⊢}{\phi }\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
9 ovolsca.9 ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
10 ovolsca.10 ${⊢}{\phi }\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{C}{R}$
11 ssrab2 ${⊢}\left\{{x}\in ℝ|{C}{x}\in {A}\right\}\subseteq ℝ$
12 3 11 eqsstrdi ${⊢}{\phi }\to {B}\subseteq ℝ$
13 ovolcl ${⊢}{B}\subseteq ℝ\to {vol}^{*}\left({B}\right)\in {ℝ}^{*}$
14 12 13 syl ${⊢}{\phi }\to {vol}^{*}\left({B}\right)\in {ℝ}^{*}$
15 ovolfcl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)\right)$
16 7 15 sylan ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge {1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)\right)$
17 16 simp3d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)$
18 16 simp1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {1}^{st}\left({F}\left({n}\right)\right)\in ℝ$
19 16 simp2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ$
20 2 rpregt0d ${⊢}{\phi }\to \left({C}\in ℝ\wedge 0<{C}\right)$
21 20 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({C}\in ℝ\wedge 0<{C}\right)$
22 lediv1 ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)↔\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\le \frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)$
23 18 19 21 22 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)\le {2}^{nd}\left({F}\left({n}\right)\right)↔\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\le \frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)$
24 17 23 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\le \frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}$
25 df-br ${⊢}\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\le \frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}↔⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in \le$
26 24 25 sylib ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in \le$
27 2 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {C}\in {ℝ}^{+}$
28 18 27 rerpdivcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\in ℝ$
29 19 27 rerpdivcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\in ℝ$
30 28 29 opelxpd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in {ℝ}^{2}$
31 26 30 elind ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to ⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in \left(\le \cap {ℝ}^{2}\right)$
32 31 6 fmptd ${⊢}{\phi }\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
33 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {G}=\left(\mathrm{abs}\circ -\right)\circ {G}$
34 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)$
35 33 34 ovolsf ${⊢}{G}:ℕ⟶\le \cap {ℝ}^{2}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
36 32 35 syl ${⊢}{\phi }\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
37 36 frnd ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\subseteq \left[0,\mathrm{+\infty }\right)$
38 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
39 37 38 sstrdi ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\subseteq {ℝ}^{*}$
40 supxrcl ${⊢}\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
41 39 40 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
42 4 2 rerpdivcld ${⊢}{\phi }\to \frac{{vol}^{*}\left({A}\right)}{{C}}\in ℝ$
43 9 rpred ${⊢}{\phi }\to {R}\in ℝ$
44 42 43 readdcld ${⊢}{\phi }\to \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\in ℝ$
45 44 rexrd ${⊢}{\phi }\to \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\in {ℝ}^{*}$
46 3 eleq2d ${⊢}{\phi }\to \left({y}\in {B}↔{y}\in \left\{{x}\in ℝ|{C}{x}\in {A}\right\}\right)$
47 oveq2 ${⊢}{x}={y}\to {C}{x}={C}{y}$
48 47 eleq1d ${⊢}{x}={y}\to \left({C}{x}\in {A}↔{C}{y}\in {A}\right)$
49 48 elrab ${⊢}{y}\in \left\{{x}\in ℝ|{C}{x}\in {A}\right\}↔\left({y}\in ℝ\wedge {C}{y}\in {A}\right)$
50 46 49 syl6bb ${⊢}{\phi }\to \left({y}\in {B}↔\left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)$
51 breq2 ${⊢}{x}={C}{y}\to \left({1}^{st}\left({F}\left({n}\right)\right)<{x}↔{1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\right)$
52 breq1 ${⊢}{x}={C}{y}\to \left({x}<{2}^{nd}\left({F}\left({n}\right)\right)↔{C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)$
53 51 52 anbi12d ${⊢}{x}={C}{y}\to \left(\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\wedge {C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
54 53 rexbidv ${⊢}{x}={C}{y}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\wedge {C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
55 ovolfioo ${⊢}\left({A}\subseteq ℝ\wedge {F}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
56 1 7 55 syl2anc ${⊢}{\phi }\to \left({A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)\right)$
57 8 56 mpbid ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)$
58 57 adantr ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{x}\wedge {x}<{2}^{nd}\left({F}\left({n}\right)\right)\right)$
59 simprr ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\to {C}{y}\in {A}$
60 54 58 59 rspcdva ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\wedge {C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)$
61 opex ${⊢}⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in \mathrm{V}$
62 6 fvmpt2 ${⊢}\left({n}\in ℕ\wedge ⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\in \mathrm{V}\right)\to {G}\left({n}\right)=⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩$
63 61 62 mpan2 ${⊢}{n}\in ℕ\to {G}\left({n}\right)=⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩$
64 63 fveq2d ${⊢}{n}\in ℕ\to {1}^{st}\left({G}\left({n}\right)\right)={1}^{st}\left(⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)$
65 ovex ${⊢}\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\in \mathrm{V}$
66 ovex ${⊢}\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\in \mathrm{V}$
67 65 66 op1st ${⊢}{1}^{st}\left(⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)=\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}$
68 64 67 syl6eq ${⊢}{n}\in ℕ\to {1}^{st}\left({G}\left({n}\right)\right)=\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}$
69 68 adantl ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to {1}^{st}\left({G}\left({n}\right)\right)=\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}$
70 69 breq1d ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({G}\left({n}\right)\right)<{y}↔\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}<{y}\right)$
71 18 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to {1}^{st}\left({F}\left({n}\right)\right)\in ℝ$
72 simplrl ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to {y}\in ℝ$
73 21 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({C}\in ℝ\wedge 0<{C}\right)$
74 ltdivmul ${⊢}\left({1}^{st}\left({F}\left({n}\right)\right)\in ℝ\wedge {y}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}<{y}↔{1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\right)$
75 71 72 73 74 syl3anc ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}<{y}↔{1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\right)$
76 70 75 bitr2d ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}↔{1}^{st}\left({G}\left({n}\right)\right)<{y}\right)$
77 19 adantlr ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ$
78 ltmuldiv2 ${⊢}\left({y}\in ℝ\wedge {2}^{nd}\left({F}\left({n}\right)\right)\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)↔{y}<\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)$
79 72 77 73 78 syl3anc ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)↔{y}<\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)$
80 63 fveq2d ${⊢}{n}\in ℕ\to {2}^{nd}\left({G}\left({n}\right)\right)={2}^{nd}\left(⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)$
81 65 66 op2nd ${⊢}{2}^{nd}\left(⟨\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}},\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}⟩\right)=\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}$
82 80 81 syl6eq ${⊢}{n}\in ℕ\to {2}^{nd}\left({G}\left({n}\right)\right)=\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}$
83 82 adantl ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to {2}^{nd}\left({G}\left({n}\right)\right)=\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}$
84 83 breq2d ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({y}<{2}^{nd}\left({G}\left({n}\right)\right)↔{y}<\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)$
85 79 84 bitr4d ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left({C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)↔{y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)$
86 76 85 anbi12d ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\wedge {n}\in ℕ\right)\to \left(\left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\wedge {C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
87 86 rexbidva ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({F}\left({n}\right)\right)<{C}{y}\wedge {C}{y}<{2}^{nd}\left({F}\left({n}\right)\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
88 60 87 mpbid ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge {C}{y}\in {A}\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)$
89 88 ex ${⊢}{\phi }\to \left(\left({y}\in ℝ\wedge {C}{y}\in {A}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
90 50 89 sylbid ${⊢}{\phi }\to \left({y}\in {B}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
91 90 ralrimiv ${⊢}{\phi }\to \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)$
92 ovolfioo ${⊢}\left({B}\subseteq ℝ\wedge {G}:ℕ⟶\le \cap {ℝ}^{2}\right)\to \left({B}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
93 12 32 92 syl2anc ${⊢}{\phi }\to \left({B}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left({1}^{st}\left({G}\left({n}\right)\right)<{y}\wedge {y}<{2}^{nd}\left({G}\left({n}\right)\right)\right)\right)$
94 91 93 mpbird ${⊢}{\phi }\to {B}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
95 34 ovollb ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {B}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\to {vol}^{*}\left({B}\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)$
96 32 94 95 syl2anc ${⊢}{\phi }\to {vol}^{*}\left({B}\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)$
97 fzfid ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(1\dots {k}\right)\in \mathrm{Fin}$
98 2 rpcnd ${⊢}{\phi }\to {C}\in ℂ$
99 98 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {C}\in ℂ$
100 simpl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {\phi }$
101 elfznn ${⊢}{n}\in \left(1\dots {k}\right)\to {n}\in ℕ$
102 19 18 resubcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\in ℝ$
103 100 101 102 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}\right)\right)\to {2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\in ℝ$
104 103 recnd ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}\right)\right)\to {2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\in ℂ$
105 2 rpne0d ${⊢}{\phi }\to {C}\ne 0$
106 105 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {C}\ne 0$
107 97 99 104 106 fsumdivc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \frac{\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)}{{C}}=\sum _{{n}=1}^{{k}}\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)$
108 82 68 oveq12d ${⊢}{n}\in ℕ\to {2}^{nd}\left({G}\left({n}\right)\right)-{1}^{st}\left({G}\left({n}\right)\right)=\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)-\left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)$
109 108 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {2}^{nd}\left({G}\left({n}\right)\right)-{1}^{st}\left({G}\left({n}\right)\right)=\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)-\left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)$
110 33 ovolfsval ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({n}\right)={2}^{nd}\left({G}\left({n}\right)\right)-{1}^{st}\left({G}\left({n}\right)\right)$
111 32 110 sylan ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({n}\right)={2}^{nd}\left({G}\left({n}\right)\right)-{1}^{st}\left({G}\left({n}\right)\right)$
112 19 recnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\right)\in ℂ$
113 18 recnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {1}^{st}\left({F}\left({n}\right)\right)\in ℂ$
114 2 rpcnne0d ${⊢}{\phi }\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
115 114 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
116 divsubdir ${⊢}\left({2}^{nd}\left({F}\left({n}\right)\right)\in ℂ\wedge {1}^{st}\left({F}\left({n}\right)\right)\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}=\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)-\left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)$
117 112 113 115 116 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}=\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)}{{C}}\right)-\left(\frac{{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)$
118 109 111 117 3eqtr4d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({n}\right)=\frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}$
119 100 101 118 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({n}\right)=\frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}$
120 simpr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in ℕ$
121 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
122 120 121 eleqtrdi ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in {ℤ}_{\ge 1}$
123 102 27 rerpdivcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\in ℝ$
124 123 recnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\in ℂ$
125 100 101 124 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}\right)\right)\to \frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\in ℂ$
126 119 122 125 fsumser ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \sum _{{n}=1}^{{k}}\left(\frac{{2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)}{{C}}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)$
127 107 126 eqtrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \frac{\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)}{{C}}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)$
128 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {F}=\left(\mathrm{abs}\circ -\right)\circ {F}$
129 128 5 ovolsf ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
130 7 129 syl ${⊢}{\phi }\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
131 130 frnd ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
132 131 38 sstrdi ${⊢}{\phi }\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
133 2 9 rpmulcld ${⊢}{\phi }\to {C}{R}\in {ℝ}^{+}$
134 133 rpred ${⊢}{\phi }\to {C}{R}\in ℝ$
135 4 134 readdcld ${⊢}{\phi }\to {vol}^{*}\left({A}\right)+{C}{R}\in ℝ$
136 135 rexrd ${⊢}{\phi }\to {vol}^{*}\left({A}\right)+{C}{R}\in {ℝ}^{*}$
137 supxrleub ${⊢}\left(\mathrm{ran}{S}\subseteq {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{C}{R}\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{C}{R}↔\forall {x}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{x}\le {vol}^{*}\left({A}\right)+{C}{R}\right)$
138 132 136 137 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+{C}{R}↔\forall {x}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{x}\le {vol}^{*}\left({A}\right)+{C}{R}\right)$
139 10 138 mpbid ${⊢}{\phi }\to \forall {x}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{x}\le {vol}^{*}\left({A}\right)+{C}{R}$
140 130 ffnd ${⊢}{\phi }\to {S}Fnℕ$
141 breq1 ${⊢}{x}={S}\left({k}\right)\to \left({x}\le {vol}^{*}\left({A}\right)+{C}{R}↔{S}\left({k}\right)\le {vol}^{*}\left({A}\right)+{C}{R}\right)$
142 141 ralrn ${⊢}{S}Fnℕ\to \left(\forall {x}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{x}\le {vol}^{*}\left({A}\right)+{C}{R}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left({A}\right)+{C}{R}\right)$
143 140 142 syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{x}\le {vol}^{*}\left({A}\right)+{C}{R}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left({A}\right)+{C}{R}\right)$
144 139 143 mpbid ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {vol}^{*}\left({A}\right)+{C}{R}$
145 144 r19.21bi ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {S}\left({k}\right)\le {vol}^{*}\left({A}\right)+{C}{R}$
146 7 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
147 128 ovolfsval ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {n}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\left({n}\right)={2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)$
148 146 101 147 syl2an ${⊢}\left(\left({\phi }\wedge {k}\in ℕ\right)\wedge {n}\in \left(1\dots {k}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\left({n}\right)={2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)$
149 148 122 104 fsumser ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)\left({k}\right)$
150 5 fveq1i ${⊢}{S}\left({k}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)\left({k}\right)$
151 149 150 syl6eqr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)={S}\left({k}\right)$
152 42 recnd ${⊢}{\phi }\to \frac{{vol}^{*}\left({A}\right)}{{C}}\in ℂ$
153 9 rpcnd ${⊢}{\phi }\to {R}\in ℂ$
154 98 152 153 adddid ${⊢}{\phi }\to {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)={C}\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{C}{R}$
155 4 recnd ${⊢}{\phi }\to {vol}^{*}\left({A}\right)\in ℂ$
156 155 98 105 divcan2d ${⊢}{\phi }\to {C}\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)={vol}^{*}\left({A}\right)$
157 156 oveq1d ${⊢}{\phi }\to {C}\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{C}{R}={vol}^{*}\left({A}\right)+{C}{R}$
158 154 157 eqtrd ${⊢}{\phi }\to {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)={vol}^{*}\left({A}\right)+{C}{R}$
159 158 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)={vol}^{*}\left({A}\right)+{C}{R}$
160 145 151 159 3brtr4d ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)\le {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
161 97 103 fsumrecl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)\in ℝ$
162 44 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\in ℝ$
163 20 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left({C}\in ℝ\wedge 0<{C}\right)$
164 ledivmul ${⊢}\left(\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)\in ℝ\wedge \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)}{{C}}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)\le {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)\right)$
165 161 162 163 164 syl3anc ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \left(\frac{\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)}{{C}}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)\le {C}\left(\left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)\right)$
166 160 165 mpbird ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to \frac{\sum _{{n}=1}^{{k}}\left({2}^{nd}\left({F}\left({n}\right)\right)-{1}^{st}\left({F}\left({n}\right)\right)\right)}{{C}}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$
167 127 166 eqbrtrrd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$
168 167 ralrimiva ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$
169 36 ffnd ${⊢}{\phi }\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)Fnℕ$
170 breq1 ${⊢}{y}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\to \left({y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
171 170 ralrn ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)Fnℕ\to \left(\forall {y}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\phantom{\rule{.4em}{0ex}}{y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
172 169 171 syl ${⊢}{\phi }\to \left(\forall {y}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\phantom{\rule{.4em}{0ex}}{y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({k}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
173 168 172 mpbird ${⊢}{\phi }\to \forall {y}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\phantom{\rule{.4em}{0ex}}{y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$
174 supxrleub ${⊢}\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\subseteq {ℝ}^{*}\wedge \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\forall {y}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\phantom{\rule{.4em}{0ex}}{y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
175 39 45 174 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}↔\forall {y}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\phantom{\rule{.4em}{0ex}}{y}\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}\right)$
176 173 175 mpbird ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right),{ℝ}^{*},<\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$
177 14 41 45 96 176 xrletrd ${⊢}{\phi }\to {vol}^{*}\left({B}\right)\le \left(\frac{{vol}^{*}\left({A}\right)}{{C}}\right)+{R}$