Step |
Hyp |
Ref |
Expression |
1 |
|
rrnval.1 |
|- X = ( RR ^m I ) |
2 |
|
rrndstprj1.1 |
|- M = ( ( abs o. - ) |` ( RR X. RR ) ) |
3 |
|
rrncms.3 |
|- J = ( MetOpen ` ( Rn ` I ) ) |
4 |
|
rrncms.4 |
|- ( ph -> I e. Fin ) |
5 |
|
rrncms.5 |
|- ( ph -> F e. ( Cau ` ( Rn ` I ) ) ) |
6 |
|
rrncms.6 |
|- ( ph -> F : NN --> X ) |
7 |
|
rrncms.7 |
|- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) ) |
8 |
|
lmrel |
|- Rel ( ~~>t ` J ) |
9 |
|
fvex |
|- ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) e. _V |
10 |
9 7
|
fnmpti |
|- P Fn I |
11 |
10
|
a1i |
|- ( ph -> P Fn I ) |
12 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
13 |
|
1zzd |
|- ( ( ph /\ n e. I ) -> 1 e. ZZ ) |
14 |
|
fveq2 |
|- ( t = k -> ( F ` t ) = ( F ` k ) ) |
15 |
14
|
fveq1d |
|- ( t = k -> ( ( F ` t ) ` n ) = ( ( F ` k ) ` n ) ) |
16 |
|
eqid |
|- ( t e. NN |-> ( ( F ` t ) ` n ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) ) |
17 |
|
fvex |
|- ( ( F ` k ) ` n ) e. _V |
18 |
15 16 17
|
fvmpt |
|- ( k e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) ) |
19 |
18
|
adantl |
|- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) ) |
20 |
6
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. X ) |
21 |
20 1
|
eleqtrdi |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( RR ^m I ) ) |
22 |
|
elmapi |
|- ( ( F ` k ) e. ( RR ^m I ) -> ( F ` k ) : I --> RR ) |
23 |
21 22
|
syl |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) : I --> RR ) |
24 |
23
|
ffvelrnda |
|- ( ( ( ph /\ k e. NN ) /\ n e. I ) -> ( ( F ` k ) ` n ) e. RR ) |
25 |
24
|
an32s |
|- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR ) |
26 |
19 25
|
eqeltrd |
|- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. RR ) |
27 |
26
|
recnd |
|- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. CC ) |
28 |
1
|
rrnmet |
|- ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) ) |
29 |
4 28
|
syl |
|- ( ph -> ( Rn ` I ) e. ( Met ` X ) ) |
30 |
|
metxmet |
|- ( ( Rn ` I ) e. ( Met ` X ) -> ( Rn ` I ) e. ( *Met ` X ) ) |
31 |
29 30
|
syl |
|- ( ph -> ( Rn ` I ) e. ( *Met ` X ) ) |
32 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
33 |
|
eqidd |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) ) |
34 |
|
eqidd |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) ) |
35 |
12 31 32 33 34 6
|
iscauf |
|- ( ph -> ( F e. ( Cau ` ( Rn ` I ) ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) ) |
36 |
5 35
|
mpbid |
|- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) |
37 |
36
|
adantr |
|- ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) |
38 |
4
|
ad3antrrr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> I e. Fin ) |
39 |
|
simpllr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> n e. I ) |
40 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> F : NN --> X ) |
41 |
|
eluznn |
|- ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN ) |
42 |
41
|
adantll |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN ) |
43 |
40 42
|
ffvelrnd |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X ) |
44 |
|
simplr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> j e. NN ) |
45 |
40 44
|
ffvelrnd |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. X ) |
46 |
1 2
|
rrndstprj1 |
|- ( ( ( I e. Fin /\ n e. I ) /\ ( ( F ` k ) e. X /\ ( F ` j ) e. X ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) ) |
47 |
38 39 43 45 46
|
syl22anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) ) |
48 |
29
|
ad3antrrr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( Rn ` I ) e. ( Met ` X ) ) |
49 |
|
metsym |
|- ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) ) |
50 |
48 43 45 49
|
syl3anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) ) |
51 |
47 50
|
breqtrd |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) ) |
52 |
51
|
adantllr |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) ) |
53 |
2
|
remet |
|- M e. ( Met ` RR ) |
54 |
53
|
a1i |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> M e. ( Met ` RR ) ) |
55 |
|
simpll |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ph /\ n e. I ) ) |
56 |
55 42 25
|
syl2anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ` n ) e. RR ) |
57 |
6
|
ffvelrnda |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) e. X ) |
58 |
57 1
|
eleqtrdi |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR ^m I ) ) |
59 |
|
elmapi |
|- ( ( F ` j ) e. ( RR ^m I ) -> ( F ` j ) : I --> RR ) |
60 |
58 59
|
syl |
|- ( ( ph /\ j e. NN ) -> ( F ` j ) : I --> RR ) |
61 |
60
|
ffvelrnda |
|- ( ( ( ph /\ j e. NN ) /\ n e. I ) -> ( ( F ` j ) ` n ) e. RR ) |
62 |
61
|
an32s |
|- ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( ( F ` j ) ` n ) e. RR ) |
63 |
62
|
adantr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ` n ) e. RR ) |
64 |
|
metcl |
|- ( ( M e. ( Met ` RR ) /\ ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR ) |
65 |
54 56 63 64
|
syl3anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR ) |
66 |
65
|
adantllr |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR ) |
67 |
|
metcl |
|- ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR ) |
68 |
48 45 43 67
|
syl3anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR ) |
69 |
68
|
adantllr |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR ) |
70 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
71 |
70
|
adantl |
|- ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> x e. RR ) |
72 |
71
|
ad2antrr |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR ) |
73 |
|
lelttr |
|- ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
74 |
66 69 72 73
|
syl3anc |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
75 |
52 74
|
mpand |
|- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
76 |
75
|
ralimdva |
|- ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
77 |
76
|
reximdva |
|- ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
78 |
77
|
ralimdva |
|- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) ) |
79 |
2
|
remetdval |
|- ( ( ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) ) |
80 |
56 63 79
|
syl2anc |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) ) |
81 |
42 18
|
syl |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) ) |
82 |
|
fveq2 |
|- ( t = j -> ( F ` t ) = ( F ` j ) ) |
83 |
82
|
fveq1d |
|- ( t = j -> ( ( F ` t ) ` n ) = ( ( F ` j ) ` n ) ) |
84 |
|
fvex |
|- ( ( F ` j ) ` n ) e. _V |
85 |
83 16 84
|
fvmpt |
|- ( j e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) ) |
86 |
85
|
ad2antlr |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) ) |
87 |
81 86
|
oveq12d |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) = ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) |
88 |
87
|
fveq2d |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) ) |
89 |
80 88
|
eqtr4d |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) ) |
90 |
89
|
breq1d |
|- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) ) |
91 |
90
|
ralbidva |
|- ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) ) |
92 |
91
|
rexbidva |
|- ( ( ph /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) ) |
93 |
92
|
ralbidv |
|- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) ) |
94 |
78 93
|
sylibd |
|- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) ) |
95 |
37 94
|
mpd |
|- ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) |
96 |
|
nnex |
|- NN e. _V |
97 |
96
|
mptex |
|- ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V |
98 |
97
|
a1i |
|- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V ) |
99 |
12 27 95 98
|
caucvg |
|- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> ) |
100 |
|
climdm |
|- ( ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> <-> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) ) |
101 |
99 100
|
sylib |
|- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) ) |
102 |
|
fveq2 |
|- ( m = n -> ( ( F ` t ) ` m ) = ( ( F ` t ) ` n ) ) |
103 |
102
|
mpteq2dv |
|- ( m = n -> ( t e. NN |-> ( ( F ` t ) ` m ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) ) ) |
104 |
103
|
fveq2d |
|- ( m = n -> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) ) |
105 |
|
fvex |
|- ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) e. _V |
106 |
104 7 105
|
fvmpt |
|- ( n e. I -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) ) |
107 |
106
|
adantl |
|- ( ( ph /\ n e. I ) -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) ) |
108 |
101 107
|
breqtrrd |
|- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) ) |
109 |
12 13 108 26
|
climrecl |
|- ( ( ph /\ n e. I ) -> ( P ` n ) e. RR ) |
110 |
109
|
ralrimiva |
|- ( ph -> A. n e. I ( P ` n ) e. RR ) |
111 |
|
ffnfv |
|- ( P : I --> RR <-> ( P Fn I /\ A. n e. I ( P ` n ) e. RR ) ) |
112 |
11 110 111
|
sylanbrc |
|- ( ph -> P : I --> RR ) |
113 |
|
reex |
|- RR e. _V |
114 |
|
elmapg |
|- ( ( RR e. _V /\ I e. Fin ) -> ( P e. ( RR ^m I ) <-> P : I --> RR ) ) |
115 |
113 4 114
|
sylancr |
|- ( ph -> ( P e. ( RR ^m I ) <-> P : I --> RR ) ) |
116 |
112 115
|
mpbird |
|- ( ph -> P e. ( RR ^m I ) ) |
117 |
116 1
|
eleqtrrdi |
|- ( ph -> P e. X ) |
118 |
|
1nn |
|- 1 e. NN |
119 |
4
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I e. Fin ) |
120 |
20
|
adantlr |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X ) |
121 |
117
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> P e. X ) |
122 |
1
|
rrnmval |
|- ( ( I e. Fin /\ ( F ` k ) e. X /\ P e. X ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) ) |
123 |
119 120 121 122
|
syl3anc |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) ) |
124 |
|
simplrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I = (/) ) |
125 |
124
|
sumeq1d |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) |
126 |
|
sum0 |
|- sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0 |
127 |
125 126
|
eqtrdi |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0 ) |
128 |
127
|
fveq2d |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( sqrt ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) = ( sqrt ` 0 ) ) |
129 |
123 128
|
eqtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqrt ` 0 ) ) |
130 |
|
sqrt0 |
|- ( sqrt ` 0 ) = 0 |
131 |
129 130
|
eqtrdi |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = 0 ) |
132 |
|
simplrl |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> x e. RR+ ) |
133 |
132
|
rpgt0d |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> 0 < x ) |
134 |
131 133
|
eqbrtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) |
135 |
134
|
ralrimiva |
|- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) |
136 |
|
fveq2 |
|- ( j = 1 -> ( ZZ>= ` j ) = ( ZZ>= ` 1 ) ) |
137 |
136 12
|
eqtr4di |
|- ( j = 1 -> ( ZZ>= ` j ) = NN ) |
138 |
137
|
raleqdv |
|- ( j = 1 -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x <-> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
139 |
138
|
rspcev |
|- ( ( 1 e. NN /\ A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) |
140 |
118 135 139
|
sylancr |
|- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) |
141 |
140
|
expr |
|- ( ( ph /\ x e. RR+ ) -> ( I = (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
142 |
|
1zzd |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> 1 e. ZZ ) |
143 |
|
simprl |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> x e. RR+ ) |
144 |
|
simprr |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I =/= (/) ) |
145 |
4
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I e. Fin ) |
146 |
|
hashnncl |
|- ( I e. Fin -> ( ( # ` I ) e. NN <-> I =/= (/) ) ) |
147 |
145 146
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( ( # ` I ) e. NN <-> I =/= (/) ) ) |
148 |
144 147
|
mpbird |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. NN ) |
149 |
148
|
nnrpd |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. RR+ ) |
150 |
149
|
rpsqrtcld |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( sqrt ` ( # ` I ) ) e. RR+ ) |
151 |
143 150
|
rpdivcld |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ ) |
152 |
151
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ ) |
153 |
18
|
adantl |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) ) |
154 |
108
|
adantlr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) ) |
155 |
12 142 152 153 154
|
climi2 |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
156 |
|
1z |
|- 1 e. ZZ |
157 |
12
|
rexuz3 |
|- ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
158 |
156 157
|
ax-mp |
|- ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
159 |
25
|
adantllr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR ) |
160 |
109
|
adantlr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( P ` n ) e. RR ) |
161 |
160
|
adantr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( P ` n ) e. RR ) |
162 |
2
|
remetdval |
|- ( ( ( ( F ` k ) ` n ) e. RR /\ ( P ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) ) |
163 |
159 161 162
|
syl2anc |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) ) |
164 |
163
|
breq1d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
165 |
41 164
|
sylan2 |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
166 |
165
|
anassrs |
|- ( ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
167 |
166
|
ralbidva |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
168 |
167
|
rexbidva |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
169 |
158 168
|
bitr3id |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
170 |
155 169
|
mpbird |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
171 |
170
|
ralrimiva |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
172 |
12
|
rexuz3 |
|- ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
173 |
156 172
|
ax-mp |
|- ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
174 |
|
rexfiuz |
|- ( I e. Fin -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
175 |
145 174
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
176 |
173 175
|
syl5bb |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) |
177 |
171 176
|
mpbird |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) |
178 |
4
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. Fin ) |
179 |
|
simplrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I =/= (/) ) |
180 |
|
eldifsn |
|- ( I e. ( Fin \ { (/) } ) <-> ( I e. Fin /\ I =/= (/) ) ) |
181 |
178 179 180
|
sylanbrc |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. ( Fin \ { (/) } ) ) |
182 |
6
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> F : NN --> X ) |
183 |
182
|
ffvelrnda |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X ) |
184 |
117
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> P e. X ) |
185 |
151
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ ) |
186 |
1 2
|
rrndstprj2 |
|- ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ /\ A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) |
187 |
186
|
expr |
|- ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( x / ( sqrt ` ( # ` I ) ) ) e. RR+ ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) ) |
188 |
181 183 184 185 187
|
syl31anc |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) ) |
189 |
|
simplrl |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. RR+ ) |
190 |
189
|
rpcnd |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. CC ) |
191 |
150
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) e. RR+ ) |
192 |
191
|
rpcnd |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) e. CC ) |
193 |
191
|
rpne0d |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqrt ` ( # ` I ) ) =/= 0 ) |
194 |
190 192 193
|
divcan1d |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) = x ) |
195 |
194
|
breq2d |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) <-> ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
196 |
188 195
|
sylibd |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
197 |
41 196
|
sylan2 |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
198 |
197
|
anassrs |
|- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
199 |
198
|
ralimdva |
|- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
200 |
199
|
reximdva |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqrt ` ( # ` I ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
201 |
177 200
|
mpd |
|- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) |
202 |
201
|
expr |
|- ( ( ph /\ x e. RR+ ) -> ( I =/= (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) |
203 |
141 202
|
pm2.61dne |
|- ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) |
204 |
203
|
ralrimiva |
|- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) |
205 |
3 31 12 32 33 6
|
lmmbrf |
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) ) |
206 |
117 204 205
|
mpbir2and |
|- ( ph -> F ( ~~>t ` J ) P ) |
207 |
|
releldm |
|- ( ( Rel ( ~~>t ` J ) /\ F ( ~~>t ` J ) P ) -> F e. dom ( ~~>t ` J ) ) |
208 |
8 206 207
|
sylancr |
|- ( ph -> F e. dom ( ~~>t ` J ) ) |