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
|- X = ( RR ^m I )
rrndstprj1.1
|- M = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion rrndstprj2
|- ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( F ( Rn ` I ) G ) < ( R x. ( sqrt ` ( # ` I ) ) ) )

Proof

Step Hyp Ref Expression
1 rrnval.1
 |-  X = ( RR ^m I )
2 rrndstprj1.1
 |-  M = ( ( abs o. - ) |` ( RR X. RR ) )
3 simpl1
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> I e. ( Fin \ { (/) } ) )
4 3 eldifad
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> I e. Fin )
5 simpl2
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> F e. X )
6 simpl3
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> G e. X )
7 1 rrnmval
 |-  ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F ( Rn ` I ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
8 4 5 6 7 syl3anc
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( F ( Rn ` I ) G ) = ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
9 eldifsni
 |-  ( I e. ( Fin \ { (/) } ) -> I =/= (/) )
10 3 9 syl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> I =/= (/) )
11 5 1 eleqtrdi
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> F e. ( RR ^m I ) )
12 elmapi
 |-  ( F e. ( RR ^m I ) -> F : I --> RR )
13 11 12 syl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> F : I --> RR )
14 13 ffvelrnda
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( F ` k ) e. RR )
15 6 1 eleqtrdi
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> G e. ( RR ^m I ) )
16 elmapi
 |-  ( G e. ( RR ^m I ) -> G : I --> RR )
17 15 16 syl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> G : I --> RR )
18 17 ffvelrnda
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( G ` k ) e. RR )
19 14 18 resubcld
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( F ` k ) - ( G ` k ) ) e. RR )
20 19 resqcld
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR )
21 simprl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> R e. RR+ )
22 21 rpred
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> R e. RR )
23 22 resqcld
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( R ^ 2 ) e. RR )
24 23 adantr
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( R ^ 2 ) e. RR )
25 absresq
 |-  ( ( ( F ` k ) - ( G ` k ) ) e. RR -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) ^ 2 ) = ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
26 19 25 syl
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) ^ 2 ) = ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
27 2 remetdval
 |-  ( ( ( F ` k ) e. RR /\ ( G ` k ) e. RR ) -> ( ( F ` k ) M ( G ` k ) ) = ( abs ` ( ( F ` k ) - ( G ` k ) ) ) )
28 14 18 27 syl2anc
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( F ` k ) M ( G ` k ) ) = ( abs ` ( ( F ` k ) - ( G ` k ) ) ) )
29 simprr
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> A. n e. I ( ( F ` n ) M ( G ` n ) ) < R )
30 fveq2
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
31 fveq2
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
32 30 31 oveq12d
 |-  ( n = k -> ( ( F ` n ) M ( G ` n ) ) = ( ( F ` k ) M ( G ` k ) ) )
33 32 breq1d
 |-  ( n = k -> ( ( ( F ` n ) M ( G ` n ) ) < R <-> ( ( F ` k ) M ( G ` k ) ) < R ) )
34 33 rspccva
 |-  ( ( A. n e. I ( ( F ` n ) M ( G ` n ) ) < R /\ k e. I ) -> ( ( F ` k ) M ( G ` k ) ) < R )
35 29 34 sylan
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( F ` k ) M ( G ` k ) ) < R )
36 28 35 eqbrtrrd
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < R )
37 19 recnd
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( F ` k ) - ( G ` k ) ) e. CC )
38 37 abscld
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( abs ` ( ( F ` k ) - ( G ` k ) ) ) e. RR )
39 22 adantr
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> R e. RR )
40 37 absge0d
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> 0 <_ ( abs ` ( ( F ` k ) - ( G ` k ) ) ) )
41 21 rpge0d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> 0 <_ R )
42 41 adantr
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> 0 <_ R )
43 38 39 40 42 lt2sqd
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) < R <-> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) ^ 2 ) < ( R ^ 2 ) ) )
44 36 43 mpbid
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( abs ` ( ( F ` k ) - ( G ` k ) ) ) ^ 2 ) < ( R ^ 2 ) )
45 26 44 eqbrtrrd
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) < ( R ^ 2 ) )
46 4 10 20 24 45 fsumlt
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) < sum_ k e. I ( R ^ 2 ) )
47 4 20 fsumrecl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR )
48 19 sqge0d
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) /\ k e. I ) -> 0 <_ ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
49 4 20 48 fsumge0
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> 0 <_ sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
50 resqrtth
 |-  ( ( sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) e. RR /\ 0 <_ sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) = sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
51 47 49 50 syl2anc
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) = sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
52 hashnncl
 |-  ( I e. Fin -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
53 4 52 syl
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
54 10 53 mpbird
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( # ` I ) e. NN )
55 54 nnrpd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( # ` I ) e. RR+ )
56 55 rpred
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( # ` I ) e. RR )
57 55 rpge0d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> 0 <_ ( # ` I ) )
58 resqrtth
 |-  ( ( ( # ` I ) e. RR /\ 0 <_ ( # ` I ) ) -> ( ( sqrt ` ( # ` I ) ) ^ 2 ) = ( # ` I ) )
59 56 57 58 syl2anc
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( sqrt ` ( # ` I ) ) ^ 2 ) = ( # ` I ) )
60 59 oveq2d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( R ^ 2 ) x. ( ( sqrt ` ( # ` I ) ) ^ 2 ) ) = ( ( R ^ 2 ) x. ( # ` I ) ) )
61 23 recnd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( R ^ 2 ) e. CC )
62 55 rpcnd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( # ` I ) e. CC )
63 61 62 mulcomd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( R ^ 2 ) x. ( # ` I ) ) = ( ( # ` I ) x. ( R ^ 2 ) ) )
64 60 63 eqtrd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( R ^ 2 ) x. ( ( sqrt ` ( # ` I ) ) ^ 2 ) ) = ( ( # ` I ) x. ( R ^ 2 ) ) )
65 21 rpcnd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> R e. CC )
66 55 rpsqrtcld
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( sqrt ` ( # ` I ) ) e. RR+ )
67 66 rpcnd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( sqrt ` ( # ` I ) ) e. CC )
68 65 67 sqmuld
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( R x. ( sqrt ` ( # ` I ) ) ) ^ 2 ) = ( ( R ^ 2 ) x. ( ( sqrt ` ( # ` I ) ) ^ 2 ) ) )
69 fsumconst
 |-  ( ( I e. Fin /\ ( R ^ 2 ) e. CC ) -> sum_ k e. I ( R ^ 2 ) = ( ( # ` I ) x. ( R ^ 2 ) ) )
70 4 61 69 syl2anc
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> sum_ k e. I ( R ^ 2 ) = ( ( # ` I ) x. ( R ^ 2 ) ) )
71 64 68 70 3eqtr4d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( R x. ( sqrt ` ( # ` I ) ) ) ^ 2 ) = sum_ k e. I ( R ^ 2 ) )
72 46 51 71 3brtr4d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) < ( ( R x. ( sqrt ` ( # ` I ) ) ) ^ 2 ) )
73 47 49 resqrtcld
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) e. RR )
74 21 66 rpmulcld
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( R x. ( sqrt ` ( # ` I ) ) ) e. RR+ )
75 74 rpred
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( R x. ( sqrt ` ( # ` I ) ) ) e. RR )
76 47 49 sqrtge0d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> 0 <_ ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
77 74 rpge0d
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> 0 <_ ( R x. ( sqrt ` ( # ` I ) ) ) )
78 73 75 76 77 lt2sqd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) < ( R x. ( sqrt ` ( # ` I ) ) ) <-> ( ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) ^ 2 ) < ( ( R x. ( sqrt ` ( # ` I ) ) ) ^ 2 ) ) )
79 72 78 mpbird
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( sqrt ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) < ( R x. ( sqrt ` ( # ` I ) ) ) )
80 8 79 eqbrtrd
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( F ( Rn ` I ) G ) < ( R x. ( sqrt ` ( # ` I ) ) ) )