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	$$⊢\phi \to I\in \mathrm{Fin}$$
	rrndistlt.z	$$⊢\phi \to I\ne \varnothing$$
	rrndistlt.n	$$⊢N=\left|I\right|$$
	rrndistlt.x	$$⊢\phi \to X\in \left({ℝ}^I\right)$$
	rrndistlt.y	$$⊢\phi \to Y\in \left({ℝ}^I\right)$$
	rrndistlt.l	$$⊢\left(\phi \wedge i\in I\right)\to \left|X\left(i\right)-Y\left(i\right)\right|<E$$
	rrndistlt.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	rrndistlt.d
Assertion	rrndistlt	$$⊢\phi \to XDY<\sqrt{N}E$$

Proof

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