This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda 
 |-  ( ( ( ( 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 ffvelcdmda 
 |-  ( ( ( ( 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 ) ) ) )