# Metamath Proof Explorer

## Theorem ovoliunlem1

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

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 {ℝ}^{+}$
ovoliun.s ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)$
ovoliun.u ${⊢}{U}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)$
ovoliun.h ${⊢}{H}=\left({k}\in ℕ⟼{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\right)$
ovoliun.j ${⊢}{\phi }\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
ovoliun.f ${⊢}{\phi }\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
ovoliun.x1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
ovoliun.x2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
ovoliun.k ${⊢}{\phi }\to {K}\in ℕ$
ovoliun.l1 ${⊢}{\phi }\to {L}\in ℤ$
ovoliun.l2 ${⊢}{\phi }\to \forall {w}\in \left(1\dots {K}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {L}$
Assertion ovoliunlem1 ${⊢}{\phi }\to {U}\left({K}\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 ovoliun.s ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)$
8 ovoliun.u ${⊢}{U}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)$
9 ovoliun.h ${⊢}{H}=\left({k}\in ℕ⟼{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\right)$
10 ovoliun.j ${⊢}{\phi }\to {J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ$
11 ovoliun.f ${⊢}{\phi }\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
12 ovoliun.x1 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
13 ovoliun.x2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
14 ovoliun.k ${⊢}{\phi }\to {K}\in ℕ$
15 ovoliun.l1 ${⊢}{\phi }\to {L}\in ℤ$
16 ovoliun.l2 ${⊢}{\phi }\to \forall {w}\in \left(1\dots {K}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {L}$
17 2fveq3 ${⊢}{j}={J}\left({m}\right)\to {F}\left({1}^{st}\left({j}\right)\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)$
18 fveq2 ${⊢}{j}={J}\left({m}\right)\to {2}^{nd}\left({j}\right)={2}^{nd}\left({J}\left({m}\right)\right)$
19 17 18 fveq12d ${⊢}{j}={J}\left({m}\right)\to {F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)$
20 19 fveq2d ${⊢}{j}={J}\left({m}\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
21 19 fveq2d ${⊢}{j}={J}\left({m}\right)\to {1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
22 20 21 oveq12d ${⊢}{j}={J}\left({m}\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
23 fzfid ${⊢}{\phi }\to \left(1\dots {K}\right)\in \mathrm{Fin}$
24 f1of1 ${⊢}{J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\to {J}:ℕ\underset{1-1}{⟶}ℕ×ℕ$
25 10 24 syl ${⊢}{\phi }\to {J}:ℕ\underset{1-1}{⟶}ℕ×ℕ$
26 fz1ssnn ${⊢}\left(1\dots {K}\right)\subseteq ℕ$
27 f1ores ${⊢}\left({J}:ℕ\underset{1-1}{⟶}ℕ×ℕ\wedge \left(1\dots {K}\right)\subseteq ℕ\right)\to \left({{J}↾}_{\left(1\dots {K}\right)}\right):\left(1\dots {K}\right)\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]$
28 25 26 27 sylancl ${⊢}{\phi }\to \left({{J}↾}_{\left(1\dots {K}\right)}\right):\left(1\dots {K}\right)\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]$
29 fvres ${⊢}{m}\in \left(1\dots {K}\right)\to \left({{J}↾}_{\left(1\dots {K}\right)}\right)\left({m}\right)={J}\left({m}\right)$
30 29 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to \left({{J}↾}_{\left(1\dots {K}\right)}\right)\left({m}\right)={J}\left({m}\right)$
31 11 adantr ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
32 imassrn ${⊢}{J}\left[\left(1\dots {K}\right)\right]\subseteq \mathrm{ran}{J}$
33 f1of ${⊢}{J}:ℕ\underset{1-1 onto}{⟶}ℕ×ℕ\to {J}:ℕ⟶ℕ×ℕ$
34 10 33 syl ${⊢}{\phi }\to {J}:ℕ⟶ℕ×ℕ$
35 34 frnd ${⊢}{\phi }\to \mathrm{ran}{J}\subseteq ℕ×ℕ$
36 32 35 sstrid ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\subseteq ℕ×ℕ$
37 36 sselda ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {j}\in \left(ℕ×ℕ\right)$
38 xp1st ${⊢}{j}\in \left(ℕ×ℕ\right)\to {1}^{st}\left({j}\right)\in ℕ$
39 37 38 syl ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {1}^{st}\left({j}\right)\in ℕ$
40 31 39 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {F}\left({1}^{st}\left({j}\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
41 elovolmlem ${⊢}{F}\left({1}^{st}\left({j}\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}\left({1}^{st}\left({j}\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
42 40 41 sylib ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {F}\left({1}^{st}\left({j}\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
43 xp2nd ${⊢}{j}\in \left(ℕ×ℕ\right)\to {2}^{nd}\left({j}\right)\in ℕ$
44 37 43 syl ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {2}^{nd}\left({j}\right)\in ℕ$
45 42 44 ffvelrnd ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\in \left(\le \cap {ℝ}^{2}\right)$
46 45 elin2d ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\in {ℝ}^{2}$
47 xp2nd ${⊢}{F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℝ$
48 46 47 syl ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℝ$
49 xp1st ${⊢}{F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\in {ℝ}^{2}\to {1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℝ$
50 46 49 syl ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℝ$
51 48 50 resubcld ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℝ$
52 51 recnd ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\in ℂ$
53 22 23 28 30 52 fsumf1o ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)=\sum _{{m}=1}^{{K}}\left({2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)\right)$
54 11 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}$
55 34 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {J}\left({k}\right)\in \left(ℕ×ℕ\right)$
56 xp1st ${⊢}{J}\left({k}\right)\in \left(ℕ×ℕ\right)\to {1}^{st}\left({J}\left({k}\right)\right)\in ℕ$
57 55 56 syl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {1}^{st}\left({J}\left({k}\right)\right)\in ℕ$
58 54 57 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
59 elovolmlem ${⊢}{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}\left({1}^{st}\left({J}\left({k}\right)\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
60 58 59 sylib ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
61 xp2nd ${⊢}{J}\left({k}\right)\in \left(ℕ×ℕ\right)\to {2}^{nd}\left({J}\left({k}\right)\right)\in ℕ$
62 55 61 syl ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {2}^{nd}\left({J}\left({k}\right)\right)\in ℕ$
63 60 62 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)\in \left(\le \cap {ℝ}^{2}\right)$
64 63 9 fmptd ${⊢}{\phi }\to {H}:ℕ⟶\le \cap {ℝ}^{2}$
65 elfznn ${⊢}{m}\in \left(1\dots {K}\right)\to {m}\in ℕ$
66 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {H}=\left(\mathrm{abs}\circ -\right)\circ {H}$
67 66 ovolfsval ${⊢}\left({H}:ℕ⟶\le \cap {ℝ}^{2}\wedge {m}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\left({m}\right)={2}^{nd}\left({H}\left({m}\right)\right)-{1}^{st}\left({H}\left({m}\right)\right)$
68 64 65 67 syl2an ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\left({m}\right)={2}^{nd}\left({H}\left({m}\right)\right)-{1}^{st}\left({H}\left({m}\right)\right)$
69 65 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {m}\in ℕ$
70 2fveq3 ${⊢}{k}={m}\to {1}^{st}\left({J}\left({k}\right)\right)={1}^{st}\left({J}\left({m}\right)\right)$
71 70 fveq2d ${⊢}{k}={m}\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)$
72 2fveq3 ${⊢}{k}={m}\to {2}^{nd}\left({J}\left({k}\right)\right)={2}^{nd}\left({J}\left({m}\right)\right)$
73 71 72 fveq12d ${⊢}{k}={m}\to {F}\left({1}^{st}\left({J}\left({k}\right)\right)\right)\left({2}^{nd}\left({J}\left({k}\right)\right)\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)$
74 fvex ${⊢}{F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\in \mathrm{V}$
75 73 9 74 fvmpt ${⊢}{m}\in ℕ\to {H}\left({m}\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)$
76 69 75 syl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {H}\left({m}\right)={F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)$
77 76 fveq2d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({H}\left({m}\right)\right)={2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
78 76 fveq2d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {1}^{st}\left({H}\left({m}\right)\right)={1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
79 77 78 oveq12d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({H}\left({m}\right)\right)-{1}^{st}\left({H}\left({m}\right)\right)={2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
80 68 79 eqtrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\left({m}\right)={2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)$
81 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
82 14 81 eleqtrdi ${⊢}{\phi }\to {K}\in {ℤ}_{\ge 1}$
83 ffvelrn ${⊢}\left({H}:ℕ⟶\le \cap {ℝ}^{2}\wedge {m}\in ℕ\right)\to {H}\left({m}\right)\in \left(\le \cap {ℝ}^{2}\right)$
84 64 65 83 syl2an ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {H}\left({m}\right)\in \left(\le \cap {ℝ}^{2}\right)$
85 84 elin2d ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {H}\left({m}\right)\in {ℝ}^{2}$
86 xp2nd ${⊢}{H}\left({m}\right)\in {ℝ}^{2}\to {2}^{nd}\left({H}\left({m}\right)\right)\in ℝ$
87 85 86 syl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({H}\left({m}\right)\right)\in ℝ$
88 xp1st ${⊢}{H}\left({m}\right)\in {ℝ}^{2}\to {1}^{st}\left({H}\left({m}\right)\right)\in ℝ$
89 85 88 syl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {1}^{st}\left({H}\left({m}\right)\right)\in ℝ$
90 87 89 resubcld ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({H}\left({m}\right)\right)-{1}^{st}\left({H}\left({m}\right)\right)\in ℝ$
91 90 recnd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({H}\left({m}\right)\right)-{1}^{st}\left({H}\left({m}\right)\right)\in ℂ$
92 79 91 eqeltrrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {K}\right)\right)\to {2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)\in ℂ$
93 80 82 92 fsumser ${⊢}{\phi }\to \sum _{{m}=1}^{{K}}\left({2}^{nd}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({J}\left({m}\right)\right)\right)\left({2}^{nd}\left({J}\left({m}\right)\right)\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)\left({K}\right)$
94 53 93 eqtrd ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)\left({K}\right)$
95 8 fveq1i ${⊢}{U}\left({K}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {H}\right)\right)\left({K}\right)$
96 94 95 syl6eqr ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)={U}\left({K}\right)$
97 f1oeng ${⊢}\left(\left(1\dots {K}\right)\in \mathrm{Fin}\wedge \left({{J}↾}_{\left(1\dots {K}\right)}\right):\left(1\dots {K}\right)\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]\right)\to \left(1\dots {K}\right)\approx {J}\left[\left(1\dots {K}\right)\right]$
98 23 28 97 syl2anc ${⊢}{\phi }\to \left(1\dots {K}\right)\approx {J}\left[\left(1\dots {K}\right)\right]$
99 98 ensymd ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\approx \left(1\dots {K}\right)$
100 enfii ${⊢}\left(\left(1\dots {K}\right)\in \mathrm{Fin}\wedge {J}\left[\left(1\dots {K}\right)\right]\approx \left(1\dots {K}\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\in \mathrm{Fin}$
101 23 99 100 syl2anc ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\in \mathrm{Fin}$
102 101 51 fsumrecl ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)\in ℝ$
103 fzfid ${⊢}{\phi }\to \left(1\dots {L}\right)\in \mathrm{Fin}$
104 elfznn ${⊢}{n}\in \left(1\dots {L}\right)\to {n}\in ℕ$
105 104 4 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {vol}^{*}\left({A}\right)\in ℝ$
106 103 105 fsumrecl ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)\in ℝ$
107 6 rpred ${⊢}{\phi }\to {B}\in ℝ$
108 2nn ${⊢}2\in ℕ$
109 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
110 nnexpcl ${⊢}\left(2\in ℕ\wedge {n}\in {ℕ}_{0}\right)\to {2}^{{n}}\in ℕ$
111 108 109 110 sylancr ${⊢}{n}\in ℕ\to {2}^{{n}}\in ℕ$
112 104 111 syl ${⊢}{n}\in \left(1\dots {L}\right)\to {2}^{{n}}\in ℕ$
113 nndivre ${⊢}\left({B}\in ℝ\wedge {2}^{{n}}\in ℕ\right)\to \frac{{B}}{{2}^{{n}}}\in ℝ$
114 107 112 113 syl2an ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \frac{{B}}{{2}^{{n}}}\in ℝ$
115 103 114 fsumrecl ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)\in ℝ$
116 106 115 readdcld ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)+\sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)\in ℝ$
117 5 107 readdcld ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}\in ℝ$
118 relxp ${⊢}\mathrm{Rel}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
119 relres ${⊢}\mathrm{Rel}\left({{J}\left[\left(1\dots {K}\right)\right]↾}_{\left\{{n}\right\}}\right)$
120 elsni ${⊢}{x}\in \left\{{n}\right\}\to {x}={n}$
121 120 opeq1d ${⊢}{x}\in \left\{{n}\right\}\to ⟨{x},{y}⟩=⟨{n},{y}⟩$
122 121 eleq1d ${⊢}{x}\in \left\{{n}\right\}\to \left(⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]↔⟨{n},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\right)$
123 vex ${⊢}{n}\in \mathrm{V}$
124 vex ${⊢}{y}\in \mathrm{V}$
125 123 124 elimasn ${⊢}{y}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]↔⟨{n},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]$
126 122 125 syl6bbr ${⊢}{x}\in \left\{{n}\right\}\to \left(⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]↔{y}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
127 126 pm5.32i ${⊢}\left({x}\in \left\{{n}\right\}\wedge ⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\right)↔\left({x}\in \left\{{n}\right\}\wedge {y}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
128 124 opelresi ${⊢}⟨{x},{y}⟩\in \left({{J}\left[\left(1\dots {K}\right)\right]↾}_{\left\{{n}\right\}}\right)↔\left({x}\in \left\{{n}\right\}\wedge ⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\right)$
129 opelxp ${⊢}⟨{x},{y}⟩\in \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)↔\left({x}\in \left\{{n}\right\}\wedge {y}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
130 127 128 129 3bitr4ri ${⊢}⟨{x},{y}⟩\in \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)↔⟨{x},{y}⟩\in \left({{J}\left[\left(1\dots {K}\right)\right]↾}_{\left\{{n}\right\}}\right)$
131 118 119 130 eqrelriiv ${⊢}\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]={{J}\left[\left(1\dots {K}\right)\right]↾}_{\left\{{n}\right\}}$
132 df-res ${⊢}{{J}\left[\left(1\dots {K}\right)\right]↾}_{\left\{{n}\right\}}={J}\left[\left(1\dots {K}\right)\right]\cap \left(\left\{{n}\right\}×\mathrm{V}\right)$
133 131 132 eqtri ${⊢}\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]={J}\left[\left(1\dots {K}\right)\right]\cap \left(\left\{{n}\right\}×\mathrm{V}\right)$
134 133 a1i ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]={J}\left[\left(1\dots {K}\right)\right]\cap \left(\left\{{n}\right\}×\mathrm{V}\right)$
135 134 iuneq2dv ${⊢}{\phi }\to \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)=\bigcup _{{n}=1}^{{L}}\left({J}\left[\left(1\dots {K}\right)\right]\cap \left(\left\{{n}\right\}×\mathrm{V}\right)\right)$
136 iunin2 ${⊢}\bigcup _{{n}=1}^{{L}}\left({J}\left[\left(1\dots {K}\right)\right]\cap \left(\left\{{n}\right\}×\mathrm{V}\right)\right)={J}\left[\left(1\dots {K}\right)\right]\cap \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)$
137 135 136 syl6eq ${⊢}{\phi }\to \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)={J}\left[\left(1\dots {K}\right)\right]\cap \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)$
138 relxp ${⊢}\mathrm{Rel}\left(ℕ×ℕ\right)$
139 relss ${⊢}{J}\left[\left(1\dots {K}\right)\right]\subseteq ℕ×ℕ\to \left(\mathrm{Rel}\left(ℕ×ℕ\right)\to \mathrm{Rel}{J}\left[\left(1\dots {K}\right)\right]\right)$
140 36 138 139 mpisyl ${⊢}{\phi }\to \mathrm{Rel}{J}\left[\left(1\dots {K}\right)\right]$
141 34 ffnd ${⊢}{\phi }\to {J}Fnℕ$
142 fveq2 ${⊢}{j}={J}\left({w}\right)\to {1}^{st}\left({j}\right)={1}^{st}\left({J}\left({w}\right)\right)$
143 142 breq1d ${⊢}{j}={J}\left({w}\right)\to \left({1}^{st}\left({j}\right)\le {L}↔{1}^{st}\left({J}\left({w}\right)\right)\le {L}\right)$
144 143 ralima ${⊢}\left({J}Fnℕ\wedge \left(1\dots {K}\right)\subseteq ℕ\right)\to \left(\forall {j}\in {J}\left[\left(1\dots {K}\right)\right]\phantom{\rule{.4em}{0ex}}{1}^{st}\left({j}\right)\le {L}↔\forall {w}\in \left(1\dots {K}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {L}\right)$
145 141 26 144 sylancl ${⊢}{\phi }\to \left(\forall {j}\in {J}\left[\left(1\dots {K}\right)\right]\phantom{\rule{.4em}{0ex}}{1}^{st}\left({j}\right)\le {L}↔\forall {w}\in \left(1\dots {K}\right)\phantom{\rule{.4em}{0ex}}{1}^{st}\left({J}\left({w}\right)\right)\le {L}\right)$
146 16 145 mpbird ${⊢}{\phi }\to \forall {j}\in {J}\left[\left(1\dots {K}\right)\right]\phantom{\rule{.4em}{0ex}}{1}^{st}\left({j}\right)\le {L}$
147 146 r19.21bi ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {1}^{st}\left({j}\right)\le {L}$
148 39 81 eleqtrdi ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {1}^{st}\left({j}\right)\in {ℤ}_{\ge 1}$
149 15 adantr ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {L}\in ℤ$
150 elfz5 ${⊢}\left({1}^{st}\left({j}\right)\in {ℤ}_{\ge 1}\wedge {L}\in ℤ\right)\to \left({1}^{st}\left({j}\right)\in \left(1\dots {L}\right)↔{1}^{st}\left({j}\right)\le {L}\right)$
151 148 149 150 syl2anc ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to \left({1}^{st}\left({j}\right)\in \left(1\dots {L}\right)↔{1}^{st}\left({j}\right)\le {L}\right)$
152 147 151 mpbird ${⊢}\left({\phi }\wedge {j}\in {J}\left[\left(1\dots {K}\right)\right]\right)\to {1}^{st}\left({j}\right)\in \left(1\dots {L}\right)$
153 152 ralrimiva ${⊢}{\phi }\to \forall {j}\in {J}\left[\left(1\dots {K}\right)\right]\phantom{\rule{.4em}{0ex}}{1}^{st}\left({j}\right)\in \left(1\dots {L}\right)$
154 vex ${⊢}{x}\in \mathrm{V}$
155 154 124 op1std ${⊢}{j}=⟨{x},{y}⟩\to {1}^{st}\left({j}\right)={x}$
156 155 eleq1d ${⊢}{j}=⟨{x},{y}⟩\to \left({1}^{st}\left({j}\right)\in \left(1\dots {L}\right)↔{x}\in \left(1\dots {L}\right)\right)$
157 156 rspccv ${⊢}\forall {j}\in {J}\left[\left(1\dots {K}\right)\right]\phantom{\rule{.4em}{0ex}}{1}^{st}\left({j}\right)\in \left(1\dots {L}\right)\to \left(⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\to {x}\in \left(1\dots {L}\right)\right)$
158 153 157 syl ${⊢}{\phi }\to \left(⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\to {x}\in \left(1\dots {L}\right)\right)$
159 opelxp ${⊢}⟨{x},{y}⟩\in \left(\bigcup _{{n}=1}^{{L}}\left\{{n}\right\}×\mathrm{V}\right)↔\left({x}\in \bigcup _{{n}=1}^{{L}}\left\{{n}\right\}\wedge {y}\in \mathrm{V}\right)$
160 124 biantru ${⊢}{x}\in \bigcup _{{n}=1}^{{L}}\left\{{n}\right\}↔\left({x}\in \bigcup _{{n}=1}^{{L}}\left\{{n}\right\}\wedge {y}\in \mathrm{V}\right)$
161 iunid ${⊢}\bigcup _{{n}=1}^{{L}}\left\{{n}\right\}=\left(1\dots {L}\right)$
162 161 eleq2i ${⊢}{x}\in \bigcup _{{n}=1}^{{L}}\left\{{n}\right\}↔{x}\in \left(1\dots {L}\right)$
163 159 160 162 3bitr2i ${⊢}⟨{x},{y}⟩\in \left(\bigcup _{{n}=1}^{{L}}\left\{{n}\right\}×\mathrm{V}\right)↔{x}\in \left(1\dots {L}\right)$
164 158 163 syl6ibr ${⊢}{\phi }\to \left(⟨{x},{y}⟩\in {J}\left[\left(1\dots {K}\right)\right]\to ⟨{x},{y}⟩\in \left(\bigcup _{{n}=1}^{{L}}\left\{{n}\right\}×\mathrm{V}\right)\right)$
165 140 164 relssdv ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\subseteq \bigcup _{{n}=1}^{{L}}\left\{{n}\right\}×\mathrm{V}$
166 xpiundir ${⊢}\bigcup _{{n}=1}^{{L}}\left\{{n}\right\}×\mathrm{V}=\bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)$
167 165 166 sseqtrdi ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\subseteq \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)$
168 df-ss ${⊢}{J}\left[\left(1\dots {K}\right)\right]\subseteq \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)↔{J}\left[\left(1\dots {K}\right)\right]\cap \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)={J}\left[\left(1\dots {K}\right)\right]$
169 167 168 sylib ${⊢}{\phi }\to {J}\left[\left(1\dots {K}\right)\right]\cap \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×\mathrm{V}\right)={J}\left[\left(1\dots {K}\right)\right]$
170 137 169 eqtrd ${⊢}{\phi }\to \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)={J}\left[\left(1\dots {K}\right)\right]$
171 170 101 eqeltrd ${⊢}{\phi }\to \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\in \mathrm{Fin}$
172 ssiun2 ${⊢}{n}\in \left(1\dots {L}\right)\to \left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\subseteq \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
173 ssfi ${⊢}\left(\bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\in \mathrm{Fin}\wedge \left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\subseteq \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to \left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}$
174 171 172 173 syl2an ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}$
175 2ndconst ${⊢}{n}\in \mathrm{V}\to \left({{2}^{nd}↾}_{\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)}\right):\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]$
176 175 elv ${⊢}\left({{2}^{nd}↾}_{\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)}\right):\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]$
177 f1oeng ${⊢}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}\wedge \left({{2}^{nd}↾}_{\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)}\right):\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\underset{1-1 onto}{⟶}{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\to \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\approx {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]$
178 174 176 177 sylancl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\approx {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]$
179 178 ensymd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\approx \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)$
180 enfii ${⊢}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}\wedge {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\approx \left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}$
181 174 179 180 syl2anc ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\in \mathrm{Fin}$
182 ffvelrn ${⊢}\left({F}:ℕ⟶{\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\wedge {n}\in ℕ\right)\to {F}\left({n}\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
183 11 104 182 syl2an ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {F}\left({n}\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)$
184 elovolmlem ${⊢}{F}\left({n}\right)\in \left({\left(\le \cap {ℝ}^{2}\right)}^{ℕ}\right)↔{F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
185 183 184 sylib ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
186 185 adantrr ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}$
187 imassrn ${⊢}{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\subseteq \mathrm{ran}{J}\left[\left(1\dots {K}\right)\right]$
188 36 adantr ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\subseteq ℕ×ℕ$
189 rnss ${⊢}{J}\left[\left(1\dots {K}\right)\right]\subseteq ℕ×ℕ\to \mathrm{ran}{J}\left[\left(1\dots {K}\right)\right]\subseteq \mathrm{ran}\left(ℕ×ℕ\right)$
190 188 189 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{J}\left[\left(1\dots {K}\right)\right]\subseteq \mathrm{ran}\left(ℕ×ℕ\right)$
191 rnxpid ${⊢}\mathrm{ran}\left(ℕ×ℕ\right)=ℕ$
192 190 191 sseqtrdi ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{J}\left[\left(1\dots {K}\right)\right]\subseteq ℕ$
193 187 192 sstrid ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\subseteq ℕ$
194 193 sseld ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left({i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\to {i}\in ℕ\right)$
195 194 impr ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {i}\in ℕ$
196 186 195 ffvelrnd ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {F}\left({n}\right)\left({i}\right)\in \left(\le \cap {ℝ}^{2}\right)$
197 196 elin2d ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {F}\left({n}\right)\left({i}\right)\in {ℝ}^{2}$
198 xp2nd ${⊢}{F}\left({n}\right)\left({i}\right)\in {ℝ}^{2}\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
199 197 198 syl ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
200 xp1st ${⊢}{F}\left({n}\right)\left({i}\right)\in {ℝ}^{2}\to {1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
201 197 200 syl ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
202 199 201 resubcld ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
203 202 anassrs ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
204 181 203 fsumrecl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)\in ℝ$
205 107 111 113 syl2an ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{B}}{{2}^{{n}}}\in ℝ$
206 4 205 readdcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\in ℝ$
207 104 206 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\in ℝ$
208 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)=\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)$
209 208 7 ovolsf ${⊢}{F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
210 185 209 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {S}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
211 210 frnd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{S}\subseteq \left[0,\mathrm{+\infty }\right)$
212 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
213 211 212 sstrdi ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{S}\subseteq {ℝ}^{*}$
214 supxrcl ${⊢}\mathrm{ran}{S}\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
215 213 214 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}$
216 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
217 216 a1i ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
218 105 rexrd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {vol}^{*}\left({A}\right)\in {ℝ}^{*}$
219 105 mnfltd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{-\infty }<{vol}^{*}\left({A}\right)$
220 104 12 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)$
221 7 ovollb ${⊢}\left({F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}\wedge {A}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\left({n}\right)\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
222 185 220 221 syl2anc ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
223 217 218 215 219 222 xrltletrd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{-\infty }
224 104 13 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
225 xrre ${⊢}\left(\left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }
226 215 207 223 224 225 syl22anc ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ$
227 1zzd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to 1\in ℤ$
228 208 ovolfsval ${⊢}\left({F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}\wedge {i}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\left({i}\right)={2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)$
229 185 228 sylan ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\left({i}\right)={2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)$
230 208 ovolfsf ${⊢}{F}\left({n}\right):ℕ⟶\le \cap {ℝ}^{2}\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
231 185 230 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
232 231 ffvelrnda ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\left({i}\right)\in \left[0,\mathrm{+\infty }\right)$
233 229 232 eqeltrrd ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in \left[0,\mathrm{+\infty }\right)$
234 elrege0 ${⊢}{2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in \left[0,\mathrm{+\infty }\right)↔\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ\wedge 0\le {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)$
235 233 234 sylib ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to \left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ\wedge 0\le {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)$
236 235 simpld ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℝ$
237 235 simprd ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {i}\in ℕ\right)\to 0\le {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)$
238 supxrub ${⊢}\left(\mathrm{ran}{S}\subseteq {ℝ}^{*}\wedge {z}\in \mathrm{ran}{S}\right)\to {z}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
239 213 238 sylan ${⊢}\left(\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\wedge {z}\in \mathrm{ran}{S}\right)\to {z}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
240 239 ralrimiva ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
241 brralrspcev ${⊢}\left(sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\in ℝ\wedge \forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
242 226 240 241 syl2anc ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}$
243 210 ffnd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {S}Fnℕ$
244 breq1 ${⊢}{z}={S}\left({k}\right)\to \left({z}\le {x}↔{S}\left({k}\right)\le {x}\right)$
245 244 ralrn ${⊢}{S}Fnℕ\to \left(\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {x}\right)$
246 243 245 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left(\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {x}\right)$
247 246 rexbidv ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {x}\right)$
248 242 247 mpbid ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{S}\left({k}\right)\le {x}$
249 81 7 227 229 236 237 248 isumsup2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {S}⇝sup\left(\mathrm{ran}{S},ℝ,<\right)$
250 7 249 eqbrtrrid ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)⇝sup\left(\mathrm{ran}{S},ℝ,<\right)$
251 climrel ${⊢}\mathrm{Rel}⇝$
252 251 releldmi ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)⇝sup\left(\mathrm{ran}{S},ℝ,<\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)\in \mathrm{dom}⇝$
253 250 252 syl ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\left({n}\right)\right)\right)\in \mathrm{dom}⇝$
254 81 227 181 193 229 236 237 253 isumless ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)\le \sum _{{i}\in ℕ}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)$
255 81 7 227 229 236 237 248 isumsup ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in ℕ}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)=sup\left(\mathrm{ran}{S},ℝ,<\right)$
256 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
257 211 256 sstrdi ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{S}\subseteq ℝ$
258 1nn ${⊢}1\in ℕ$
259 210 fdmd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{dom}{S}=ℕ$
260 258 259 eleqtrrid ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to 1\in \mathrm{dom}{S}$
261 260 ne0d ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{dom}{S}\ne \varnothing$
262 dm0rn0 ${⊢}\mathrm{dom}{S}=\varnothing ↔\mathrm{ran}{S}=\varnothing$
263 262 necon3bii ${⊢}\mathrm{dom}{S}\ne \varnothing ↔\mathrm{ran}{S}\ne \varnothing$
264 261 263 sylib ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \mathrm{ran}{S}\ne \varnothing$
265 supxrre ${⊢}\left(\mathrm{ran}{S}\subseteq ℝ\wedge \mathrm{ran}{S}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{S}\phantom{\rule{.4em}{0ex}}{z}\le {x}\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{S},ℝ,<\right)$
266 257 264 242 265 syl3anc ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)=sup\left(\mathrm{ran}{S},ℝ,<\right)$
267 255 266 eqtr4d ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in ℕ}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)=sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
268 254 267 breqtrd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)\le sup\left(\mathrm{ran}{S},{ℝ}^{*},<\right)$
269 204 226 207 268 224 letrd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)\le {vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)$
270 103 204 207 269 fsumle ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)\le \sum _{{n}=1}^{{L}}\left({vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)$
271 vex ${⊢}{i}\in \mathrm{V}$
272 123 271 op1std ${⊢}{j}=⟨{n},{i}⟩\to {1}^{st}\left({j}\right)={n}$
273 272 fveq2d ${⊢}{j}=⟨{n},{i}⟩\to {F}\left({1}^{st}\left({j}\right)\right)={F}\left({n}\right)$
274 123 271 op2ndd ${⊢}{j}=⟨{n},{i}⟩\to {2}^{nd}\left({j}\right)={i}$
275 273 274 fveq12d ${⊢}{j}=⟨{n},{i}⟩\to {F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)={F}\left({n}\right)\left({i}\right)$
276 275 fveq2d ${⊢}{j}=⟨{n},{i}⟩\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)$
277 275 fveq2d ${⊢}{j}=⟨{n},{i}⟩\to {1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)$
278 276 277 oveq12d ${⊢}{j}=⟨{n},{i}⟩\to {2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)={2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)$
279 202 recnd ${⊢}\left({\phi }\wedge \left({n}\in \left(1\dots {L}\right)\wedge {i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)\right)\to {2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\in ℂ$
280 278 103 181 279 fsum2d ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)=\sum _{{j}\in \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)$
281 170 sumeq1d ${⊢}{\phi }\to \sum _{{j}\in \bigcup _{{n}=1}^{{L}}\left(\left\{{n}\right\}×{J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]\right)}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)=\sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)$
282 280 281 eqtrd ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\sum _{{i}\in {J}\left[\left(1\dots {K}\right)\right]\left[\left\{{n}\right\}\right]}\left({2}^{nd}\left({F}\left({n}\right)\left({i}\right)\right)-{1}^{st}\left({F}\left({n}\right)\left({i}\right)\right)\right)=\sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)$
283 105 recnd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {vol}^{*}\left({A}\right)\in ℂ$
284 114 recnd ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to \frac{{B}}{{2}^{{n}}}\in ℂ$
285 103 283 284 fsumadd ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\left({vol}^{*}\left({A}\right)+\left(\frac{{B}}{{2}^{{n}}}\right)\right)=\sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)+\sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)$
286 270 282 285 3brtr3d ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)\le \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)+\sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)$
287 1zzd ${⊢}{\phi }\to 1\in ℤ$
288 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
289 2 fvmpt2 ${⊢}\left({n}\in ℕ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\to {G}\left({n}\right)={vol}^{*}\left({A}\right)$
290 288 4 289 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\left({n}\right)={vol}^{*}\left({A}\right)$
291 290 4 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\left({n}\right)\in ℝ$
292 81 287 291 serfre ${⊢}{\phi }\to seq1\left(+,{G}\right):ℕ⟶ℝ$
293 1 feq1i ${⊢}{T}:ℕ⟶ℝ↔seq1\left(+,{G}\right):ℕ⟶ℝ$
294 292 293 sylibr ${⊢}{\phi }\to {T}:ℕ⟶ℝ$
295 294 frnd ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq ℝ$
296 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
297 295 296 sstrdi ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq {ℝ}^{*}$
298 104 290 sylan2 ${⊢}\left({\phi }\wedge {n}\in \left(1\dots {L}\right)\right)\to {G}\left({n}\right)={vol}^{*}\left({A}\right)$
299 1red ${⊢}{\phi }\to 1\in ℝ$
300 ffvelrn ${⊢}\left({J}:ℕ⟶ℕ×ℕ\wedge 1\in ℕ\right)\to {J}\left(1\right)\in \left(ℕ×ℕ\right)$
301 34 258 300 sylancl ${⊢}{\phi }\to {J}\left(1\right)\in \left(ℕ×ℕ\right)$
302 xp1st ${⊢}{J}\left(1\right)\in \left(ℕ×ℕ\right)\to {1}^{st}\left({J}\left(1\right)\right)\in ℕ$
303 301 302 syl ${⊢}{\phi }\to {1}^{st}\left({J}\left(1\right)\right)\in ℕ$
304 303 nnred ${⊢}{\phi }\to {1}^{st}\left({J}\left(1\right)\right)\in ℝ$
305 15 zred ${⊢}{\phi }\to {L}\in ℝ$
306 303 nnge1d ${⊢}{\phi }\to 1\le {1}^{st}\left({J}\left(1\right)\right)$
307 2fveq3 ${⊢}{w}=1\to {1}^{st}\left({J}\left({w}\right)\right)={1}^{st}\left({J}\left(1\right)\right)$
308 307 breq1d ${⊢}{w}=1\to \left({1}^{st}\left({J}\left({w}\right)\right)\le {L}↔{1}^{st}\left({J}\left(1\right)\right)\le {L}\right)$
309 eluzfz1 ${⊢}{K}\in {ℤ}_{\ge 1}\to 1\in \left(1\dots {K}\right)$
310 82 309 syl ${⊢}{\phi }\to 1\in \left(1\dots {K}\right)$
311 308 16 310 rspcdva ${⊢}{\phi }\to {1}^{st}\left({J}\left(1\right)\right)\le {L}$
312 299 304 305 306 311 letrd ${⊢}{\phi }\to 1\le {L}$
313 elnnz1 ${⊢}{L}\in ℕ↔\left({L}\in ℤ\wedge 1\le {L}\right)$
314 15 312 313 sylanbrc ${⊢}{\phi }\to {L}\in ℕ$
315 314 81 eleqtrdi ${⊢}{\phi }\to {L}\in {ℤ}_{\ge 1}$
316 298 315 283 fsumser ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)=seq1\left(+,{G}\right)\left({L}\right)$
317 seqfn ${⊢}1\in ℤ\to seq1\left(+,{G}\right)Fn{ℤ}_{\ge 1}$
318 287 317 syl ${⊢}{\phi }\to seq1\left(+,{G}\right)Fn{ℤ}_{\ge 1}$
319 fnfvelrn ${⊢}\left(seq1\left(+,{G}\right)Fn{ℤ}_{\ge 1}\wedge {L}\in {ℤ}_{\ge 1}\right)\to seq1\left(+,{G}\right)\left({L}\right)\in \mathrm{ran}seq1\left(+,{G}\right)$
320 318 315 319 syl2anc ${⊢}{\phi }\to seq1\left(+,{G}\right)\left({L}\right)\in \mathrm{ran}seq1\left(+,{G}\right)$
321 1 rneqi ${⊢}\mathrm{ran}{T}=\mathrm{ran}seq1\left(+,{G}\right)$
322 320 321 eleqtrrdi ${⊢}{\phi }\to seq1\left(+,{G}\right)\left({L}\right)\in \mathrm{ran}{T}$
323 316 322 eqeltrd ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)\in \mathrm{ran}{T}$
324 supxrub ${⊢}\left(\mathrm{ran}{T}\subseteq {ℝ}^{*}\wedge \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)\in \mathrm{ran}{T}\right)\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
325 297 323 324 syl2anc ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
326 107 recnd ${⊢}{\phi }\to {B}\in ℂ$
327 geo2sum ${⊢}\left({L}\in ℕ\wedge {B}\in ℂ\right)\to \sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)={B}-\left(\frac{{B}}{{2}^{{L}}}\right)$
328 314 326 327 syl2anc ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)={B}-\left(\frac{{B}}{{2}^{{L}}}\right)$
329 314 nnnn0d ${⊢}{\phi }\to {L}\in {ℕ}_{0}$
330 nnexpcl ${⊢}\left(2\in ℕ\wedge {L}\in {ℕ}_{0}\right)\to {2}^{{L}}\in ℕ$
331 108 329 330 sylancr ${⊢}{\phi }\to {2}^{{L}}\in ℕ$
332 331 nnrpd ${⊢}{\phi }\to {2}^{{L}}\in {ℝ}^{+}$
333 6 332 rpdivcld ${⊢}{\phi }\to \frac{{B}}{{2}^{{L}}}\in {ℝ}^{+}$
334 333 rpge0d ${⊢}{\phi }\to 0\le \frac{{B}}{{2}^{{L}}}$
335 107 331 nndivred ${⊢}{\phi }\to \frac{{B}}{{2}^{{L}}}\in ℝ$
336 107 335 subge02d ${⊢}{\phi }\to \left(0\le \frac{{B}}{{2}^{{L}}}↔{B}-\left(\frac{{B}}{{2}^{{L}}}\right)\le {B}\right)$
337 334 336 mpbid ${⊢}{\phi }\to {B}-\left(\frac{{B}}{{2}^{{L}}}\right)\le {B}$
338 328 337 eqbrtrd ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)\le {B}$
339 106 115 5 107 325 338 le2addd ${⊢}{\phi }\to \sum _{{n}=1}^{{L}}{vol}^{*}\left({A}\right)+\sum _{{n}=1}^{{L}}\left(\frac{{B}}{{2}^{{n}}}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
340 102 116 117 286 339 letrd ${⊢}{\phi }\to \sum _{{j}\in {J}\left[\left(1\dots {K}\right)\right]}\left({2}^{nd}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)-{1}^{st}\left({F}\left({1}^{st}\left({j}\right)\right)\left({2}^{nd}\left({j}\right)\right)\right)\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$
341 96 340 eqbrtrrd ${⊢}{\phi }\to {U}\left({K}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)+{B}$