Metamath Proof Explorer

Theorem rrntotbnd

Description: A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses rrntotbnd.1 
|- X = ( RR ^m I )
rrntotbnd.2 
|- M = ( ( Rn ` I ) |` ( Y X. Y ) )
Assertion rrntotbnd 
|- ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) )

Proof

Step Hyp Ref Expression
1 rrntotbnd.1 
 |-  X = ( RR ^m I )
2 rrntotbnd.2 
 |-  M = ( ( Rn ` I ) |` ( Y X. Y ) )
3 eqid 
 |-  ( ( CCfld |`s RR ) ^s I ) = ( ( CCfld |`s RR ) ^s I )
4 eqid 
 |-  ( dist ` ( ( CCfld |`s RR ) ^s I ) ) = ( dist ` ( ( CCfld |`s RR ) ^s I ) )
5 3 4 1 repwsmet 
 |-  ( I e. Fin -> ( dist ` ( ( CCfld |`s RR ) ^s I ) ) e. ( Met ` X ) )
6 1 rrnmet 
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
7 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
8 nn0re 
 |-  ( ( # ` I ) e. NN0 -> ( # ` I ) e. RR )
9 nn0ge0 
 |-  ( ( # ` I ) e. NN0 -> 0 <_ ( # ` I ) )
10 8 9 resqrtcld 
 |-  ( ( # ` I ) e. NN0 -> ( sqrt ` ( # ` I ) ) e. RR )
11 7 10 syl 
 |-  ( I e. Fin -> ( sqrt ` ( # ` I ) ) e. RR )
12 8 9 sqrtge0d 
 |-  ( ( # ` I ) e. NN0 -> 0 <_ ( sqrt ` ( # ` I ) ) )
13 7 12 syl 
 |-  ( I e. Fin -> 0 <_ ( sqrt ` ( # ` I ) ) )
14 11 13 ge0p1rpd 
 |-  ( I e. Fin -> ( ( sqrt ` ( # ` I ) ) + 1 ) e. RR+ )
15 1rp 
 |-  1 e. RR+
16 15 a1i 
 |-  ( I e. Fin -> 1 e. RR+ )
17 metcl 
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x ( Rn ` I ) y ) e. RR )
18 17 3expb 
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) e. RR )
19 6 18 sylan 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) e. RR )
20 11 adantr 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` ( # ` I ) ) e. RR )
21 5 adantr 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( dist ` ( ( CCfld |`s RR ) ^s I ) ) e. ( Met ` X ) )
22 simprl 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> x e. X )
23 simprr 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> y e. X )
24 metcl 
 |-  ( ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) e. RR )
25 metge0 
 |-  ( ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) e. ( Met ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) )
26 24 25 jca 
 |-  ( ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) e. ( Met ` X ) /\ x e. X /\ y e. X ) -> ( ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) e. RR /\ 0 <_ ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
27 21 22 23 26 syl3anc 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) e. RR /\ 0 <_ ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
28 27 simpld 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) e. RR )
29 20 28 remulcld 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` ( # ` I ) ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) e. RR )
30 peano2re 
 |-  ( ( sqrt ` ( # ` I ) ) e. RR -> ( ( sqrt ` ( # ` I ) ) + 1 ) e. RR )
31 11 30 syl 
 |-  ( I e. Fin -> ( ( sqrt ` ( # ` I ) ) + 1 ) e. RR )
32 31 adantr 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` ( # ` I ) ) + 1 ) e. RR )
33 32 28 remulcld 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( ( sqrt ` ( # ` I ) ) + 1 ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) e. RR )
34 id 
 |-  ( I e. Fin -> I e. Fin )
35 3 4 1 34 rrnequiv 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) <_ ( x ( Rn ` I ) y ) /\ ( x ( Rn ` I ) y ) <_ ( ( sqrt ` ( # ` I ) ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) ) )
36 35 simprd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) <_ ( ( sqrt ` ( # ` I ) ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
37 20 lep1d 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( sqrt ` ( # ` I ) ) <_ ( ( sqrt ` ( # ` I ) ) + 1 ) )
38 lemul1a 
 |-  ( ( ( ( sqrt ` ( # ` I ) ) e. RR /\ ( ( sqrt ` ( # ` I ) ) + 1 ) e. RR /\ ( ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) e. RR /\ 0 <_ ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) ) /\ ( sqrt ` ( # ` I ) ) <_ ( ( sqrt ` ( # ` I ) ) + 1 ) ) -> ( ( sqrt ` ( # ` I ) ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) <_ ( ( ( sqrt ` ( # ` I ) ) + 1 ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
39 20 32 27 37 38 syl31anc 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( ( sqrt ` ( # ` I ) ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) <_ ( ( ( sqrt ` ( # ` I ) ) + 1 ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
40 19 29 33 36 39 letrd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) <_ ( ( ( sqrt ` ( # ` I ) ) + 1 ) x. ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) ) )
41 35 simpld 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) <_ ( x ( Rn ` I ) y ) )
42 19 recnd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( Rn ` I ) y ) e. CC )
43 42 mulid2d 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( 1 x. ( x ( Rn ` I ) y ) ) = ( x ( Rn ` I ) y ) )
44 41 43 breqtrrd 
 |-  ( ( I e. Fin /\ ( x e. X /\ y e. X ) ) -> ( x ( dist ` ( ( CCfld |`s RR ) ^s I ) ) y ) <_ ( 1 x. ( x ( Rn ` I ) y ) ) )
45 eqid 
 |-  ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) ) = ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) )
46 ax-resscn 
 |-  RR C_ CC
47 3 45 cnpwstotbnd 
 |-  ( ( RR C_ CC /\ I e. Fin ) -> ( ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) ) e. ( TotBnd ` Y ) <-> ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) ) e. ( Bnd ` Y ) ) )
48 46 47 mpan 
 |-  ( I e. Fin -> ( ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) ) e. ( TotBnd ` Y ) <-> ( ( dist ` ( ( CCfld |`s RR ) ^s I ) ) |` ( Y X. Y ) ) e. ( Bnd ` Y ) ) )
49 5 6 14 16 40 44 45 2 48 equivbnd2 
 |-  ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) )