lebnumii

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

		Ref	Expression
	Assertion	lebnumii	$⊢ (U \subseteq II \land [0, 1] = ⋃ U) \to \exists n \in ℕ \forall k \in (1 \dots n) \exists u \in U [\frac{k - 1}{n}, \frac{k}{n}] \subseteq u$

Proof

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

Metamath Proof Explorer

Theorem lebnumii

Proof