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 ) / 𝑛 ) [,] ( π‘˜ / 𝑛 ) ) βŠ† 𝑒 )