Metamath Proof Explorer


Theorem cvgcmp

Description: A comparison test for convergence of a real infinite series. Exercise 3 of Gleason p. 182. (Contributed by NM, 1-May-2005) (Revised by Mario Carneiro, 24-Mar-2014)

Ref Expression
Hypotheses cvgcmp.1
|- Z = ( ZZ>= ` M )
cvgcmp.2
|- ( ph -> N e. Z )
cvgcmp.3
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
cvgcmp.4
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
cvgcmp.5
|- ( ph -> seq M ( + , F ) e. dom ~~> )
cvgcmp.6
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> 0 <_ ( G ` k ) )
cvgcmp.7
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( G ` k ) <_ ( F ` k ) )
Assertion cvgcmp
|- ( ph -> seq M ( + , G ) e. dom ~~> )

Proof

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 ~~> )