Step |
Hyp |
Ref |
Expression |
1 |
|
cvgcmp.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
cvgcmp.2 |
|- ( ph -> N e. Z ) |
3 |
|
cvgcmp.3 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) |
4 |
|
cvgcmp.4 |
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR ) |
5 |
|
cvgcmp.5 |
|- ( ph -> seq M ( + , F ) e. dom ~~> ) |
6 |
|
cvgcmp.6 |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( G ` k ) ) |
7 |
|
cvgcmp.7 |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( G ` k ) <_ ( F ` k ) ) |
8 |
|
seqex |
|- seq M ( + , G ) e. _V |
9 |
8
|
a1i |
|- ( ph -> seq M ( + , G ) e. _V ) |
10 |
2 1
|
eleqtrdi |
|- ( ph -> N e. ( ZZ>= ` M ) ) |
11 |
|
eluzel2 |
|- ( N e. ( ZZ>= ` M ) -> M e. ZZ ) |
12 |
10 11
|
syl |
|- ( ph -> M e. ZZ ) |
13 |
1
|
climcau |
|- ( ( M e. ZZ /\ seq M ( + , F ) e. dom ~~> ) -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) |
14 |
12 5 13
|
syl2anc |
|- ( ph -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) |
15 |
1 12 3
|
serfre |
|- ( ph -> seq M ( + , F ) : Z --> RR ) |
16 |
15
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. RR ) |
17 |
16
|
recnd |
|- ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. CC ) |
18 |
17
|
ralrimiva |
|- ( ph -> A. n e. Z ( seq M ( + , F ) ` n ) e. CC ) |
19 |
1
|
r19.29uz |
|- ( ( A. n e. Z ( seq M ( + , F ) ` n ) e. CC /\ E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) |
20 |
19
|
ex |
|- ( A. n e. Z ( seq M ( + , F ) ` n ) e. CC -> ( E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x -> E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) ) |
21 |
18 20
|
syl |
|- ( ph -> ( E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x -> E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) ) |
22 |
21
|
ralimdv |
|- ( ph -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) ) |
23 |
14 22
|
mpd |
|- ( ph -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) |
24 |
1
|
uztrn2 |
|- ( ( N e. Z /\ n e. ( ZZ>= ` N ) ) -> n e. Z ) |
25 |
2 24
|
sylan |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. Z ) |
26 |
1 12 4
|
serfre |
|- ( ph -> seq M ( + , G ) : Z --> RR ) |
27 |
26
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. RR ) |
28 |
27
|
recnd |
|- ( ( ph /\ n e. Z ) -> ( seq M ( + , G ) ` n ) e. CC ) |
29 |
25 28
|
syldan |
|- ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( + , G ) ` n ) e. CC ) |
30 |
29
|
ralrimiva |
|- ( ph -> A. n e. ( ZZ>= ` N ) ( seq M ( + , G ) ` n ) e. CC ) |
31 |
30
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> A. n e. ( ZZ>= ` N ) ( seq M ( + , G ) ` n ) e. CC ) |
32 |
|
simpll |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ph ) |
33 |
32 15
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> seq M ( + , F ) : Z --> RR ) |
34 |
32 2
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> N e. Z ) |
35 |
|
simprl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> m e. ( ZZ>= ` N ) ) |
36 |
1
|
uztrn2 |
|- ( ( N e. Z /\ m e. ( ZZ>= ` N ) ) -> m e. Z ) |
37 |
34 35 36
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> m e. Z ) |
38 |
33 37
|
ffvelrnd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` m ) e. RR ) |
39 |
|
eqid |
|- ( ZZ>= ` N ) = ( ZZ>= ` N ) |
40 |
39
|
uztrn2 |
|- ( ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) -> n e. ( ZZ>= ` N ) ) |
41 |
40
|
adantl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> n e. ( ZZ>= ` N ) ) |
42 |
34 41 24
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> n e. Z ) |
43 |
32 42 16
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` n ) e. RR ) |
44 |
32 42 27
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , G ) ` n ) e. RR ) |
45 |
32 26
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> seq M ( + , G ) : Z --> RR ) |
46 |
45 37
|
ffvelrnd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , G ) ` m ) e. RR ) |
47 |
44 46
|
resubcld |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) e. RR ) |
48 |
37 1
|
eleqtrdi |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> m e. ( ZZ>= ` M ) ) |
49 |
|
simprr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> n e. ( ZZ>= ` m ) ) |
50 |
|
elfzuz |
|- ( k e. ( M ... n ) -> k e. ( ZZ>= ` M ) ) |
51 |
50 1
|
eleqtrrdi |
|- ( k e. ( M ... n ) -> k e. Z ) |
52 |
|
fveq2 |
|- ( m = k -> ( F ` m ) = ( F ` k ) ) |
53 |
|
fveq2 |
|- ( m = k -> ( G ` m ) = ( G ` k ) ) |
54 |
52 53
|
oveq12d |
|- ( m = k -> ( ( F ` m ) - ( G ` m ) ) = ( ( F ` k ) - ( G ` k ) ) ) |
55 |
|
eqid |
|- ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) = ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) |
56 |
|
ovex |
|- ( ( F ` k ) - ( G ` k ) ) e. _V |
57 |
54 55 56
|
fvmpt |
|- ( k e. Z -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) = ( ( F ` k ) - ( G ` k ) ) ) |
58 |
57
|
adantl |
|- ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) = ( ( F ` k ) - ( G ` k ) ) ) |
59 |
3 4
|
resubcld |
|- ( ( ph /\ k e. Z ) -> ( ( F ` k ) - ( G ` k ) ) e. RR ) |
60 |
58 59
|
eqeltrd |
|- ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) e. RR ) |
61 |
32 51 60
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) e. RR ) |
62 |
|
elfzuz |
|- ( k e. ( ( m + 1 ) ... n ) -> k e. ( ZZ>= ` ( m + 1 ) ) ) |
63 |
|
peano2uz |
|- ( m e. ( ZZ>= ` N ) -> ( m + 1 ) e. ( ZZ>= ` N ) ) |
64 |
35 63
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( m + 1 ) e. ( ZZ>= ` N ) ) |
65 |
39
|
uztrn2 |
|- ( ( ( m + 1 ) e. ( ZZ>= ` N ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> k e. ( ZZ>= ` N ) ) |
66 |
64 65
|
sylan |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> k e. ( ZZ>= ` N ) ) |
67 |
1
|
uztrn2 |
|- ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z ) |
68 |
2 67
|
sylan |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. Z ) |
69 |
3 4
|
subge0d |
|- ( ( ph /\ k e. Z ) -> ( 0 <_ ( ( F ` k ) - ( G ` k ) ) <-> ( G ` k ) <_ ( F ` k ) ) ) |
70 |
68 69
|
syldan |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( 0 <_ ( ( F ` k ) - ( G ` k ) ) <-> ( G ` k ) <_ ( F ` k ) ) ) |
71 |
7 70
|
mpbird |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( ( F ` k ) - ( G ` k ) ) ) |
72 |
68 57
|
syl |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) = ( ( F ` k ) - ( G ` k ) ) ) |
73 |
71 72
|
breqtrrd |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) ) |
74 |
32 66 73
|
syl2an2r |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> 0 <_ ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) ) |
75 |
62 74
|
sylan2 |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ( m + 1 ) ... n ) ) -> 0 <_ ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) ) |
76 |
48 49 61 75
|
sermono |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ) ` m ) <_ ( seq M ( + , ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ) ` n ) ) |
77 |
|
elfzuz |
|- ( k e. ( M ... m ) -> k e. ( ZZ>= ` M ) ) |
78 |
77 1
|
eleqtrrdi |
|- ( k e. ( M ... m ) -> k e. Z ) |
79 |
3
|
recnd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
80 |
32 78 79
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... m ) ) -> ( F ` k ) e. CC ) |
81 |
4
|
recnd |
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC ) |
82 |
32 78 81
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... m ) ) -> ( G ` k ) e. CC ) |
83 |
32 78 58
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... m ) ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) = ( ( F ` k ) - ( G ` k ) ) ) |
84 |
48 80 82 83
|
sersub |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ) ` m ) = ( ( seq M ( + , F ) ` m ) - ( seq M ( + , G ) ` m ) ) ) |
85 |
42 1
|
eleqtrdi |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> n e. ( ZZ>= ` M ) ) |
86 |
32 51 79
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. CC ) |
87 |
32 51 81
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( G ` k ) e. CC ) |
88 |
32 51 58
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ` k ) = ( ( F ` k ) - ( G ` k ) ) ) |
89 |
85 86 87 88
|
sersub |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , ( m e. Z |-> ( ( F ` m ) - ( G ` m ) ) ) ) ` n ) = ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) ) |
90 |
76 84 89
|
3brtr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , F ) ` m ) - ( seq M ( + , G ) ` m ) ) <_ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) ) |
91 |
43 44
|
resubcld |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) e. RR ) |
92 |
38 46 91
|
lesubaddd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( ( seq M ( + , F ) ` m ) - ( seq M ( + , G ) ` m ) ) <_ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) <-> ( seq M ( + , F ) ` m ) <_ ( ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) + ( seq M ( + , G ) ` m ) ) ) ) |
93 |
90 92
|
mpbid |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` m ) <_ ( ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) + ( seq M ( + , G ) ` m ) ) ) |
94 |
43
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` n ) e. CC ) |
95 |
44
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , G ) ` n ) e. CC ) |
96 |
46
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , G ) ` m ) e. CC ) |
97 |
94 95 96
|
subsubd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , F ) ` n ) - ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) = ( ( ( seq M ( + , F ) ` n ) - ( seq M ( + , G ) ` n ) ) + ( seq M ( + , G ) ` m ) ) ) |
98 |
93 97
|
breqtrrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` m ) <_ ( ( seq M ( + , F ) ` n ) - ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) ) |
99 |
38 43 47 98
|
lesubd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) <_ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) |
100 |
43 38
|
resubcld |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) e. RR ) |
101 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
102 |
101
|
ad2antlr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> x e. RR ) |
103 |
|
lelttr |
|- ( ( ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) e. RR /\ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) e. RR /\ x e. RR ) -> ( ( ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) <_ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) /\ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) < x ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) < x ) ) |
104 |
47 100 102 103
|
syl3anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) <_ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) /\ ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) < x ) -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) < x ) ) |
105 |
99 104
|
mpand |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) < x -> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) < x ) ) |
106 |
32 51 3
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. RR ) |
107 |
62 66
|
sylan2 |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ( m + 1 ) ... n ) ) -> k e. ( ZZ>= ` N ) ) |
108 |
|
0red |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 e. RR ) |
109 |
68 4
|
syldan |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( G ` k ) e. RR ) |
110 |
68 3
|
syldan |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR ) |
111 |
108 109 110 6 7
|
letrd |
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( F ` k ) ) |
112 |
32 107 111
|
syl2an2r |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ( m + 1 ) ... n ) ) -> 0 <_ ( F ` k ) ) |
113 |
48 49 106 112
|
sermono |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , F ) ` m ) <_ ( seq M ( + , F ) ` n ) ) |
114 |
38 43 113
|
abssubge0d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) = ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) |
115 |
114
|
breq1d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x <-> ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) < x ) ) |
116 |
32 51 4
|
syl2an |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( M ... n ) ) -> ( G ` k ) e. RR ) |
117 |
32 66 6
|
syl2an2r |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> 0 <_ ( G ` k ) ) |
118 |
62 117
|
sylan2 |
|- ( ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) /\ k e. ( ( m + 1 ) ... n ) ) -> 0 <_ ( G ` k ) ) |
119 |
48 49 116 118
|
sermono |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( seq M ( + , G ) ` m ) <_ ( seq M ( + , G ) ` n ) ) |
120 |
46 44 119
|
abssubge0d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) = ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) |
121 |
120
|
breq1d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x <-> ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) < x ) ) |
122 |
105 115 121
|
3imtr4d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( m e. ( ZZ>= ` N ) /\ n e. ( ZZ>= ` m ) ) ) -> ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
123 |
122
|
anassrs |
|- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( ZZ>= ` N ) ) /\ n e. ( ZZ>= ` m ) ) -> ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
124 |
123
|
adantld |
|- ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( ZZ>= ` N ) ) /\ n e. ( ZZ>= ` m ) ) -> ( ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
125 |
124
|
ralimdva |
|- ( ( ( ph /\ x e. RR+ ) /\ m e. ( ZZ>= ` N ) ) -> ( A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
126 |
125
|
reximdva |
|- ( ( ph /\ x e. RR+ ) -> ( E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
127 |
39
|
r19.29uz |
|- ( ( A. n e. ( ZZ>= ` N ) ( seq M ( + , G ) ` n ) e. CC /\ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
128 |
31 126 127
|
syl6an |
|- ( ( ph /\ x e. RR+ ) -> ( E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
129 |
128
|
ralimdva |
|- ( ph -> ( A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
130 |
1 39
|
cau4 |
|- ( N e. Z -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) ) |
131 |
2 130
|
syl |
|- ( ph -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) ) ) |
132 |
1 39
|
cau4 |
|- ( N e. Z -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
133 |
2 132
|
syl |
|- ( ph -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` N ) A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
134 |
129 131 133
|
3imtr4d |
|- ( ph -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , F ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` m ) ) ) < x ) -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
135 |
23 134
|
mpd |
|- ( ph -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
136 |
1
|
uztrn2 |
|- ( ( m e. Z /\ n e. ( ZZ>= ` m ) ) -> n e. Z ) |
137 |
|
simpr |
|- ( ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) |
138 |
27
|
biantrurd |
|- ( ( ph /\ n e. Z ) -> ( ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x <-> ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
139 |
137 138
|
syl5ib |
|- ( ( ph /\ n e. Z ) -> ( ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
140 |
136 139
|
sylan2 |
|- ( ( ph /\ ( m e. Z /\ n e. ( ZZ>= ` m ) ) ) -> ( ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
141 |
140
|
anassrs |
|- ( ( ( ph /\ m e. Z ) /\ n e. ( ZZ>= ` m ) ) -> ( ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
142 |
141
|
ralimdva |
|- ( ( ph /\ m e. Z ) -> ( A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
143 |
142
|
reximdva |
|- ( ph -> ( E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
144 |
143
|
ralimdv |
|- ( ph -> ( A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. CC /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) ) |
145 |
135 144
|
mpd |
|- ( ph -> A. x e. RR+ E. m e. Z A. n e. ( ZZ>= ` m ) ( ( seq M ( + , G ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , G ) ` n ) - ( seq M ( + , G ) ` m ) ) ) < x ) ) |
146 |
1 9 145
|
caurcvg2 |
|- ( ph -> seq M ( + , G ) e. dom ~~> ) |