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 ( ( 𝑈 ⊆ II ∧ ( 0 [,] 1 ) = ∪ 𝑈 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑢 ∈ 𝑈 ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑢 )

Proof

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