Step |
Hyp |
Ref |
Expression |
1 |
|
ulmss.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
ulmss.t |
|- ( ph -> T C_ S ) |
3 |
|
ulmss.a |
|- ( ( ph /\ x e. Z ) -> A e. W ) |
4 |
|
ulmss.u |
|- ( ph -> ( x e. Z |-> A ) ( ~~>u ` S ) G ) |
5 |
1
|
uztrn2 |
|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z ) |
6 |
2
|
adantr |
|- ( ( ph /\ k e. Z ) -> T C_ S ) |
7 |
|
ssralv |
|- ( T C_ S -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
8 |
6 7
|
syl |
|- ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
9 |
|
fvres |
|- ( z e. T -> ( ( A |` T ) ` z ) = ( A ` z ) ) |
10 |
9
|
ad2antll |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( A |` T ) ` z ) = ( A ` z ) ) |
11 |
|
simprl |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> x e. Z ) |
12 |
3
|
adantrr |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> A e. W ) |
13 |
12
|
resexd |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( A |` T ) e. _V ) |
14 |
|
eqid |
|- ( x e. Z |-> ( A |` T ) ) = ( x e. Z |-> ( A |` T ) ) |
15 |
14
|
fvmpt2 |
|- ( ( x e. Z /\ ( A |` T ) e. _V ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) ) |
16 |
11 13 15
|
syl2anc |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) ) |
17 |
16
|
fveq1d |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( A |` T ) ` z ) ) |
18 |
|
eqid |
|- ( x e. Z |-> A ) = ( x e. Z |-> A ) |
19 |
18
|
fvmpt2 |
|- ( ( x e. Z /\ A e. W ) -> ( ( x e. Z |-> A ) ` x ) = A ) |
20 |
11 12 19
|
syl2anc |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> A ) ` x ) = A ) |
21 |
20
|
fveq1d |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( A ` z ) ) |
22 |
10 17 21
|
3eqtr4d |
|- ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) ) |
23 |
22
|
ralrimivva |
|- ( ph -> A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) ) |
24 |
|
nfv |
|- F/ k A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) |
25 |
|
nfcv |
|- F/_ x T |
26 |
|
nffvmpt1 |
|- F/_ x ( ( x e. Z |-> ( A |` T ) ) ` k ) |
27 |
|
nfcv |
|- F/_ x z |
28 |
26 27
|
nffv |
|- F/_ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) |
29 |
|
nffvmpt1 |
|- F/_ x ( ( x e. Z |-> A ) ` k ) |
30 |
29 27
|
nffv |
|- F/_ x ( ( ( x e. Z |-> A ) ` k ) ` z ) |
31 |
28 30
|
nfeq |
|- F/ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) |
32 |
25 31
|
nfralw |
|- F/ x A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) |
33 |
|
fveq2 |
|- ( x = k -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( ( x e. Z |-> ( A |` T ) ) ` k ) ) |
34 |
33
|
fveq1d |
|- ( x = k -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) ) |
35 |
|
fveq2 |
|- ( x = k -> ( ( x e. Z |-> A ) ` x ) = ( ( x e. Z |-> A ) ` k ) ) |
36 |
35
|
fveq1d |
|- ( x = k -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) |
37 |
34 36
|
eqeq12d |
|- ( x = k -> ( ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) ) |
38 |
37
|
ralbidv |
|- ( x = k -> ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) ) |
39 |
24 32 38
|
cbvralw |
|- ( A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) |
40 |
23 39
|
sylib |
|- ( ph -> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) |
41 |
40
|
r19.21bi |
|- ( ( ph /\ k e. Z ) -> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) |
42 |
|
fvoveq1 |
|- ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) ) |
43 |
42
|
breq1d |
|- ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
44 |
43
|
ralimi |
|- ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
45 |
|
ralbi |
|- ( A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
46 |
41 44 45
|
3syl |
|- ( ( ph /\ k e. Z ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
47 |
8 46
|
sylibrd |
|- ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
48 |
5 47
|
sylan2 |
|- ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
49 |
48
|
anassrs |
|- ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
50 |
49
|
ralimdva |
|- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
51 |
50
|
reximdva |
|- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
52 |
51
|
ralimdv |
|- ( ph -> ( A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
53 |
|
ulmf |
|- ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) ) |
54 |
4 53
|
syl |
|- ( ph -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) ) |
55 |
|
fdm |
|- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> dom ( x e. Z |-> A ) = ( ZZ>= ` m ) ) |
56 |
18
|
dmmptss |
|- dom ( x e. Z |-> A ) C_ Z |
57 |
55 56
|
eqsstrrdi |
|- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ( ZZ>= ` m ) C_ Z ) |
58 |
|
uzid |
|- ( m e. ZZ -> m e. ( ZZ>= ` m ) ) |
59 |
58
|
adantl |
|- ( ( ph /\ m e. ZZ ) -> m e. ( ZZ>= ` m ) ) |
60 |
|
ssel |
|- ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> m e. Z ) ) |
61 |
|
eluzel2 |
|- ( m e. ( ZZ>= ` M ) -> M e. ZZ ) |
62 |
61 1
|
eleq2s |
|- ( m e. Z -> M e. ZZ ) |
63 |
60 62
|
syl6 |
|- ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> M e. ZZ ) ) |
64 |
57 59 63
|
syl2imc |
|- ( ( ph /\ m e. ZZ ) -> ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) ) |
65 |
64
|
rexlimdva |
|- ( ph -> ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) ) |
66 |
54 65
|
mpd |
|- ( ph -> M e. ZZ ) |
67 |
3
|
ralrimiva |
|- ( ph -> A. x e. Z A e. W ) |
68 |
18
|
fnmpt |
|- ( A. x e. Z A e. W -> ( x e. Z |-> A ) Fn Z ) |
69 |
67 68
|
syl |
|- ( ph -> ( x e. Z |-> A ) Fn Z ) |
70 |
|
frn |
|- ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) |
71 |
70
|
rexlimivw |
|- ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) |
72 |
54 71
|
syl |
|- ( ph -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) |
73 |
|
df-f |
|- ( ( x e. Z |-> A ) : Z --> ( CC ^m S ) <-> ( ( x e. Z |-> A ) Fn Z /\ ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) ) |
74 |
69 72 73
|
sylanbrc |
|- ( ph -> ( x e. Z |-> A ) : Z --> ( CC ^m S ) ) |
75 |
|
eqidd |
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( ( x e. Z |-> A ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) |
76 |
|
eqidd |
|- ( ( ph /\ z e. S ) -> ( G ` z ) = ( G ` z ) ) |
77 |
|
ulmcl |
|- ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> G : S --> CC ) |
78 |
4 77
|
syl |
|- ( ph -> G : S --> CC ) |
79 |
|
ulmscl |
|- ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> S e. _V ) |
80 |
4 79
|
syl |
|- ( ph -> S e. _V ) |
81 |
1 66 74 75 76 78 80
|
ulm2 |
|- ( ph -> ( ( x e. Z |-> A ) ( ~~>u ` S ) G <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
82 |
74
|
fvmptelrn |
|- ( ( ph /\ x e. Z ) -> A e. ( CC ^m S ) ) |
83 |
|
elmapi |
|- ( A e. ( CC ^m S ) -> A : S --> CC ) |
84 |
82 83
|
syl |
|- ( ( ph /\ x e. Z ) -> A : S --> CC ) |
85 |
2
|
adantr |
|- ( ( ph /\ x e. Z ) -> T C_ S ) |
86 |
84 85
|
fssresd |
|- ( ( ph /\ x e. Z ) -> ( A |` T ) : T --> CC ) |
87 |
|
cnex |
|- CC e. _V |
88 |
80 2
|
ssexd |
|- ( ph -> T e. _V ) |
89 |
88
|
adantr |
|- ( ( ph /\ x e. Z ) -> T e. _V ) |
90 |
|
elmapg |
|- ( ( CC e. _V /\ T e. _V ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) ) |
91 |
87 89 90
|
sylancr |
|- ( ( ph /\ x e. Z ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) ) |
92 |
86 91
|
mpbird |
|- ( ( ph /\ x e. Z ) -> ( A |` T ) e. ( CC ^m T ) ) |
93 |
92
|
fmpttd |
|- ( ph -> ( x e. Z |-> ( A |` T ) ) : Z --> ( CC ^m T ) ) |
94 |
|
eqidd |
|- ( ( ph /\ ( k e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) ) |
95 |
|
fvres |
|- ( z e. T -> ( ( G |` T ) ` z ) = ( G ` z ) ) |
96 |
95
|
adantl |
|- ( ( ph /\ z e. T ) -> ( ( G |` T ) ` z ) = ( G ` z ) ) |
97 |
78 2
|
fssresd |
|- ( ph -> ( G |` T ) : T --> CC ) |
98 |
1 66 93 94 96 97 88
|
ulm2 |
|- ( ph -> ( ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) ) |
99 |
52 81 98
|
3imtr4d |
|- ( ph -> ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) ) ) |
100 |
4 99
|
mpd |
|- ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) ) |