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 
|- ( ( U C_ II /\ ( 0 [,] 1 ) = U. U ) -> E. n e. NN A. k e. ( 1 ... n ) E. u e. U ( ( ( k - 1 ) / n ) [,] ( k / n ) ) C_ u )

Proof

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