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