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	$⊢ φ \to I \in Fin$
	rrndistlt.z	$⊢ φ \to I \neq \emptyset$
	rrndistlt.n	$⊢ N = \|I\|$
	rrndistlt.x	$⊢ φ \to X \in (ℝ^{I})$
	rrndistlt.y	$⊢ φ \to Y \in (ℝ^{I})$
	rrndistlt.l	$⊢ (φ \land i \in I) \to \|X (i) - Y (i)\| < E$
	rrndistlt.e	$⊢ φ \to E \in ℝ^{+}$
	rrndistlt.d	$⊢ D = dist (I)$
Assertion	rrndistlt	$⊢ φ \to X D Y < \sqrt{N} E$

Proof

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

Metamath Proof Explorer

Theorem rrndistlt

Proof