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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 imbitrid 
 |-  ( ( 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 ~~> )