Metamath Proof Explorer

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 ‘ 𝐼 ) 𝐺 ) < ( 𝑅 · ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )