Step |
Hyp |
Ref |
Expression |
1 |
|
ulm2.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
ulm2.m |
|- ( ph -> M e. ZZ ) |
3 |
|
ulm2.f |
|- ( ph -> F : Z --> ( CC ^m S ) ) |
4 |
|
ulm2.b |
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = B ) |
5 |
|
ulm2.a |
|- ( ( ph /\ z e. S ) -> ( G ` z ) = A ) |
6 |
|
ulm2.g |
|- ( ph -> G : S --> CC ) |
7 |
|
ulm2.s |
|- ( ph -> S e. V ) |
8 |
|
ulmval |
|- ( S e. V -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) |
9 |
7 8
|
syl |
|- ( ph -> ( F ( ~~>u ` S ) G <-> E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) |
10 |
|
3anan12 |
|- ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) |
11 |
3
|
fdmd |
|- ( ph -> dom F = Z ) |
12 |
|
fdm |
|- ( F : ( ZZ>= ` n ) --> ( CC ^m S ) -> dom F = ( ZZ>= ` n ) ) |
13 |
11 12
|
sylan9req |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> Z = ( ZZ>= ` n ) ) |
14 |
1 13
|
eqtr3id |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( ZZ>= ` M ) = ( ZZ>= ` n ) ) |
15 |
2
|
adantr |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> M e. ZZ ) |
16 |
|
uz11 |
|- ( M e. ZZ -> ( ( ZZ>= ` M ) = ( ZZ>= ` n ) <-> M = n ) ) |
17 |
15 16
|
syl |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( ( ZZ>= ` M ) = ( ZZ>= ` n ) <-> M = n ) ) |
18 |
14 17
|
mpbid |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> M = n ) |
19 |
18
|
eqcomd |
|- ( ( ph /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> n = M ) |
20 |
|
fveq2 |
|- ( n = M -> ( ZZ>= ` n ) = ( ZZ>= ` M ) ) |
21 |
20 1
|
eqtr4di |
|- ( n = M -> ( ZZ>= ` n ) = Z ) |
22 |
21
|
feq2d |
|- ( n = M -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) <-> F : Z --> ( CC ^m S ) ) ) |
23 |
22
|
biimparc |
|- ( ( F : Z --> ( CC ^m S ) /\ n = M ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) ) |
24 |
3 23
|
sylan |
|- ( ( ph /\ n = M ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) ) |
25 |
19 24
|
impbida |
|- ( ph -> ( F : ( ZZ>= ` n ) --> ( CC ^m S ) <-> n = M ) ) |
26 |
25
|
anbi1d |
|- ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) |
27 |
6
|
biantrurd |
|- ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) ) ) |
28 |
|
simp-4l |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ph ) |
29 |
|
simpr |
|- ( ( ph /\ n = M ) -> n = M ) |
30 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
31 |
2 30
|
syl |
|- ( ph -> M e. ( ZZ>= ` M ) ) |
32 |
31 1
|
eleqtrrdi |
|- ( ph -> M e. Z ) |
33 |
32
|
adantr |
|- ( ( ph /\ n = M ) -> M e. Z ) |
34 |
29 33
|
eqeltrd |
|- ( ( ph /\ n = M ) -> n e. Z ) |
35 |
1
|
uztrn2 |
|- ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z ) |
36 |
34 35
|
sylan |
|- ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) -> j e. Z ) |
37 |
1
|
uztrn2 |
|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z ) |
38 |
36 37
|
sylan |
|- ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z ) |
39 |
38
|
adantr |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> k e. Z ) |
40 |
|
simpr |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> z e. S ) |
41 |
28 39 40 4
|
syl12anc |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) = B ) |
42 |
28 5
|
sylancom |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( G ` z ) = A ) |
43 |
41 42
|
oveq12d |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( ( F ` k ) ` z ) - ( G ` z ) ) = ( B - A ) ) |
44 |
43
|
fveq2d |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( B - A ) ) ) |
45 |
44
|
breq1d |
|- ( ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> ( abs ` ( B - A ) ) < x ) ) |
46 |
45
|
ralbidva |
|- ( ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. z e. S ( abs ` ( B - A ) ) < x ) ) |
47 |
46
|
ralbidva |
|- ( ( ( ph /\ n = M ) /\ j e. ( ZZ>= ` n ) ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
48 |
47
|
rexbidva |
|- ( ( ph /\ n = M ) -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
49 |
48
|
ralbidv |
|- ( ( ph /\ n = M ) -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
50 |
49
|
pm5.32da |
|- ( ph -> ( ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) ) |
51 |
26 27 50
|
3bitr3d |
|- ( ph -> ( ( G : S --> CC /\ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) ) |
52 |
10 51
|
syl5bb |
|- ( ph -> ( ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) ) |
53 |
52
|
rexbidv |
|- ( ph -> ( E. n e. ZZ ( F : ( ZZ>= ` n ) --> ( CC ^m S ) /\ G : S --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) <-> E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) ) |
54 |
21
|
rexeqdv |
|- ( n = M -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
55 |
54
|
ralbidv |
|- ( n = M -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
56 |
55
|
ceqsrexv |
|- ( M e. ZZ -> ( E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
57 |
2 56
|
syl |
|- ( ph -> ( E. n e. ZZ ( n = M /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |
58 |
9 53 57
|
3bitrd |
|- ( ph -> ( F ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( B - A ) ) < x ) ) |