Step |
Hyp |
Ref |
Expression |
1 |
|
caures.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
caures.3 |
|- ( ph -> M e. ZZ ) |
3 |
|
caures.4 |
|- ( ph -> D e. ( Met ` X ) ) |
4 |
|
caushft.4 |
|- W = ( ZZ>= ` ( M + N ) ) |
5 |
|
caushft.5 |
|- ( ph -> N e. ZZ ) |
6 |
|
caushft.7 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` ( k + N ) ) ) |
7 |
|
caushft.8 |
|- ( ph -> F e. ( Cau ` D ) ) |
8 |
|
caushft.9 |
|- ( ph -> G : W --> X ) |
9 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
10 |
3 9
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
11 |
6
|
ralrimiva |
|- ( ph -> A. k e. Z ( F ` k ) = ( G ` ( k + N ) ) ) |
12 |
|
fveq2 |
|- ( k = j -> ( F ` k ) = ( F ` j ) ) |
13 |
|
fvoveq1 |
|- ( k = j -> ( G ` ( k + N ) ) = ( G ` ( j + N ) ) ) |
14 |
12 13
|
eqeq12d |
|- ( k = j -> ( ( F ` k ) = ( G ` ( k + N ) ) <-> ( F ` j ) = ( G ` ( j + N ) ) ) ) |
15 |
14
|
rspccva |
|- ( ( A. k e. Z ( F ` k ) = ( G ` ( k + N ) ) /\ j e. Z ) -> ( F ` j ) = ( G ` ( j + N ) ) ) |
16 |
11 15
|
sylan |
|- ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` ( j + N ) ) ) |
17 |
1 10 2 6 16
|
iscau4 |
|- ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) ) ) ) |
18 |
7 17
|
mpbid |
|- ( ph -> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) ) ) |
19 |
18
|
simprd |
|- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) ) |
20 |
1
|
eleq2i |
|- ( j e. Z <-> j e. ( ZZ>= ` M ) ) |
21 |
20
|
biimpi |
|- ( j e. Z -> j e. ( ZZ>= ` M ) ) |
22 |
|
eluzadd |
|- ( ( j e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( j + N ) e. ( ZZ>= ` ( M + N ) ) ) |
23 |
21 5 22
|
syl2anr |
|- ( ( ph /\ j e. Z ) -> ( j + N ) e. ( ZZ>= ` ( M + N ) ) ) |
24 |
23 4
|
eleqtrrdi |
|- ( ( ph /\ j e. Z ) -> ( j + N ) e. W ) |
25 |
|
simplr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. Z ) |
26 |
25 1
|
eleqtrdi |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. ( ZZ>= ` M ) ) |
27 |
|
eluzelz |
|- ( j e. ( ZZ>= ` M ) -> j e. ZZ ) |
28 |
26 27
|
syl |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> j e. ZZ ) |
29 |
5
|
ad2antrr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> N e. ZZ ) |
30 |
|
simpr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. ( ZZ>= ` ( j + N ) ) ) |
31 |
|
eluzsub |
|- ( ( j e. ZZ /\ N e. ZZ /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( m - N ) e. ( ZZ>= ` j ) ) |
32 |
28 29 30 31
|
syl3anc |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( m - N ) e. ( ZZ>= ` j ) ) |
33 |
|
simp3 |
|- ( ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) |
34 |
33
|
ralimi |
|- ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) |
35 |
|
fvoveq1 |
|- ( k = ( m - N ) -> ( G ` ( k + N ) ) = ( G ` ( ( m - N ) + N ) ) ) |
36 |
35
|
oveq1d |
|- ( k = ( m - N ) -> ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) = ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) ) |
37 |
36
|
breq1d |
|- ( k = ( m - N ) -> ( ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x <-> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x ) ) |
38 |
37
|
rspcv |
|- ( ( m - N ) e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x ) ) |
39 |
32 34 38
|
syl2im |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x ) ) |
40 |
|
eluzelz |
|- ( m e. ( ZZ>= ` ( j + N ) ) -> m e. ZZ ) |
41 |
40
|
adantl |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. ZZ ) |
42 |
41
|
zcnd |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. CC ) |
43 |
5
|
zcnd |
|- ( ph -> N e. CC ) |
44 |
43
|
ad2antrr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> N e. CC ) |
45 |
42 44
|
npcand |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( m - N ) + N ) = m ) |
46 |
45
|
fveq2d |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` ( ( m - N ) + N ) ) = ( G ` m ) ) |
47 |
46
|
oveq1d |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) = ( ( G ` m ) D ( G ` ( j + N ) ) ) ) |
48 |
3
|
ad2antrr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> D e. ( Met ` X ) ) |
49 |
8
|
ad2antrr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> G : W --> X ) |
50 |
4
|
uztrn2 |
|- ( ( ( j + N ) e. W /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. W ) |
51 |
24 50
|
sylan |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> m e. W ) |
52 |
49 51
|
ffvelrnd |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` m ) e. X ) |
53 |
8
|
adantr |
|- ( ( ph /\ j e. Z ) -> G : W --> X ) |
54 |
53 24
|
ffvelrnd |
|- ( ( ph /\ j e. Z ) -> ( G ` ( j + N ) ) e. X ) |
55 |
54
|
adantr |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( G ` ( j + N ) ) e. X ) |
56 |
|
metsym |
|- ( ( D e. ( Met ` X ) /\ ( G ` m ) e. X /\ ( G ` ( j + N ) ) e. X ) -> ( ( G ` m ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) ) |
57 |
48 52 55 56
|
syl3anc |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` m ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) ) |
58 |
47 57
|
eqtrd |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) ) |
59 |
58
|
breq1d |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( ( ( G ` ( ( m - N ) + N ) ) D ( G ` ( j + N ) ) ) < x <-> ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) ) |
60 |
39 59
|
sylibd |
|- ( ( ( ph /\ j e. Z ) /\ m e. ( ZZ>= ` ( j + N ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) ) |
61 |
60
|
ralrimdva |
|- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) ) |
62 |
|
fveq2 |
|- ( n = ( j + N ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( j + N ) ) ) |
63 |
|
fveq2 |
|- ( n = ( j + N ) -> ( G ` n ) = ( G ` ( j + N ) ) ) |
64 |
63
|
oveq1d |
|- ( n = ( j + N ) -> ( ( G ` n ) D ( G ` m ) ) = ( ( G ` ( j + N ) ) D ( G ` m ) ) ) |
65 |
64
|
breq1d |
|- ( n = ( j + N ) -> ( ( ( G ` n ) D ( G ` m ) ) < x <-> ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) ) |
66 |
62 65
|
raleqbidv |
|- ( n = ( j + N ) -> ( A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x <-> A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) ) |
67 |
66
|
rspcev |
|- ( ( ( j + N ) e. W /\ A. m e. ( ZZ>= ` ( j + N ) ) ( ( G ` ( j + N ) ) D ( G ` m ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) |
68 |
24 61 67
|
syl6an |
|- ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) ) |
69 |
68
|
rexlimdva |
|- ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) ) |
70 |
69
|
ralimdv |
|- ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( G ` ( k + N ) ) e. X /\ ( ( G ` ( k + N ) ) D ( G ` ( j + N ) ) ) < x ) -> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) ) |
71 |
19 70
|
mpd |
|- ( ph -> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) |
72 |
2 5
|
zaddcld |
|- ( ph -> ( M + N ) e. ZZ ) |
73 |
|
eqidd |
|- ( ( ph /\ m e. W ) -> ( G ` m ) = ( G ` m ) ) |
74 |
|
eqidd |
|- ( ( ph /\ n e. W ) -> ( G ` n ) = ( G ` n ) ) |
75 |
4 10 72 73 74 8
|
iscauf |
|- ( ph -> ( G e. ( Cau ` D ) <-> A. x e. RR+ E. n e. W A. m e. ( ZZ>= ` n ) ( ( G ` n ) D ( G ` m ) ) < x ) ) |
76 |
71 75
|
mpbird |
|- ( ph -> G e. ( Cau ` D ) ) |