# Metamath Proof Explorer

## Theorem lebnumii

Description: Specialize the Lebesgue number lemma lebnum to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Assertion lebnumii ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}$

### Proof

Step Hyp Ref Expression
1 df-ii ${⊢}\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$
2 cnmet ${⊢}\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$
3 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
4 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 3 4 sstri ${⊢}\left[0,1\right]\subseteq ℂ$
6 metres2 ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\wedge \left[0,1\right]\subseteq ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{Met}\left(\left[0,1\right]\right)$
7 2 5 6 mp2an ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{Met}\left(\left[0,1\right]\right)$
8 7 a1i ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{Met}\left(\left[0,1\right]\right)$
9 iicmp ${⊢}\mathrm{II}\in \mathrm{Comp}$
10 9 a1i ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \mathrm{II}\in \mathrm{Comp}$
11 simpl ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to {U}\subseteq \mathrm{II}$
12 simpr ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \left[0,1\right]=\bigcup {U}$
13 1 8 10 11 12 lebnum ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}$
14 rpreccl ${⊢}{r}\in {ℝ}^{+}\to \frac{1}{{r}}\in {ℝ}^{+}$
15 14 adantl ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to \frac{1}{{r}}\in {ℝ}^{+}$
16 15 rpred ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to \frac{1}{{r}}\in ℝ$
17 15 rpge0d ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to 0\le \frac{1}{{r}}$
18 flge0nn0 ${⊢}\left(\frac{1}{{r}}\in ℝ\wedge 0\le \frac{1}{{r}}\right)\to ⌊\frac{1}{{r}}⌋\in {ℕ}_{0}$
19 16 17 18 syl2anc ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to ⌊\frac{1}{{r}}⌋\in {ℕ}_{0}$
20 nn0p1nn ${⊢}⌊\frac{1}{{r}}⌋\in {ℕ}_{0}\to ⌊\frac{1}{{r}}⌋+1\in ℕ$
21 19 20 syl ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to ⌊\frac{1}{{r}}⌋+1\in ℕ$
22 elfznn ${⊢}{k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\to {k}\in ℕ$
23 22 adantl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\in ℕ$
24 23 nnrpd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\in {ℝ}^{+}$
25 21 adantr ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to ⌊\frac{1}{{r}}⌋+1\in ℕ$
26 25 nnrpd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to ⌊\frac{1}{{r}}⌋+1\in {ℝ}^{+}$
27 24 26 rpdivcld ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in {ℝ}^{+}$
28 27 rpred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in ℝ$
29 27 rpge0d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0\le \frac{{k}}{⌊\frac{1}{{r}}⌋+1}$
30 elfzle2 ${⊢}{k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\to {k}\le ⌊\frac{1}{{r}}⌋+1$
31 30 adantl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\le ⌊\frac{1}{{r}}⌋+1$
32 25 nnred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to ⌊\frac{1}{{r}}⌋+1\in ℝ$
33 32 recnd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to ⌊\frac{1}{{r}}⌋+1\in ℂ$
34 33 mulid1d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(⌊\frac{1}{{r}}⌋+1\right)\cdot 1=⌊\frac{1}{{r}}⌋+1$
35 31 34 breqtrrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\le \left(⌊\frac{1}{{r}}⌋+1\right)\cdot 1$
36 23 nnred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\in ℝ$
37 1red ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 1\in ℝ$
38 25 nngt0d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0<⌊\frac{1}{{r}}⌋+1$
39 ledivmul ${⊢}\left({k}\in ℝ\wedge 1\in ℝ\wedge \left(⌊\frac{1}{{r}}⌋+1\in ℝ\wedge 0<⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\le 1↔{k}\le \left(⌊\frac{1}{{r}}⌋+1\right)\cdot 1\right)$
40 36 37 32 38 39 syl112anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\le 1↔{k}\le \left(⌊\frac{1}{{r}}⌋+1\right)\cdot 1\right)$
41 35 40 mpbird ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\le 1$
42 elicc01 ${⊢}\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in \left[0,1\right]↔\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in ℝ\wedge 0\le \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\wedge \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\le 1\right)$
43 28 29 41 42 syl3anbrc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in \left[0,1\right]$
44 oveq1 ${⊢}{x}=\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\to {x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}=\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}$
45 44 sseq1d ${⊢}{x}=\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\to \left({x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}↔\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\right)$
46 45 rexbidv ${⊢}{x}=\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}↔\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\right)$
47 46 rspcv ${⊢}\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in \left[0,1\right]\to \left(\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\right)$
48 43 47 syl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\right)$
49 simplr ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {r}\in {ℝ}^{+}$
50 49 rpred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {r}\in ℝ$
51 28 50 resubcld ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r}\in ℝ$
52 51 rexrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r}\in {ℝ}^{*}$
53 28 50 readdcld ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\in ℝ$
54 53 rexrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\in {ℝ}^{*}$
55 nnm1nn0 ${⊢}{k}\in ℕ\to {k}-1\in {ℕ}_{0}$
56 23 55 syl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}-1\in {ℕ}_{0}$
57 56 nn0red ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}-1\in ℝ$
58 57 25 nndivred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\in ℝ$
59 36 recnd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}\in ℂ$
60 57 recnd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}-1\in ℂ$
61 25 nnne0d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to ⌊\frac{1}{{r}}⌋+1\ne 0$
62 59 60 33 61 divsubdird ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}-\left({k}-1\right)}{⌊\frac{1}{{r}}⌋+1}=\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-\left(\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\right)$
63 ax-1cn ${⊢}1\in ℂ$
64 nncan ${⊢}\left({k}\in ℂ\wedge 1\in ℂ\right)\to {k}-\left({k}-1\right)=1$
65 59 63 64 sylancl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {k}-\left({k}-1\right)=1$
66 65 oveq1d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}-\left({k}-1\right)}{⌊\frac{1}{{r}}⌋+1}=\frac{1}{⌊\frac{1}{{r}}⌋+1}$
67 62 66 eqtr3d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-\left(\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\right)=\frac{1}{⌊\frac{1}{{r}}⌋+1}$
68 49 rprecred ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{1}{{r}}\in ℝ$
69 flltp1 ${⊢}\frac{1}{{r}}\in ℝ\to \frac{1}{{r}}<⌊\frac{1}{{r}}⌋+1$
70 68 69 syl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{1}{{r}}<⌊\frac{1}{{r}}⌋+1$
71 rpgt0 ${⊢}{r}\in {ℝ}^{+}\to 0<{r}$
72 71 ad2antlr ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0<{r}$
73 ltdiv23 ${⊢}\left(1\in ℝ\wedge \left({r}\in ℝ\wedge 0<{r}\right)\wedge \left(⌊\frac{1}{{r}}⌋+1\in ℝ\wedge 0<⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{1}{{r}}<⌊\frac{1}{{r}}⌋+1↔\frac{1}{⌊\frac{1}{{r}}⌋+1}<{r}\right)$
74 37 50 72 32 38 73 syl122anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{1}{{r}}<⌊\frac{1}{{r}}⌋+1↔\frac{1}{⌊\frac{1}{{r}}⌋+1}<{r}\right)$
75 70 74 mpbid ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{1}{⌊\frac{1}{{r}}⌋+1}<{r}$
76 67 75 eqbrtrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-\left(\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\right)<{r}$
77 28 58 50 76 ltsub23d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r}<\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}$
78 28 49 ltaddrpd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}<\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}$
79 iccssioo ${⊢}\left(\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r}\in {ℝ}^{*}\wedge \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\in {ℝ}^{*}\right)\wedge \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r}<\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\wedge \frac{{k}}{⌊\frac{1}{{r}}⌋+1}<\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)$
80 52 54 77 78 79 syl22anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)$
81 0red ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0\in ℝ$
82 56 nn0ge0d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0\le {k}-1$
83 divge0 ${⊢}\left(\left({k}-1\in ℝ\wedge 0\le {k}-1\right)\wedge \left(⌊\frac{1}{{r}}⌋+1\in ℝ\wedge 0<⌊\frac{1}{{r}}⌋+1\right)\right)\to 0\le \frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}$
84 57 82 32 38 83 syl22anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to 0\le \frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}$
85 iccss ${⊢}\left(\left(0\in ℝ\wedge 1\in ℝ\right)\wedge \left(0\le \frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}\wedge \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\le 1\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left[0,1\right]$
86 81 37 84 41 85 syl22anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left[0,1\right]$
87 80 86 ssind ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)\cap \left[0,1\right]$
88 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
89 88 rexmet ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)$
90 sseqin2 ${⊢}\left[0,1\right]\subseteq ℝ↔ℝ\cap \left[0,1\right]=\left[0,1\right]$
91 3 90 mpbi ${⊢}ℝ\cap \left[0,1\right]=\left[0,1\right]$
92 43 91 eleqtrrdi ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in \left(ℝ\cap \left[0,1\right]\right)$
93 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
94 93 ad2antlr ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to {r}\in {ℝ}^{*}$
95 xpss12 ${⊢}\left(\left[0,1\right]\subseteq ℝ\wedge \left[0,1\right]\subseteq ℝ\right)\to \left[0,1\right]×\left[0,1\right]\subseteq {ℝ}^{2}$
96 3 3 95 mp2an ${⊢}\left[0,1\right]×\left[0,1\right]\subseteq {ℝ}^{2}$
97 resabs1 ${⊢}\left[0,1\right]×\left[0,1\right]\subseteq {ℝ}^{2}\to {\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}$
98 96 97 ax-mp ${⊢}{\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}$
99 98 eqcomi ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}={\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}$
100 99 blres ${⊢}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\in \mathrm{\infty Met}\left(ℝ\right)\wedge \frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in \left(ℝ\cap \left[0,1\right]\right)\wedge {r}\in {ℝ}^{*}\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){r}\right)\cap \left[0,1\right]$
101 89 92 94 100 mp3an2i ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){r}\right)\cap \left[0,1\right]$
102 88 bl2ioo ${⊢}\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\in ℝ\wedge {r}\in ℝ\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){r}=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)$
103 28 50 102 syl2anc ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){r}=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)$
104 103 ineq1d ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right){r}\right)\cap \left[0,1\right]=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)\cap \left[0,1\right]$
105 101 104 eqtrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}=\left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)-{r},\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)+{r}\right)\cap \left[0,1\right]$
106 87 105 sseqtrrd ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}$
107 sstr2 ${⊢}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq \left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\to \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
108 106 107 syl ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
109 108 reximdv ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left(\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right)\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
110 48 109 syld ${⊢}\left(\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\wedge {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\right)\to \left(\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
111 110 ralrimdva ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \forall {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
112 oveq2 ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \left(1\dots {n}\right)=\left(1\dots ⌊\frac{1}{{r}}⌋+1\right)$
113 oveq2 ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \frac{{k}-1}{{n}}=\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1}$
114 oveq2 ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \frac{{k}}{{n}}=\frac{{k}}{⌊\frac{1}{{r}}⌋+1}$
115 113 114 oveq12d ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]=\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]$
116 115 sseq1d ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \left(\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}↔\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
117 116 rexbidv ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \left(\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}↔\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
118 112 117 raleqbidv ${⊢}{n}=⌊\frac{1}{{r}}⌋+1\to \left(\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}↔\forall {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)$
119 118 rspcev ${⊢}\left(⌊\frac{1}{{r}}⌋+1\in ℕ\wedge \forall {k}\in \left(1\dots ⌊\frac{1}{{r}}⌋+1\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{⌊\frac{1}{{r}}⌋+1},\frac{{k}}{⌊\frac{1}{{r}}⌋+1}\right]\subseteq {u}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}$
120 21 111 119 syl6an ${⊢}\left(\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}\right)$
121 120 rexlimdva ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {x}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}{x}\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right){r}\subseteq {u}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}\right)$
122 13 121 mpd ${⊢}\left({U}\subseteq \mathrm{II}\wedge \left[0,1\right]=\bigcup {U}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}\exists {u}\in {U}\phantom{\rule{.4em}{0ex}}\left[\frac{{k}-1}{{n}},\frac{{k}}{{n}}\right]\subseteq {u}$