# Metamath Proof Explorer

## Theorem uniioombllem3

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
uniioombl.a ${⊢}{A}=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
uniioombl.e ${⊢}{\phi }\to {vol}^{*}\left({E}\right)\in ℝ$
uniioombl.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
uniioombl.g ${⊢}{\phi }\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
uniioombl.s ${⊢}{\phi }\to {E}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
uniioombl.t ${⊢}{T}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)$
uniioombl.v ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\le {vol}^{*}\left({E}\right)+{C}$
uniioombl.m ${⊢}{\phi }\to {M}\in ℕ$
uniioombl.m2 ${⊢}{\phi }\to \left|{T}\left({M}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
uniioombl.k ${⊢}{K}=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]$
Assertion uniioombllem3 ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)<{vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left({K}\setminus {A}\right)+{C}+{C}$

### Proof

Step Hyp Ref Expression
1 uniioombl.1 ${⊢}{\phi }\to {F}:ℕ⟶\le \cap {ℝ}^{2}$
2 uniioombl.2 ${⊢}{\phi }\to \underset{{x}\in ℕ}{Disj}\left(.\right)\left({F}\left({x}\right)\right)$
3 uniioombl.3 ${⊢}{S}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right)\right)$
4 uniioombl.a ${⊢}{A}=\bigcup \mathrm{ran}\left(\left(.\right)\circ {F}\right)$
5 uniioombl.e ${⊢}{\phi }\to {vol}^{*}\left({E}\right)\in ℝ$
6 uniioombl.c ${⊢}{\phi }\to {C}\in {ℝ}^{+}$
7 uniioombl.g ${⊢}{\phi }\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
8 uniioombl.s ${⊢}{\phi }\to {E}\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
9 uniioombl.t ${⊢}{T}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)$
10 uniioombl.v ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\le {vol}^{*}\left({E}\right)+{C}$
11 uniioombl.m ${⊢}{\phi }\to {M}\in ℕ$
12 uniioombl.m2 ${⊢}{\phi }\to \left|{T}\left({M}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}$
13 uniioombl.k ${⊢}{K}=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]$
14 inss1 ${⊢}{E}\cap {A}\subseteq {E}$
15 14 a1i ${⊢}{\phi }\to {E}\cap {A}\subseteq {E}$
16 7 uniiccdif ${⊢}{\phi }\to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {G}\right)\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left[.\right]\circ {G}\right)\setminus \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)=0\right)$
17 16 simpld ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq \bigcup \mathrm{ran}\left(\left[.\right]\circ {G}\right)$
18 ovolficcss ${⊢}{G}:ℕ⟶\le \cap {ℝ}^{2}\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {G}\right)\subseteq ℝ$
19 7 18 syl ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left[.\right]\circ {G}\right)\subseteq ℝ$
20 17 19 sstrd ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq ℝ$
21 8 20 sstrd ${⊢}{\phi }\to {E}\subseteq ℝ$
22 ovolsscl ${⊢}\left({E}\cap {A}\subseteq {E}\wedge {E}\subseteq ℝ\wedge {vol}^{*}\left({E}\right)\in ℝ\right)\to {vol}^{*}\left({E}\cap {A}\right)\in ℝ$
23 15 21 5 22 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)\in ℝ$
24 difssd ${⊢}{\phi }\to {E}\setminus {A}\subseteq {E}$
25 ovolsscl ${⊢}\left({E}\setminus {A}\subseteq {E}\wedge {E}\subseteq ℝ\wedge {vol}^{*}\left({E}\right)\in ℝ\right)\to {vol}^{*}\left({E}\setminus {A}\right)\in ℝ$
26 24 21 5 25 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({E}\setminus {A}\right)\in ℝ$
27 inss1 ${⊢}{K}\cap {A}\subseteq {K}$
28 27 a1i ${⊢}{\phi }\to {K}\cap {A}\subseteq {K}$
29 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3a ${⊢}{\phi }\to \left({K}=\bigcup _{{j}=1}^{{M}}\left(.\right)\left({G}\left({j}\right)\right)\wedge {vol}^{*}\left({K}\right)\in ℝ\right)$
30 29 simpld ${⊢}{\phi }\to {K}=\bigcup _{{j}=1}^{{M}}\left(.\right)\left({G}\left({j}\right)\right)$
31 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
32 elfznn ${⊢}{j}\in \left(1\dots {M}\right)\to {j}\in ℕ$
33 ffvelrn ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {j}\in ℕ\right)\to {G}\left({j}\right)\in \left(\le \cap {ℝ}^{2}\right)$
34 7 32 33 syl2an ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {G}\left({j}\right)\in \left(\le \cap {ℝ}^{2}\right)$
35 31 34 sseldi ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {G}\left({j}\right)\in {ℝ}^{2}$
36 1st2nd2 ${⊢}{G}\left({j}\right)\in {ℝ}^{2}\to {G}\left({j}\right)=⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩$
37 35 36 syl ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {G}\left({j}\right)=⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩$
38 37 fveq2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩\right)$
39 df-ov ${⊢}\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)=\left(.\right)\left(⟨{1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)⟩\right)$
40 38 39 syl6eqr ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)=\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)$
41 ioossre ${⊢}\left({1}^{st}\left({G}\left({j}\right)\right),{2}^{nd}\left({G}\left({j}\right)\right)\right)\subseteq ℝ$
42 40 41 eqsstrdi ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
43 42 ralrimiva ${⊢}{\phi }\to \forall {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}\left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
44 iunss ${⊢}\bigcup _{{j}=1}^{{M}}\left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ↔\forall {j}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}\left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
45 43 44 sylibr ${⊢}{\phi }\to \bigcup _{{j}=1}^{{M}}\left(.\right)\left({G}\left({j}\right)\right)\subseteq ℝ$
46 30 45 eqsstrd ${⊢}{\phi }\to {K}\subseteq ℝ$
47 29 simprd ${⊢}{\phi }\to {vol}^{*}\left({K}\right)\in ℝ$
48 ovolsscl ${⊢}\left({K}\cap {A}\subseteq {K}\wedge {K}\subseteq ℝ\wedge {vol}^{*}\left({K}\right)\in ℝ\right)\to {vol}^{*}\left({K}\cap {A}\right)\in ℝ$
49 28 46 47 48 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)\in ℝ$
50 6 rpred ${⊢}{\phi }\to {C}\in ℝ$
51 49 50 readdcld ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)+{C}\in ℝ$
52 difssd ${⊢}{\phi }\to {K}\setminus {A}\subseteq {K}$
53 ovolsscl ${⊢}\left({K}\setminus {A}\subseteq {K}\wedge {K}\subseteq ℝ\wedge {vol}^{*}\left({K}\right)\in ℝ\right)\to {vol}^{*}\left({K}\setminus {A}\right)\in ℝ$
54 52 46 47 53 syl3anc ${⊢}{\phi }\to {vol}^{*}\left({K}\setminus {A}\right)\in ℝ$
55 54 50 readdcld ${⊢}{\phi }\to {vol}^{*}\left({K}\setminus {A}\right)+{C}\in ℝ$
56 ssun2 ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
57 ioof ${⊢}\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ$
58 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
59 31 58 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
60 fss ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}\right)\to {G}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
61 7 59 60 sylancl ${⊢}{\phi }\to {G}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}$
62 fco ${⊢}\left(\left(.\right):{ℝ}^{*}×{ℝ}^{*}⟶𝒫ℝ\wedge {G}:ℕ⟶{ℝ}^{*}×{ℝ}^{*}\right)\to \left(\left(.\right)\circ {G}\right):ℕ⟶𝒫ℝ$
63 57 61 62 sylancr ${⊢}{\phi }\to \left(\left(.\right)\circ {G}\right):ℕ⟶𝒫ℝ$
64 63 ffnd ${⊢}{\phi }\to \left(\left(.\right)\circ {G}\right)Fnℕ$
65 fnima ${⊢}\left(\left(.\right)\circ {G}\right)Fnℕ\to \left(\left(.\right)\circ {G}\right)\left[ℕ\right]=\mathrm{ran}\left(\left(.\right)\circ {G}\right)$
66 64 65 syl ${⊢}{\phi }\to \left(\left(.\right)\circ {G}\right)\left[ℕ\right]=\mathrm{ran}\left(\left(.\right)\circ {G}\right)$
67 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
68 11 peano2nnd ${⊢}{\phi }\to {M}+1\in ℕ$
69 68 67 eleqtrdi ${⊢}{\phi }\to {M}+1\in {ℤ}_{\ge 1}$
70 uzsplit ${⊢}{M}+1\in {ℤ}_{\ge 1}\to {ℤ}_{\ge 1}=\left(1\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
71 69 70 syl ${⊢}{\phi }\to {ℤ}_{\ge 1}=\left(1\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
72 67 71 syl5eq ${⊢}{\phi }\to ℕ=\left(1\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
73 11 nncnd ${⊢}{\phi }\to {M}\in ℂ$
74 ax-1cn ${⊢}1\in ℂ$
75 pncan ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}+1-1={M}$
76 73 74 75 sylancl ${⊢}{\phi }\to {M}+1-1={M}$
77 76 oveq2d ${⊢}{\phi }\to \left(1\dots {M}+1-1\right)=\left(1\dots {M}\right)$
78 77 uneq1d ${⊢}{\phi }\to \left(1\dots {M}+1-1\right)\cup {ℤ}_{\ge \left({M}+1\right)}=\left(1\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
79 72 78 eqtrd ${⊢}{\phi }\to ℕ=\left(1\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}$
80 79 imaeq2d ${⊢}{\phi }\to \left(\left(.\right)\circ {G}\right)\left[ℕ\right]=\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}\right]$
81 66 80 eqtr3d ${⊢}{\phi }\to \mathrm{ran}\left(\left(.\right)\circ {G}\right)=\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}\right]$
82 imaundi ${⊢}\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\cup {ℤ}_{\ge \left({M}+1\right)}\right]=\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
83 81 82 syl6eq ${⊢}{\phi }\to \mathrm{ran}\left(\left(.\right)\circ {G}\right)=\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
84 83 unieqd ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)=\bigcup \left(\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
85 uniun ${⊢}\bigcup \left(\left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
86 84 85 syl6eq ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
87 13 uneq1i ${⊢}{K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\bigcup \left(\left(.\right)\circ {G}\right)\left[\left(1\dots {M}\right)\right]\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
88 86 87 syl6eqr ${⊢}{\phi }\to \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)={K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
89 56 88 sseqtrrid ${⊢}{\phi }\to \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
90 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
91 ssid ${⊢}\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
92 9 ovollb ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
93 7 91 92 sylancl ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
94 ovollecl ${⊢}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq ℝ\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right)\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\in ℝ$
95 20 90 93 94 syl3anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\in ℝ$
96 ovolsscl ${⊢}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
97 89 20 95 96 syl3anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
98 49 97 readdcld ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
99 unss1 ${⊢}{K}\cap {A}\subseteq {K}\to \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
100 27 99 ax-mp ${⊢}\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
101 100 88 sseqtrrid ${⊢}{\phi }\to \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
102 ovolsscl ${⊢}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
103 101 20 95 102 syl3anc ${⊢}{\phi }\to {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
104 8 88 sseqtrd ${⊢}{\phi }\to {E}\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
105 104 ssrind ${⊢}{\phi }\to {E}\cap {A}\subseteq \left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\cap {A}$
106 indir ${⊢}\left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\cap {A}=\left({K}\cap {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\cap {A}\right)$
107 inss1 ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\cap {A}\subseteq \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
108 unss2 ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\cap {A}\subseteq \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\to \left({K}\cap {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\cap {A}\right)\subseteq \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
109 107 108 ax-mp ${⊢}\left({K}\cap {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\cap {A}\right)\subseteq \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
110 106 109 eqsstri ${⊢}\left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\cap {A}\subseteq \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
111 105 110 sstrdi ${⊢}{\phi }\to {E}\cap {A}\subseteq \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
112 101 20 sstrd ${⊢}{\phi }\to \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ$
113 ovolss ${⊢}\left({E}\cap {A}\subseteq \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\wedge \left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ\right)\to {vol}^{*}\left({E}\cap {A}\right)\le {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
114 111 112 113 syl2anc ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)\le {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
115 28 46 sstrd ${⊢}{\phi }\to {K}\cap {A}\subseteq ℝ$
116 89 20 sstrd ${⊢}{\phi }\to \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ$
117 ovolun ${⊢}\left(\left({K}\cap {A}\subseteq ℝ\wedge {vol}^{*}\left({K}\cap {A}\right)\in ℝ\right)\wedge \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le {vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
118 115 49 116 97 117 syl22anc ${⊢}{\phi }\to {vol}^{*}\left(\left({K}\cap {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le {vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
119 23 103 98 114 118 letrd ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)\le {vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
120 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
121 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ {G}=\left(\mathrm{abs}\circ -\right)\circ {G}$
122 121 9 ovolsf ${⊢}{G}:ℕ⟶\le \cap {ℝ}^{2}\to {T}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
123 7 122 syl ${⊢}{\phi }\to {T}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
124 123 11 ffvelrnd ${⊢}{\phi }\to {T}\left({M}\right)\in \left[0,\mathrm{+\infty }\right)$
125 120 124 sseldi ${⊢}{\phi }\to {T}\left({M}\right)\in ℝ$
126 90 125 resubcld ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\in ℝ$
127 97 rexrd ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in {ℝ}^{*}$
128 id ${⊢}{z}\in ℕ\to {z}\in ℕ$
129 nnaddcl ${⊢}\left({z}\in ℕ\wedge {M}\in ℕ\right)\to {z}+{M}\in ℕ$
130 128 11 129 syl2anr ${⊢}\left({\phi }\wedge {z}\in ℕ\right)\to {z}+{M}\in ℕ$
131 7 ffvelrnda ${⊢}\left({\phi }\wedge {z}+{M}\in ℕ\right)\to {G}\left({z}+{M}\right)\in \left(\le \cap {ℝ}^{2}\right)$
132 130 131 syldan ${⊢}\left({\phi }\wedge {z}\in ℕ\right)\to {G}\left({z}+{M}\right)\in \left(\le \cap {ℝ}^{2}\right)$
133 132 fmpttd ${⊢}{\phi }\to \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
134 eqid ${⊢}\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)=\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
135 eqid ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)$
136 134 135 ovolsf ${⊢}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right):ℕ⟶\le \cap {ℝ}^{2}\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
137 133 136 syl ${⊢}{\phi }\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right):ℕ⟶\left[0,\mathrm{+\infty }\right)$
138 137 frnd ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\subseteq \left[0,\mathrm{+\infty }\right)$
139 icossxr ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq {ℝ}^{*}$
140 138 139 sstrdi ${⊢}{\phi }\to \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\subseteq {ℝ}^{*}$
141 supxrcl ${⊢}\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
142 140 141 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
143 126 rexrd ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\in {ℝ}^{*}$
144 1zzd ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to 1\in ℤ$
145 11 nnzd ${⊢}{\phi }\to {M}\in ℤ$
146 145 adantr ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {M}\in ℤ$
147 addcom ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}+1=1+{M}$
148 73 74 147 sylancl ${⊢}{\phi }\to {M}+1=1+{M}$
149 148 fveq2d ${⊢}{\phi }\to {ℤ}_{\ge \left({M}+1\right)}={ℤ}_{\ge \left(1+{M}\right)}$
150 149 eleq2d ${⊢}{\phi }\to \left({x}\in {ℤ}_{\ge \left({M}+1\right)}↔{x}\in {ℤ}_{\ge \left(1+{M}\right)}\right)$
151 150 biimpa ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in {ℤ}_{\ge \left(1+{M}\right)}$
152 eluzsub ${⊢}\left(1\in ℤ\wedge {M}\in ℤ\wedge {x}\in {ℤ}_{\ge \left(1+{M}\right)}\right)\to {x}-{M}\in {ℤ}_{\ge 1}$
153 144 146 151 152 syl3anc ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}-{M}\in {ℤ}_{\ge 1}$
154 153 67 eleqtrrdi ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}-{M}\in ℕ$
155 eluzelz ${⊢}{x}\in {ℤ}_{\ge \left({M}+1\right)}\to {x}\in ℤ$
156 155 adantl ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in ℤ$
157 156 zcnd ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in ℂ$
158 73 adantr ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {M}\in ℂ$
159 157 158 npcand ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}-{M}+{M}={x}$
160 159 eqcomd ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}={x}-{M}+{M}$
161 oveq1 ${⊢}{z}={x}-{M}\to {z}+{M}={x}-{M}+{M}$
162 161 rspceeqv ${⊢}\left({x}-{M}\in ℕ\wedge {x}={x}-{M}+{M}\right)\to \exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={z}+{M}$
163 154 160 162 syl2anc ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to \exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={z}+{M}$
164 eqid ${⊢}\left({z}\in ℕ⟼{z}+{M}\right)=\left({z}\in ℕ⟼{z}+{M}\right)$
165 164 elrnmpt ${⊢}{x}\in \mathrm{V}\to \left({x}\in \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)↔\exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={z}+{M}\right)$
166 165 elv ${⊢}{x}\in \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)↔\exists {z}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={z}+{M}$
167 163 166 sylibr ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)$
168 167 ex ${⊢}{\phi }\to \left({x}\in {ℤ}_{\ge \left({M}+1\right)}\to {x}\in \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\right)$
169 168 ssrdv ${⊢}{\phi }\to {ℤ}_{\ge \left({M}+1\right)}\subseteq \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)$
170 imass2 ${⊢}{ℤ}_{\ge \left({M}+1\right)}\subseteq \mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\to {G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {G}\left[\mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\right]$
171 169 170 syl ${⊢}{\phi }\to {G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {G}\left[\mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\right]$
172 rnco2 ${⊢}\mathrm{ran}\left({G}\circ \left({z}\in ℕ⟼{z}+{M}\right)\right)={G}\left[\mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\right]$
173 7 130 cofmpt ${⊢}{\phi }\to {G}\circ \left({z}\in ℕ⟼{z}+{M}\right)=\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
174 173 rneqd ${⊢}{\phi }\to \mathrm{ran}\left({G}\circ \left({z}\in ℕ⟼{z}+{M}\right)\right)=\mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
175 172 174 syl5eqr ${⊢}{\phi }\to {G}\left[\mathrm{ran}\left({z}\in ℕ⟼{z}+{M}\right)\right]=\mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
176 171 175 sseqtrd ${⊢}{\phi }\to {G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
177 imass2 ${⊢}{G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\to \left(.\right)\left[{G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right]\subseteq \left(.\right)\left[\mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right]$
178 176 177 syl ${⊢}{\phi }\to \left(.\right)\left[{G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right]\subseteq \left(.\right)\left[\mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right]$
179 imaco ${⊢}\left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left(.\right)\left[{G}\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right]$
180 rnco2 ${⊢}\mathrm{ran}\left(\left(.\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)=\left(.\right)\left[\mathrm{ran}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right]$
181 178 179 180 3sstr4g ${⊢}{\phi }\to \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \mathrm{ran}\left(\left(.\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)$
182 181 unissd ${⊢}{\phi }\to \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)$
183 135 ovollb ${⊢}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right):ℕ⟶\le \cap {ℝ}^{2}\wedge \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)$
184 133 182 183 syl2anc ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)$
185 123 frnd ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq \left[0,\mathrm{+\infty }\right)$
186 185 139 sstrdi ${⊢}{\phi }\to \mathrm{ran}{T}\subseteq {ℝ}^{*}$
187 9 fveq1i ${⊢}{T}\left({M}+{n}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({M}+{n}\right)$
188 11 nnred ${⊢}{\phi }\to {M}\in ℝ$
189 188 ltp1d ${⊢}{\phi }\to {M}<{M}+1$
190 fzdisj ${⊢}{M}<{M}+1\to \left(1\dots {M}\right)\cap \left({M}+1\dots {M}+{n}\right)=\varnothing$
191 189 190 syl ${⊢}{\phi }\to \left(1\dots {M}\right)\cap \left({M}+1\dots {M}+{n}\right)=\varnothing$
192 191 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {M}\right)\cap \left({M}+1\dots {M}+{n}\right)=\varnothing$
193 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
194 nn0addge1 ${⊢}\left({M}\in ℝ\wedge {n}\in {ℕ}_{0}\right)\to {M}\le {M}+{n}$
195 188 193 194 syl2an ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\le {M}+{n}$
196 11 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in ℕ$
197 196 67 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in {ℤ}_{\ge 1}$
198 nnaddcl ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}+{n}\in ℕ$
199 11 198 sylan ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+{n}\in ℕ$
200 199 nnzd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+{n}\in ℤ$
201 elfz5 ${⊢}\left({M}\in {ℤ}_{\ge 1}\wedge {M}+{n}\in ℤ\right)\to \left({M}\in \left(1\dots {M}+{n}\right)↔{M}\le {M}+{n}\right)$
202 197 200 201 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({M}\in \left(1\dots {M}+{n}\right)↔{M}\le {M}+{n}\right)$
203 195 202 mpbird ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in \left(1\dots {M}+{n}\right)$
204 fzsplit ${⊢}{M}\in \left(1\dots {M}+{n}\right)\to \left(1\dots {M}+{n}\right)=\left(1\dots {M}\right)\cup \left({M}+1\dots {M}+{n}\right)$
205 203 204 syl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {M}+{n}\right)=\left(1\dots {M}\right)\cup \left({M}+1\dots {M}+{n}\right)$
206 fzfid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(1\dots {M}+{n}\right)\in \mathrm{Fin}$
207 7 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
208 elfznn ${⊢}{j}\in \left(1\dots {M}+{n}\right)\to {j}\in ℕ$
209 ovolfcl ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {j}\in ℕ\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
210 207 208 209 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
211 210 simp2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ$
212 210 simp1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to {1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
213 211 212 resubcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
214 213 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℂ$
215 192 205 206 214 fsumsplit ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}=1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)=\sum _{{j}=1}^{{M}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)+\sum _{{j}={M}+1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)$
216 121 ovolfsval ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {j}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({j}\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
217 207 208 216 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}+{n}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({j}\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
218 199 67 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+{n}\in {ℤ}_{\ge 1}$
219 217 218 214 fsumser ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}=1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({M}+{n}\right)$
220 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
221 32 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {j}\in ℕ$
222 220 221 216 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\left({j}\right)={2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)$
223 7 32 209 syl2an ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
224 223 simp2d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ$
225 223 simp1d ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
226 224 225 resubcld ${⊢}\left({\phi }\wedge {j}\in \left(1\dots {M}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
227 226 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
228 227 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left(1\dots {M}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℂ$
229 222 197 228 fsumser ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}=1}^{{M}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({M}\right)$
230 9 fveq1i ${⊢}{T}\left({M}\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({M}\right)$
231 229 230 syl6eqr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}=1}^{{M}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)={T}\left({M}\right)$
232 196 nnzd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in ℤ$
233 232 peano2zd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+1\in ℤ$
234 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
235 196 peano2nnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+1\in ℕ$
236 elfzuz ${⊢}{j}\in \left({M}+1\dots {M}+{n}\right)\to {j}\in {ℤ}_{\ge \left({M}+1\right)}$
237 eluznn ${⊢}\left({M}+1\in ℕ\wedge {j}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {j}\in ℕ$
238 235 236 237 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {j}\in ℕ$
239 234 238 209 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to \left({1}^{st}\left({G}\left({j}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({j}\right)\right)\le {2}^{nd}\left({G}\left({j}\right)\right)\right)$
240 239 simp2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)\in ℝ$
241 239 simp1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
242 240 241 resubcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℝ$
243 242 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {j}\in \left({M}+1\dots {M}+{n}\right)\right)\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\in ℂ$
244 2fveq3 ${⊢}{j}={k}+{M}\to {2}^{nd}\left({G}\left({j}\right)\right)={2}^{nd}\left({G}\left({k}+{M}\right)\right)$
245 2fveq3 ${⊢}{j}={k}+{M}\to {1}^{st}\left({G}\left({j}\right)\right)={1}^{st}\left({G}\left({k}+{M}\right)\right)$
246 244 245 oveq12d ${⊢}{j}={k}+{M}\to {2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)={2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)$
247 232 233 200 243 246 fsumshftm ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}={M}+1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)=\sum _{{k}={M}+1-{M}}^{{M}+{n}-{M}}\left({2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\right)$
248 196 nncnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in ℂ$
249 pncan2 ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}+1-{M}=1$
250 248 74 249 sylancl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+1-{M}=1$
251 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
252 251 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℂ$
253 248 252 pncan2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}+{n}-{M}={n}$
254 250 253 oveq12d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({M}+1-{M}\dots {M}+{n}-{M}\right)=\left(1\dots {n}\right)$
255 254 sumeq1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{k}={M}+1-{M}}^{{M}+{n}-{M}}\left({2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\right)=\sum _{{k}=1}^{{n}}\left({2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\right)$
256 133 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right):ℕ⟶\le \cap {ℝ}^{2}$
257 elfznn ${⊢}{k}\in \left(1\dots {n}\right)\to {k}\in ℕ$
258 134 ovolfsval ${⊢}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right):ℕ⟶\le \cap {ℝ}^{2}\wedge {k}\in ℕ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\left({k}\right)={2}^{nd}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)-{1}^{st}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)$
259 256 257 258 syl2an ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\left({k}\right)={2}^{nd}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)-{1}^{st}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)$
260 257 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℕ$
261 fvoveq1 ${⊢}{z}={k}\to {G}\left({z}+{M}\right)={G}\left({k}+{M}\right)$
262 eqid ${⊢}\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)=\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)$
263 fvex ${⊢}{G}\left({k}+{M}\right)\in \mathrm{V}$
264 261 262 263 fvmpt ${⊢}{k}\in ℕ\to \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)={G}\left({k}+{M}\right)$
265 260 264 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)={G}\left({k}+{M}\right)$
266 265 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)={2}^{nd}\left({G}\left({k}+{M}\right)\right)$
267 265 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {1}^{st}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)={1}^{st}\left({G}\left({k}+{M}\right)\right)$
268 266 267 oveq12d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)-{1}^{st}\left(\left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\left({k}\right)\right)={2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)$
269 259 268 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\left({k}\right)={2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)$
270 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
271 270 67 eleqtrdi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in {ℤ}_{\ge 1}$
272 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {G}:ℕ⟶\le \cap {ℝ}^{2}$
273 nnaddcl ${⊢}\left({k}\in ℕ\wedge {M}\in ℕ\right)\to {k}+{M}\in ℕ$
274 257 196 273 syl2anr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}+{M}\in ℕ$
275 ovolfcl ${⊢}\left({G}:ℕ⟶\le \cap {ℝ}^{2}\wedge {k}+{M}\in ℕ\right)\to \left({1}^{st}\left({G}\left({k}+{M}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({k}+{M}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({k}+{M}\right)\right)\le {2}^{nd}\left({G}\left({k}+{M}\right)\right)\right)$
276 272 274 275 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to \left({1}^{st}\left({G}\left({k}+{M}\right)\right)\in ℝ\wedge {2}^{nd}\left({G}\left({k}+{M}\right)\right)\in ℝ\wedge {1}^{st}\left({G}\left({k}+{M}\right)\right)\le {2}^{nd}\left({G}\left({k}+{M}\right)\right)\right)$
277 276 simp2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left({G}\left({k}+{M}\right)\right)\in ℝ$
278 276 simp1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {1}^{st}\left({G}\left({k}+{M}\right)\right)\in ℝ$
279 277 278 resubcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\in ℝ$
280 279 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {k}\in \left(1\dots {n}\right)\right)\to {2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\in ℂ$
281 269 271 280 fsumser ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{k}=1}^{{n}}\left({2}^{nd}\left({G}\left({k}+{M}\right)\right)-{1}^{st}\left({G}\left({k}+{M}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)$
282 247 255 281 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}={M}+1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)$
283 231 282 oveq12d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \sum _{{j}=1}^{{M}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)+\sum _{{j}={M}+1}^{{M}+{n}}\left({2}^{nd}\left({G}\left({j}\right)\right)-{1}^{st}\left({G}\left({j}\right)\right)\right)={T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)$
284 215 219 283 3eqtr3d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ {G}\right)\right)\left({M}+{n}\right)={T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)$
285 187 284 syl5eq ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {T}\left({M}+{n}\right)={T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)$
286 123 ffnd ${⊢}{\phi }\to {T}Fnℕ$
287 fnfvelrn ${⊢}\left({T}Fnℕ\wedge {M}+{n}\in ℕ\right)\to {T}\left({M}+{n}\right)\in \mathrm{ran}{T}$
288 286 199 287 syl2an2r ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {T}\left({M}+{n}\right)\in \mathrm{ran}{T}$
289 285 288 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\in \mathrm{ran}{T}$
290 supxrub ${⊢}\left(\mathrm{ran}{T}\subseteq {ℝ}^{*}\wedge {T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\in \mathrm{ran}{T}\right)\to {T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
291 186 289 290 syl2an2r ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)$
292 125 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {T}\left({M}\right)\in ℝ$
293 137 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\in \left[0,\mathrm{+\infty }\right)$
294 120 293 sseldi ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\in ℝ$
295 90 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\in ℝ$
296 292 294 295 leaddsub2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({T}\left({M}\right)+seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)↔seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
297 291 296 mpbid ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)$
298 297 ralrimiva ${⊢}{\phi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)$
299 137 ffnd ${⊢}{\phi }\to seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)Fnℕ$
300 breq1 ${⊢}{x}=seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\to \left({x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)↔seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
301 300 ralrn ${⊢}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)Fnℕ\to \left(\forall {x}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
302 299 301 syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\left({n}\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
303 298 302 mpbird ${⊢}{\phi }\to \forall {x}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)$
304 supxrleub ${⊢}\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\subseteq {ℝ}^{*}\wedge sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)↔\forall {x}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
305 140 143 304 syl2anc ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)↔\forall {x}\in \mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{x}\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)\right)$
306 303 305 mpbird ${⊢}{\phi }\to sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ \left({z}\in ℕ⟼{G}\left({z}+{M}\right)\right)\right)\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)$
307 127 142 143 184 306 xrletrd ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)$
308 125 90 50 absdifltd ${⊢}{\phi }\to \left(\left|{T}\left({M}\right)-sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)\right|<{C}↔\left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{C}<{T}\left({M}\right)\wedge {T}\left({M}\right)
309 12 308 mpbid ${⊢}{\phi }\to \left(sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{C}<{T}\left({M}\right)\wedge {T}\left({M}\right)
310 309 simpld ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{C}<{T}\left({M}\right)$
311 90 50 125 310 ltsub23d ${⊢}{\phi }\to sup\left(\mathrm{ran}{T},{ℝ}^{*},<\right)-{T}\left({M}\right)<{C}$
312 97 126 50 307 311 lelttrd ${⊢}{\phi }\to {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)<{C}$
313 97 50 49 312 ltadd2dd ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)<{vol}^{*}\left({K}\cap {A}\right)+{C}$
314 23 98 51 119 313 lelttrd ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)<{vol}^{*}\left({K}\cap {A}\right)+{C}$
315 54 97 readdcld ${⊢}{\phi }\to {vol}^{*}\left({K}\setminus {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
316 difss ${⊢}{K}\setminus {A}\subseteq {K}$
317 unss1 ${⊢}{K}\setminus {A}\subseteq {K}\to \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
318 316 317 ax-mp ${⊢}\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq {K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
319 318 88 sseqtrrid ${⊢}{\phi }\to \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)$
320 ovolsscl ${⊢}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\wedge \bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \mathrm{ran}\left(\left(.\right)\circ {G}\right)\right)\in ℝ\right)\to {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
321 319 20 95 320 syl3anc ${⊢}{\phi }\to {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ$
322 104 ssdifd ${⊢}{\phi }\to {E}\setminus {A}\subseteq \left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\setminus {A}$
323 difundir ${⊢}\left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\setminus {A}=\left({K}\setminus {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\setminus {A}\right)$
324 difss ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\setminus {A}\subseteq \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
325 unss2 ${⊢}\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\setminus {A}\subseteq \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\to \left({K}\setminus {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\setminus {A}\right)\subseteq \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
326 324 325 ax-mp ${⊢}\left({K}\setminus {A}\right)\cup \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\setminus {A}\right)\subseteq \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
327 323 326 eqsstri ${⊢}\left({K}\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\setminus {A}\subseteq \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
328 322 327 sstrdi ${⊢}{\phi }\to {E}\setminus {A}\subseteq \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]$
329 319 20 sstrd ${⊢}{\phi }\to \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ$
330 ovolss ${⊢}\left({E}\setminus {A}\subseteq \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\wedge \left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ\right)\to {vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
331 328 329 330 syl2anc ${⊢}{\phi }\to {vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
332 52 46 sstrd ${⊢}{\phi }\to {K}\setminus {A}\subseteq ℝ$
333 ovolun ${⊢}\left(\left({K}\setminus {A}\subseteq ℝ\wedge {vol}^{*}\left({K}\setminus {A}\right)\in ℝ\right)\wedge \left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\subseteq ℝ\wedge {vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le {vol}^{*}\left({K}\setminus {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
334 332 54 116 97 333 syl22anc ${⊢}{\phi }\to {vol}^{*}\left(\left({K}\setminus {A}\right)\cup \bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)\le {vol}^{*}\left({K}\setminus {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
335 26 321 315 331 334 letrd ${⊢}{\phi }\to {vol}^{*}\left({E}\setminus {A}\right)\le {vol}^{*}\left({K}\setminus {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)$
336 97 50 54 312 ltadd2dd ${⊢}{\phi }\to {vol}^{*}\left({K}\setminus {A}\right)+{vol}^{*}\left(\bigcup \left(\left(.\right)\circ {G}\right)\left[{ℤ}_{\ge \left({M}+1\right)}\right]\right)<{vol}^{*}\left({K}\setminus {A}\right)+{C}$
337 26 315 55 335 336 lelttrd ${⊢}{\phi }\to {vol}^{*}\left({E}\setminus {A}\right)<{vol}^{*}\left({K}\setminus {A}\right)+{C}$
338 23 26 51 55 314 337 lt2addd ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)<{vol}^{*}\left({K}\cap {A}\right)+{C}+{vol}^{*}\left({K}\setminus {A}\right)+{C}$
339 49 recnd ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)\in ℂ$
340 50 recnd ${⊢}{\phi }\to {C}\in ℂ$
341 54 recnd ${⊢}{\phi }\to {vol}^{*}\left({K}\setminus {A}\right)\in ℂ$
342 339 340 341 340 add4d ${⊢}{\phi }\to {vol}^{*}\left({K}\cap {A}\right)+{C}+{vol}^{*}\left({K}\setminus {A}\right)+{C}={vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left({K}\setminus {A}\right)+{C}+{C}$
343 338 342 breqtrd ${⊢}{\phi }\to {vol}^{*}\left({E}\cap {A}\right)+{vol}^{*}\left({E}\setminus {A}\right)<{vol}^{*}\left({K}\cap {A}\right)+{vol}^{*}\left({K}\setminus {A}\right)+{C}+{C}$