Theorem rrndstprj2

Description: Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	rrnval.1	⊢ 𝑋 = ( ℝ ↑m 𝐼 )
	rrndstprj1.1	⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion	rrndstprj2	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) < ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2		rrndstprj1.1	⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
3		simpl1	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐼 ∈ ( Fin ∖ { ∅ } ) )
4	3	eldifad	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐼 ∈ Fin )
5		simpl2	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐹 ∈ 𝑋 )
6		simpl3	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐺 ∈ 𝑋 )
7	1	rrnmval	⊢ ( ( 𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
8	4 5 6 7	syl3anc	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
9		eldifsni	⊢ ( 𝐼 ∈ ( Fin ∖ { ∅ } ) → 𝐼 ≠ ∅ )
10	3 9	syl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐼 ≠ ∅ )
11	5 1	eleqtrdi	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
12		elmapi	⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
13	11 12	syl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐹 : 𝐼 ⟶ ℝ )
14	13	ffvelcdmda	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
15	6 1	eleqtrdi	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐺 ∈ ( ℝ ↑m 𝐼 ) )
16		elmapi	⊢ ( 𝐺 ∈ ( ℝ ↑m 𝐼 ) → 𝐺 : 𝐼 ⟶ ℝ )
17	15 16	syl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝐺 : 𝐼 ⟶ ℝ )
18	17	ffvelcdmda	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
19	14 18	resubcld	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
20	19	resqcld	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
21		simprl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝑅 ∈ ℝ+ )
22	21	rpred	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝑅 ∈ ℝ )
23	22	resqcld	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
24	23	adantr	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
25		absresq	⊢ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
26	19 25	syl	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) ↑ 2 ) = ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
27	2	remetdval	⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) )
28	14 18 27	syl2anc	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) )
29		simprr	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 )
30		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
31		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
32	30 31	oveq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) )
33	32	breq1d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) < 𝑅 ) )
34	33	rspccva	⊢ ( ( ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) < 𝑅 )
35	29 34	sylan	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑀 ( 𝐺 ‘ 𝑘 ) ) < 𝑅 )
36	28 35	eqbrtrrd	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑅 )
37	19	recnd	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
38	37	abscld	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ )
39	22	adantr	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑅 ∈ ℝ )
40	37	absge0d	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) )
41	21	rpge0d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 0 ≤ 𝑅 )
42	41	adantr	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ 𝑅 )
43	38 39 40 42	lt2sqd	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑅 ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) ) )
44	36 43	mpbid	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) )
45	26 44	eqbrtrrd	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) < ( 𝑅 ↑ 2 ) )
46	4 10 20 24 45	fsumlt	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) < Σ 𝑘 ∈ 𝐼 ( 𝑅 ↑ 2 ) )
47	4 20	fsumrecl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ )
48	19	sqge0d	⊢ ( ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
49	4 20 48	fsumge0	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
50		resqrtth	⊢ ( ( Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
51	47 49 50	syl2anc	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) )
52		hashnncl	⊢ ( 𝐼 ∈ Fin → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
53	4 52	syl	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
54	10 53	mpbird	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℕ )
55	54	nnrpd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
56	55	rpred	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
57	55	rpge0d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 0 ≤ ( ♯ ‘ 𝐼 ) )
58		resqrtth	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ 𝐼 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ↑ 2 ) = ( ♯ ‘ 𝐼 ) )
59	56 57 58	syl2anc	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ↑ 2 ) = ( ♯ ‘ 𝐼 ) )
60	59	oveq2d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) · ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ↑ 2 ) ) = ( ( 𝑅 ↑ 2 ) · ( ♯ ‘ 𝐼 ) ) )
61	23	recnd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
62	55	rpcnd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ♯ ‘ 𝐼 ) ∈ ℂ )
63	61 62	mulcomd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) · ( ♯ ‘ 𝐼 ) ) = ( ( ♯ ‘ 𝐼 ) · ( 𝑅 ↑ 2 ) ) )
64	60 63	eqtrd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( 𝑅 ↑ 2 ) · ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ↑ 2 ) ) = ( ( ♯ ‘ 𝐼 ) · ( 𝑅 ↑ 2 ) ) )
65	21	rpcnd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 𝑅 ∈ ℂ )
66	55	rpsqrtcld	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ+ )
67	66	rpcnd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℂ )
68	65 67	sqmuld	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↑ 2 ) = ( ( 𝑅 ↑ 2 ) · ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ↑ 2 ) ) )
69		fsumconst	⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑅 ↑ 2 ) ∈ ℂ ) → Σ 𝑘 ∈ 𝐼 ( 𝑅 ↑ 2 ) = ( ( ♯ ‘ 𝐼 ) · ( 𝑅 ↑ 2 ) ) )
70	4 61 69	syl2anc	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → Σ 𝑘 ∈ 𝐼 ( 𝑅 ↑ 2 ) = ( ( ♯ ‘ 𝐼 ) · ( 𝑅 ↑ 2 ) ) )
71	64 68 70	3eqtr4d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↑ 2 ) = Σ 𝑘 ∈ 𝐼 ( 𝑅 ↑ 2 ) )
72	46 51 71	3brtr4d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) < ( ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↑ 2 ) )
73	47 49	resqrtcld	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ∈ ℝ )
74	21 66	rpmulcld	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ+ )
75	74	rpred	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
76	47 49	sqrtge0d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 0 ≤ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) )
77	74	rpge0d	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → 0 ≤ ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
78	73 75 76 77	lt2sqd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) < ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↔ ( ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) ↑ 2 ) < ( ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↑ 2 ) ) )
79	72 78	mpbird	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ↑ 2 ) ) < ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
80	8 79	eqbrtrd	⊢ ( ( ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝐹 ‘ 𝑛 ) 𝑀 ( 𝐺 ‘ 𝑛 ) ) < 𝑅 ) ) → ( 𝐹 ( ℝn ‘ 𝐼 ) 𝐺 ) < ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )