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 ⊢ ( 𝜑 → 𝐼 ∈ Fin )
rrndistlt.z ⊢ ( 𝜑 → 𝐼 ≠ ∅ )
rrndistlt.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
rrndistlt.x ⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
rrndistlt.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝐼 ) )
rrndistlt.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) < 𝐸 )
rrndistlt.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
rrndistlt.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion rrndistlt ( 𝜑 → ( 𝑋 𝐷 𝑌 ) < ( ( √ ‘ 𝑁 ) · 𝐸 ) )

Proof

Step Hyp Ref Expression
1 rrndistlt.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
2 rrndistlt.z ⊢ ( 𝜑 → 𝐼 ≠ ∅ )
3 rrndistlt.n ⊢ 𝑁 = ( ♯ ‘ 𝐼 )
4 rrndistlt.x ⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
5 rrndistlt.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝐼 ) )
6 rrndistlt.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) < 𝐸 )
7 rrndistlt.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8 rrndistlt.d ⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
9 elmapi ⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ ℝ )
10 4 9 syl ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ℝ )
11 ax-resscn ⊢ ℝ ⊆ ℂ
12 11 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
13 10 12 fssd ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ℂ )
14 13 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℂ )
15 elmapi ⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → 𝑌 : 𝐼 ⟶ ℝ )
16 5 15 syl ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℝ )
17 16 12 fssd ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℂ )
18 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℂ )
19 14 18 subcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ∈ ℂ )
20 19 abscld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ∈ ℝ )
21 20 resqcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) ∈ ℝ )
22 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
23 22 resqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐸 ↑ 2 ) ∈ ℝ )
25 19 absge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ≤ ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) )
26 22 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐸 ∈ ℝ )
27 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐸 ∈ ℝ+ )
28 27 rpge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ≤ 𝐸 )
29 lt2sq ⊢ ( ( ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ) ∧ ( 𝐸 ∈ ℝ ∧ 0 ≤ 𝐸 ) ) → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) < 𝐸 ↔ ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) < ( 𝐸 ↑ 2 ) ) )
30 20 25 26 28 29 syl22anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) < 𝐸 ↔ ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) < ( 𝐸 ↑ 2 ) ) )
31 6 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) < ( 𝐸 ↑ 2 ) )
32 1 2 21 24 31 fsumlt ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐼 ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝐼 ( 𝐸 ↑ 2 ) )
33 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ )
34 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
35 33 34 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ∈ ℝ )
36 absresq ⊢ ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ∈ ℝ → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) = ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) = ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) = ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) )
39 38 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ 𝐼 ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) )
40 11 23 sseldi ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
41 fsumconst ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝐸 ↑ 2 ) ∈ ℂ ) → Σ 𝑖 ∈ 𝐼 ( 𝐸 ↑ 2 ) = ( ( ♯ ‘ 𝐼 ) · ( 𝐸 ↑ 2 ) ) )
42 1 40 41 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐼 ( 𝐸 ↑ 2 ) = ( ( ♯ ‘ 𝐼 ) · ( 𝐸 ↑ 2 ) ) )
43 eqcom ⊢ ( 𝑁 = ( ♯ ‘ 𝐼 ) ↔ ( ♯ ‘ 𝐼 ) = 𝑁 )
44 3 43 mpbi ⊢ ( ♯ ‘ 𝐼 ) = 𝑁
45 44 oveq1i ⊢ ( ( ♯ ‘ 𝐼 ) · ( 𝐸 ↑ 2 ) ) = ( 𝑁 · ( 𝐸 ↑ 2 ) )
46 45 a1i ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( 𝐸 ↑ 2 ) ) = ( 𝑁 · ( 𝐸 ↑ 2 ) ) )
47 42 46 eqtr2d ⊢ ( 𝜑 → ( 𝑁 · ( 𝐸 ↑ 2 ) ) = Σ 𝑖 ∈ 𝐼 ( 𝐸 ↑ 2 ) )
48 39 47 breq12d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) < ( 𝑁 · ( 𝐸 ↑ 2 ) ) ↔ Σ 𝑖 ∈ 𝐼 ( ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝐼 ( 𝐸 ↑ 2 ) ) )
49 32 48 mpbird ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) < ( 𝑁 · ( 𝐸 ↑ 2 ) ) )
50 nfv ⊢ Ⅎ 𝑖 𝜑
51 35 resqcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
52 50 1 51 fsumreclf ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
53 35 sqge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
54 1 51 53 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
55 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
56 1 55 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
57 3 56 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
58 57 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
59 58 23 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( 𝐸 ↑ 2 ) ) ∈ ℝ )
60 57 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
61 22 sqge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐸 ↑ 2 ) )
62 58 23 60 61 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 · ( 𝐸 ↑ 2 ) ) )
63 52 54 59 62 sqrtltd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) < ( 𝑁 · ( 𝐸 ↑ 2 ) ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) ) )
64 49 63 mpbid ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) )
65 8 a1i ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
66 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
67 eqid ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m 𝐼 )
68 66 67 rrxdsfi ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
69 1 68 syl ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
70 65 69 eqtrd ⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
71 fveq1 ⊢ ( 𝑓 = 𝑋 → ( 𝑓 ‘ 𝑖 ) = ( 𝑋 ‘ 𝑖 ) )
72 71 adantr ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( 𝑓 ‘ 𝑖 ) = ( 𝑋 ‘ 𝑖 ) )
73 fveq1 ⊢ ( 𝑔 = 𝑌 → ( 𝑔 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
74 73 adantl ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
75 72 74 oveq12d ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) = ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) )
76 75 oveq1d ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
77 76 sumeq2sdv ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) )
78 77 fveq2d ⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) )
79 78 adantl ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) ) → ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑖 ) − ( 𝑔 ‘ 𝑖 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) )
80 52 54 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
81 70 79 4 5 80 ovmpod ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) = ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) )
82 sqrtmul ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) ∧ ( ( 𝐸 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐸 ↑ 2 ) ) ) → ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) = ( ( √ ‘ 𝑁 ) · ( √ ‘ ( 𝐸 ↑ 2 ) ) ) )
83 58 60 23 61 82 syl22anc ⊢ ( 𝜑 → ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) = ( ( √ ‘ 𝑁 ) · ( √ ‘ ( 𝐸 ↑ 2 ) ) ) )
84 7 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐸 )
85 22 84 sqrtsqd ⊢ ( 𝜑 → ( √ ‘ ( 𝐸 ↑ 2 ) ) = 𝐸 )
86 85 oveq2d ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · ( √ ‘ ( 𝐸 ↑ 2 ) ) ) = ( ( √ ‘ 𝑁 ) · 𝐸 ) )
87 83 86 eqtr2d ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · 𝐸 ) = ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) )
88 81 87 breq12d ⊢ ( 𝜑 → ( ( 𝑋 𝐷 𝑌 ) < ( ( √ ‘ 𝑁 ) · 𝐸 ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝐼 ( ( ( 𝑋 ‘ 𝑖 ) − ( 𝑌 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ ( 𝑁 · ( 𝐸 ↑ 2 ) ) ) ) )
89 64 88 mpbird ⊢ ( 𝜑 → ( 𝑋 𝐷 𝑌 ) < ( ( √ ‘ 𝑁 ) · 𝐸 ) )