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 φ I Fin
rrndistlt.z φ I
rrndistlt.n N = I
rrndistlt.x φ X I
rrndistlt.y φ Y I
rrndistlt.l φ i I X i Y i < E
rrndistlt.e φ E +
rrndistlt.d D = dist I
Assertion rrndistlt φ X D Y < N E

Proof

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