Metamath Proof Explorer

Theorem rrncmslem

Description: Lemma for rrncms . (Contributed by Jeff Madsen, 6-Jun-2014) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses rrnval.1 
|- X = ( RR ^m I )
rrndstprj1.1 
|- M = ( ( abs o. - ) |` ( RR X. RR ) )
rrncms.3 
|- J = ( MetOpen ` ( Rn ` I ) )
rrncms.4 
|- ( ph -> I e. Fin )
rrncms.5 
|- ( ph -> F e. ( Cau ` ( Rn ` I ) ) )
rrncms.6 
|- ( ph -> F : NN --> X )
rrncms.7 
|- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )
Assertion rrncmslem 
|- ( ph -> F e. dom ( ~~>t ` J ) )

Proof

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