Metamath Proof Explorer

Theorem rrndistlt

Description: Given two points in the space of n-dimensional real numbers, if every component is closer than E then the distance between the two points is less then ( ( sqrtn ) x. E ) . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses rrndistlt.i 
|- ( ph -> I e. Fin )
rrndistlt.z 
|- ( ph -> I =/= (/) )
rrndistlt.n 
|- N = ( # ` I )
rrndistlt.x 
|- ( ph -> X e. ( RR ^m I ) )
rrndistlt.y 
|- ( ph -> Y e. ( RR ^m I ) )
rrndistlt.l 
|- ( ( ph /\ i e. I ) -> ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) < E )
rrndistlt.e 
|- ( ph -> E e. RR+ )
rrndistlt.d 
|- D = ( dist ` ( RR^ ` I ) )
Assertion rrndistlt 
|- ( ph -> ( X D Y ) < ( ( sqrt ` N ) x. E ) )

Proof

Step Hyp Ref Expression
1 rrndistlt.i 
 |-  ( ph -> I e. Fin )
2 rrndistlt.z 
 |-  ( ph -> I =/= (/) )
3 rrndistlt.n 
 |-  N = ( # ` I )
4 rrndistlt.x 
 |-  ( ph -> X e. ( RR ^m I ) )
5 rrndistlt.y 
 |-  ( ph -> Y e. ( RR ^m I ) )
6 rrndistlt.l 
 |-  ( ( ph /\ i e. I ) -> ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) < E )
7 rrndistlt.e 
 |-  ( ph -> E e. RR+ )
8 rrndistlt.d 
 |-  D = ( dist ` ( RR^ ` I ) )
9 elmapi 
 |-  ( X e. ( RR ^m I ) -> X : I --> RR )
10 4 9 syl 
 |-  ( ph -> X : I --> RR )
11 ax-resscn 
 |-  RR C_ CC
12 11 a1i 
 |-  ( ph -> RR C_ CC )
13 10 12 fssd 
 |-  ( ph -> X : I --> CC )
14 13 ffvelrnda 
 |-  ( ( ph /\ i e. I ) -> ( X ` i ) e. CC )
15 elmapi 
 |-  ( Y e. ( RR ^m I ) -> Y : I --> RR )
16 5 15 syl 
 |-  ( ph -> Y : I --> RR )
17 16 12 fssd 
 |-  ( ph -> Y : I --> CC )
18 17 ffvelrnda 
 |-  ( ( ph /\ i e. I ) -> ( Y ` i ) e. CC )
19 14 18 subcld 
 |-  ( ( ph /\ i e. I ) -> ( ( X ` i ) - ( Y ` i ) ) e. CC )
20 19 abscld 
 |-  ( ( ph /\ i e. I ) -> ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) e. RR )
21 20 resqcld 
 |-  ( ( ph /\ i e. I ) -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) e. RR )
22 7 rpred 
 |-  ( ph -> E e. RR )
23 22 resqcld 
 |-  ( ph -> ( E ^ 2 ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ i e. I ) -> ( E ^ 2 ) e. RR )
25 19 absge0d 
 |-  ( ( ph /\ i e. I ) -> 0 <_ ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) )
26 22 adantr 
 |-  ( ( ph /\ i e. I ) -> E e. RR )
27 7 adantr 
 |-  ( ( ph /\ i e. I ) -> E e. RR+ )
28 27 rpge0d 
 |-  ( ( ph /\ i e. I ) -> 0 <_ E )
29 lt2sq 
 |-  ( ( ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) e. RR /\ 0 <_ ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ) /\ ( E e. RR /\ 0 <_ E ) ) -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) < E <-> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) < ( E ^ 2 ) ) )
30 20 25 26 28 29 syl22anc 
 |-  ( ( ph /\ i e. I ) -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) < E <-> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) < ( E ^ 2 ) ) )
31 6 30 mpbid 
 |-  ( ( ph /\ i e. I ) -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) < ( E ^ 2 ) )
32 1 2 21 24 31 fsumlt 
 |-  ( ph -> sum_ i e. I ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) < sum_ i e. I ( E ^ 2 ) )
33 10 ffvelrnda 
 |-  ( ( ph /\ i e. I ) -> ( X ` i ) e. RR )
34 16 ffvelrnda 
 |-  ( ( ph /\ i e. I ) -> ( Y ` i ) e. RR )
35 33 34 resubcld 
 |-  ( ( ph /\ i e. I ) -> ( ( X ` i ) - ( Y ` i ) ) e. RR )
36 absresq 
 |-  ( ( ( X ` i ) - ( Y ` i ) ) e. RR -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) = ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
37 35 36 syl 
 |-  ( ( ph /\ i e. I ) -> ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) = ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
38 37 eqcomd 
 |-  ( ( ph /\ i e. I ) -> ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) = ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) )
39 38 sumeq2dv 
 |-  ( ph -> sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) = sum_ i e. I ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) )
40 11 23 sseldi 
 |-  ( ph -> ( E ^ 2 ) e. CC )
41 fsumconst 
 |-  ( ( I e. Fin /\ ( E ^ 2 ) e. CC ) -> sum_ i e. I ( E ^ 2 ) = ( ( # ` I ) x. ( E ^ 2 ) ) )
42 1 40 41 syl2anc 
 |-  ( ph -> sum_ i e. I ( E ^ 2 ) = ( ( # ` I ) x. ( E ^ 2 ) ) )
43 eqcom 
 |-  ( N = ( # ` I ) <-> ( # ` I ) = N )
44 3 43 mpbi 
 |-  ( # ` I ) = N
45 44 oveq1i 
 |-  ( ( # ` I ) x. ( E ^ 2 ) ) = ( N x. ( E ^ 2 ) )
46 45 a1i 
 |-  ( ph -> ( ( # ` I ) x. ( E ^ 2 ) ) = ( N x. ( E ^ 2 ) ) )
47 42 46 eqtr2d 
 |-  ( ph -> ( N x. ( E ^ 2 ) ) = sum_ i e. I ( E ^ 2 ) )
48 39 47 breq12d 
 |-  ( ph -> ( sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) < ( N x. ( E ^ 2 ) ) <-> sum_ i e. I ( ( abs ` ( ( X ` i ) - ( Y ` i ) ) ) ^ 2 ) < sum_ i e. I ( E ^ 2 ) ) )
49 32 48 mpbird 
 |-  ( ph -> sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) < ( N x. ( E ^ 2 ) ) )
50 nfv 
 |-  F/ i ph
51 35 resqcld 
 |-  ( ( ph /\ i e. I ) -> ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) e. RR )
52 50 1 51 fsumreclf 
 |-  ( ph -> sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) e. RR )
53 35 sqge0d 
 |-  ( ( ph /\ i e. I ) -> 0 <_ ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
54 1 51 53 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
55 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
56 1 55 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
57 3 56 eqeltrid 
 |-  ( ph -> N e. NN0 )
58 57 nn0red 
 |-  ( ph -> N e. RR )
59 58 23 remulcld 
 |-  ( ph -> ( N x. ( E ^ 2 ) ) e. RR )
60 57 nn0ge0d 
 |-  ( ph -> 0 <_ N )
61 22 sqge0d 
 |-  ( ph -> 0 <_ ( E ^ 2 ) )
62 58 23 60 61 mulge0d 
 |-  ( ph -> 0 <_ ( N x. ( E ^ 2 ) ) )
63 52 54 59 62 sqrtltd 
 |-  ( ph -> ( sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) < ( N x. ( E ^ 2 ) ) <-> ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) < ( sqrt ` ( N x. ( E ^ 2 ) ) ) ) )
64 49 63 mpbid 
 |-  ( ph -> ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) < ( sqrt ` ( N x. ( E ^ 2 ) ) ) )
65 8 a1i 
 |-  ( ph -> D = ( dist ` ( RR^ ` I ) ) )
66 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
67 eqid 
 |-  ( RR ^m I ) = ( RR ^m I )
68 66 67 rrxdsfi 
 |-  ( I e. Fin -> ( dist ` ( RR^ ` I ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) ) ) )
69 1 68 syl 
 |-  ( ph -> ( dist ` ( RR^ ` I ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) ) ) )
70 65 69 eqtrd 
 |-  ( ph -> D = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) ) ) )
71 fveq1 
 |-  ( f = X -> ( f ` i ) = ( X ` i ) )
72 71 adantr 
 |-  ( ( f = X /\ g = Y ) -> ( f ` i ) = ( X ` i ) )
73 fveq1 
 |-  ( g = Y -> ( g ` i ) = ( Y ` i ) )
74 73 adantl 
 |-  ( ( f = X /\ g = Y ) -> ( g ` i ) = ( Y ` i ) )
75 72 74 oveq12d 
 |-  ( ( f = X /\ g = Y ) -> ( ( f ` i ) - ( g ` i ) ) = ( ( X ` i ) - ( Y ` i ) ) )
76 75 oveq1d 
 |-  ( ( f = X /\ g = Y ) -> ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) = ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
77 76 sumeq2sdv 
 |-  ( ( f = X /\ g = Y ) -> sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) = sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) )
78 77 fveq2d 
 |-  ( ( f = X /\ g = Y ) -> ( sqrt ` sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) ) = ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) )
79 78 adantl 
 |-  ( ( ph /\ ( f = X /\ g = Y ) ) -> ( sqrt ` sum_ i e. I ( ( ( f ` i ) - ( g ` i ) ) ^ 2 ) ) = ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) )
80 52 54 resqrtcld 
 |-  ( ph -> ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) e. RR )
81 70 79 4 5 80 ovmpod 
 |-  ( ph -> ( X D Y ) = ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) )
82 sqrtmul 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ ( ( E ^ 2 ) e. RR /\ 0 <_ ( E ^ 2 ) ) ) -> ( sqrt ` ( N x. ( E ^ 2 ) ) ) = ( ( sqrt ` N ) x. ( sqrt ` ( E ^ 2 ) ) ) )
83 58 60 23 61 82 syl22anc 
 |-  ( ph -> ( sqrt ` ( N x. ( E ^ 2 ) ) ) = ( ( sqrt ` N ) x. ( sqrt ` ( E ^ 2 ) ) ) )
84 7 rpge0d 
 |-  ( ph -> 0 <_ E )
85 22 84 sqrtsqd 
 |-  ( ph -> ( sqrt ` ( E ^ 2 ) ) = E )
86 85 oveq2d 
 |-  ( ph -> ( ( sqrt ` N ) x. ( sqrt ` ( E ^ 2 ) ) ) = ( ( sqrt ` N ) x. E ) )
87 83 86 eqtr2d 
 |-  ( ph -> ( ( sqrt ` N ) x. E ) = ( sqrt ` ( N x. ( E ^ 2 ) ) ) )
88 81 87 breq12d 
 |-  ( ph -> ( ( X D Y ) < ( ( sqrt ` N ) x. E ) <-> ( sqrt ` sum_ i e. I ( ( ( X ` i ) - ( Y ` i ) ) ^ 2 ) ) < ( sqrt ` ( N x. ( E ^ 2 ) ) ) ) )
89 64 88 mpbird 
 |-  ( ph -> ( X D Y ) < ( ( sqrt ` N ) x. E ) )