Metamath Proof Explorer

Theorem iseralt

Description: The alternating series test. If G ( k ) is a decreasing sequence that converges to 0 , then sum_ k e. Z ( -u 1 ^ k ) x. G ( k ) is a convergent series. (Note that the first term is positive if M is even, and negative if M is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -u 1 using isermulc2 .) (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 9-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 iseralt.1 
 |-  Z = ( ZZ>= ` M )
2 iseralt.2 
 |-  ( ph -> M e. ZZ )
3 iseralt.3 
 |-  ( ph -> G : Z --> RR )
4 iseralt.4 
 |-  ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
5 iseralt.5 
 |-  ( ph -> G ~~> 0 )
6 iseralt.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
7 seqex 
 |-  seq M ( + , F ) e. _V
8 7 a1i 
 |-  ( ph -> seq M ( + , F ) e. _V )
9 climrel 
 |-  Rel ~~>
10 9 brrelex1i 
 |-  ( G ~~> 0 -> G e. _V )
11 5 10 syl 
 |-  ( ph -> G e. _V )
12 eqidd 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) = ( G ` n ) )
13 3 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) e. RR )
14 13 recnd 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) e. CC )
15 1 2 11 12 14 clim0c 
 |-  ( ph -> ( G ~~> 0 <-> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x ) )
16 5 15 mpbid 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x )
17 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> j e. Z )
18 17 1 eleqtrdi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
19 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
20 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
21 18 19 20 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> j e. ( ZZ>= ` j ) )
22 peano2uz 
 |-  ( j e. ( ZZ>= ` j ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
23 2fveq3 
 |-  ( n = ( j + 1 ) -> ( abs ` ( G ` n ) ) = ( abs ` ( G ` ( j + 1 ) ) ) )
24 23 breq1d 
 |-  ( n = ( j + 1 ) -> ( ( abs ` ( G ` n ) ) < x <-> ( abs ` ( G ` ( j + 1 ) ) ) < x ) )
25 24 rspcv 
 |-  ( ( j + 1 ) e. ( ZZ>= ` j ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x -> ( abs ` ( G ` ( j + 1 ) ) ) < x ) )
26 21 22 25 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x -> ( abs ` ( G ` ( j + 1 ) ) ) < x ) )
27 eluzelz 
 |-  ( n e. ( ZZ>= ` j ) -> n e. ZZ )
28 27 ad2antll 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n e. ZZ )
29 28 zcnd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n e. CC )
30 19 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
31 30 ad2antrl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j e. ZZ )
32 31 zcnd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j e. CC )
33 29 32 subcld 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( n - j ) e. CC )
34 2cnd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 2 e. CC )
35 2ne0 
 |-  2 =/= 0
36 35 a1i 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 2 =/= 0 )
37 33 34 36 divcan2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( 2 x. ( ( n - j ) / 2 ) ) = ( n - j ) )
38 37 oveq2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) = ( j + ( n - j ) ) )
39 32 29 pncan3d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( j + ( n - j ) ) = n )
40 38 39 eqtr2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n = ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) )
41 40 adantr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> n = ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) )
42 41 fveq2d 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( seq M ( + , F ) ` n ) = ( seq M ( + , F ) ` ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) ) )
43 42 fvoveq1d 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) ) - ( seq M ( + , F ) ` j ) ) ) )
44 simpll 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ph )
45 simpl 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> j e. Z )
46 45 ad2antlr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> j e. Z )
47 simpr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( ( n - j ) / 2 ) e. ZZ )
48 28 31 zsubcld 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( n - j ) e. ZZ )
49 48 zred 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( n - j ) e. RR )
50 2rp 
 |-  2 e. RR+
51 50 a1i 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 2 e. RR+ )
52 eluzle 
 |-  ( n e. ( ZZ>= ` j ) -> j <_ n )
53 52 ad2antll 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j <_ n )
54 28 zred 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n e. RR )
55 31 zred 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> j e. RR )
56 54 55 subge0d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( 0 <_ ( n - j ) <-> j <_ n ) )
57 53 56 mpbird 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 <_ ( n - j ) )
58 49 51 57 divge0d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 <_ ( ( n - j ) / 2 ) )
59 58 adantr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> 0 <_ ( ( n - j ) / 2 ) )
60 elnn0z 
 |-  ( ( ( n - j ) / 2 ) e. NN0 <-> ( ( ( n - j ) / 2 ) e. ZZ /\ 0 <_ ( ( n - j ) / 2 ) ) )
61 47 59 60 sylanbrc 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( ( n - j ) / 2 ) e. NN0 )
62 1 2 3 4 5 6 iseraltlem3 
 |-  ( ( ph /\ j e. Z /\ ( ( n - j ) / 2 ) e. NN0 ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) /\ ( abs ` ( ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) + 1 ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) ) )
63 62 simpld 
 |-  ( ( ph /\ j e. Z /\ ( ( n - j ) / 2 ) e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
64 44 46 61 63 syl3anc 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` ( j + ( 2 x. ( ( n - j ) / 2 ) ) ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
65 43 64 eqbrtrd 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( n - j ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
66 2div2e1 
 |-  ( 2 / 2 ) = 1
67 66 oveq2i 
 |-  ( ( ( ( n - j ) + 1 ) / 2 ) - ( 2 / 2 ) ) = ( ( ( ( n - j ) + 1 ) / 2 ) - 1 )
68 peano2cn 
 |-  ( ( n - j ) e. CC -> ( ( n - j ) + 1 ) e. CC )
69 33 68 syl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - j ) + 1 ) e. CC )
70 69 34 34 36 divsubdird 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( ( n - j ) + 1 ) - 2 ) / 2 ) = ( ( ( ( n - j ) + 1 ) / 2 ) - ( 2 / 2 ) ) )
71 df-2 
 |-  2 = ( 1 + 1 )
72 71 oveq2i 
 |-  ( ( ( n - j ) + 1 ) - 2 ) = ( ( ( n - j ) + 1 ) - ( 1 + 1 ) )
73 ax-1cn 
 |-  1 e. CC
74 73 a1i 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 1 e. CC )
75 33 74 74 pnpcan2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( n - j ) + 1 ) - ( 1 + 1 ) ) = ( ( n - j ) - 1 ) )
76 72 75 eqtrid 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( n - j ) + 1 ) - 2 ) = ( ( n - j ) - 1 ) )
77 76 oveq1d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( ( n - j ) + 1 ) - 2 ) / 2 ) = ( ( ( n - j ) - 1 ) / 2 ) )
78 70 77 eqtr3d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( ( n - j ) + 1 ) / 2 ) - ( 2 / 2 ) ) = ( ( ( n - j ) - 1 ) / 2 ) )
79 67 78 eqtr3id 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) = ( ( ( n - j ) - 1 ) / 2 ) )
80 79 oveq2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) = ( 2 x. ( ( ( n - j ) - 1 ) / 2 ) ) )
81 subcl 
 |-  ( ( ( n - j ) e. CC /\ 1 e. CC ) -> ( ( n - j ) - 1 ) e. CC )
82 33 73 81 sylancl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - j ) - 1 ) e. CC )
83 82 34 36 divcan2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( 2 x. ( ( ( n - j ) - 1 ) / 2 ) ) = ( ( n - j ) - 1 ) )
84 29 32 74 sub32d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - j ) - 1 ) = ( ( n - 1 ) - j ) )
85 80 83 84 3eqtrd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) = ( ( n - 1 ) - j ) )
86 85 oveq2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) = ( j + ( ( n - 1 ) - j ) ) )
87 subcl 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( n - 1 ) e. CC )
88 29 73 87 sylancl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( n - 1 ) e. CC )
89 32 88 pncan3d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( j + ( ( n - 1 ) - j ) ) = ( n - 1 ) )
90 86 89 eqtrd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) = ( n - 1 ) )
91 90 oveq1d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) = ( ( n - 1 ) + 1 ) )
92 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
93 29 73 92 sylancl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - 1 ) + 1 ) = n )
94 91 93 eqtr2d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> n = ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) )
95 94 adantr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> n = ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) )
96 95 fveq2d 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( seq M ( + , F ) ` n ) = ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) ) )
97 96 fvoveq1d 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) ) - ( seq M ( + , F ) ` j ) ) ) )
98 simpll 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ph )
99 45 ad2antlr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> j e. Z )
100 simpr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( ( ( n - j ) + 1 ) / 2 ) e. ZZ )
101 uznn0sub 
 |-  ( n e. ( ZZ>= ` j ) -> ( n - j ) e. NN0 )
102 101 ad2antll 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( n - j ) e. NN0 )
103 nn0p1nn 
 |-  ( ( n - j ) e. NN0 -> ( ( n - j ) + 1 ) e. NN )
104 102 103 syl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - j ) + 1 ) e. NN )
105 104 nnrpd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( n - j ) + 1 ) e. RR+ )
106 105 rphalfcld 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( n - j ) + 1 ) / 2 ) e. RR+ )
107 106 rpgt0d 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 < ( ( ( n - j ) + 1 ) / 2 ) )
108 107 adantr 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> 0 < ( ( ( n - j ) + 1 ) / 2 ) )
109 elnnz 
 |-  ( ( ( ( n - j ) + 1 ) / 2 ) e. NN <-> ( ( ( ( n - j ) + 1 ) / 2 ) e. ZZ /\ 0 < ( ( ( n - j ) + 1 ) / 2 ) ) )
110 100 108 109 sylanbrc 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( ( ( n - j ) + 1 ) / 2 ) e. NN )
111 nnm1nn0 
 |-  ( ( ( ( n - j ) + 1 ) / 2 ) e. NN -> ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) e. NN0 )
112 110 111 syl 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) e. NN0 )
113 1 2 3 4 5 6 iseraltlem3 
 |-  ( ( ph /\ j e. Z /\ ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) e. NN0 ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) /\ ( abs ` ( ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) ) )
114 113 simprd 
 |-  ( ( ph /\ j e. Z /\ ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
115 98 99 112 114 syl3anc 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` ( ( j + ( 2 x. ( ( ( ( n - j ) + 1 ) / 2 ) - 1 ) ) ) + 1 ) ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
116 97 115 eqbrtrd 
 |-  ( ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) /\ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
117 zeo 
 |-  ( ( n - j ) e. ZZ -> ( ( ( n - j ) / 2 ) e. ZZ \/ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) )
118 48 117 syl 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( n - j ) / 2 ) e. ZZ \/ ( ( ( n - j ) + 1 ) / 2 ) e. ZZ ) )
119 65 116 118 mpjaodan 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( G ` ( j + 1 ) ) )
120 1 peano2uzs 
 |-  ( j e. Z -> ( j + 1 ) e. Z )
121 120 adantr 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( j + 1 ) e. Z )
122 ffvelcdm 
 |-  ( ( G : Z --> RR /\ ( j + 1 ) e. Z ) -> ( G ` ( j + 1 ) ) e. RR )
123 3 121 122 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( G ` ( j + 1 ) ) e. RR )
124 1 2 3 4 5 iseraltlem1 
 |-  ( ( ph /\ ( j + 1 ) e. Z ) -> 0 <_ ( G ` ( j + 1 ) ) )
125 121 124 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> 0 <_ ( G ` ( j + 1 ) ) )
126 123 125 absidd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( G ` ( j + 1 ) ) ) = ( G ` ( j + 1 ) ) )
127 119 126 breqtrrd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( abs ` ( G ` ( j + 1 ) ) ) )
128 127 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( abs ` ( G ` ( j + 1 ) ) ) )
129 neg1rr 
 |-  -u 1 e. RR
130 129 a1i 
 |-  ( ( ph /\ k e. Z ) -> -u 1 e. RR )
131 neg1ne0 
 |-  -u 1 =/= 0
132 131 a1i 
 |-  ( ( ph /\ k e. Z ) -> -u 1 =/= 0 )
133 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
134 133 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
135 134 adantl 
 |-  ( ( ph /\ k e. Z ) -> k e. ZZ )
136 130 132 135 reexpclzd 
 |-  ( ( ph /\ k e. Z ) -> ( -u 1 ^ k ) e. RR )
137 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
138 136 137 remulcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) e. RR )
139 6 138 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
140 1 2 139 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
141 1 uztrn2 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
142 ffvelcdm 
 |-  ( ( seq M ( + , F ) : Z --> RR /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. RR )
143 140 141 142 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , F ) ` n ) e. RR )
144 ffvelcdm 
 |-  ( ( seq M ( + , F ) : Z --> RR /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
145 140 45 144 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , F ) ` j ) e. RR )
146 143 145 resubcld 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) e. RR )
147 146 recnd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) e. CC )
148 147 abscld 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) e. RR )
149 148 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) e. RR )
150 126 123 eqeltrd 
 |-  ( ( ph /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( G ` ( j + 1 ) ) ) e. RR )
151 150 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( abs ` ( G ` ( j + 1 ) ) ) e. RR )
152 rpre 
 |-  ( x e. RR+ -> x e. RR )
153 152 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> x e. RR )
154 lelttr 
 |-  ( ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) e. RR /\ ( abs ` ( G ` ( j + 1 ) ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( abs ` ( G ` ( j + 1 ) ) ) /\ ( abs ` ( G ` ( j + 1 ) ) ) < x ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) )
155 149 151 153 154 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) <_ ( abs ` ( G ` ( j + 1 ) ) ) /\ ( abs ` ( G ` ( j + 1 ) ) ) < x ) -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) )
156 128 155 mpand 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( G ` ( j + 1 ) ) ) < x -> ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) )
157 140 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> seq M ( + , F ) : Z --> RR )
158 157 141 142 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( seq M ( + , F ) ` n ) e. RR )
159 156 158 jctild 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ n e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( G ` ( j + 1 ) ) ) < x -> ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
160 159 anassrs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ n e. ( ZZ>= ` j ) ) -> ( ( abs ` ( G ` ( j + 1 ) ) ) < x -> ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
161 160 ralrimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( ( abs ` ( G ` ( j + 1 ) ) ) < x -> A. n e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
162 26 161 syld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x -> A. n e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
163 162 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x -> E. j e. Z A. n e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
164 163 ralimdva 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( G ` n ) ) < x -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) ) )
165 16 164 mpd 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) ( ( seq M ( + , F ) ` n ) e. RR /\ ( abs ` ( ( seq M ( + , F ) ` n ) - ( seq M ( + , F ) ` j ) ) ) < x ) )
166 1 8 165 caurcvg2 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )