This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mertenslem1

Description: Lemma for mertens . (Contributed by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses mertens.1 
|- ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )
mertens.2 
|- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
mertens.3 
|- ( ( ph /\ j e. NN0 ) -> A e. CC )
mertens.4 
|- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )
mertens.5 
|- ( ( ph /\ k e. NN0 ) -> B e. CC )
mertens.6 
|- ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
mertens.7 
|- ( ph -> seq 0 ( + , K ) e. dom ~~> )
mertens.8 
|- ( ph -> seq 0 ( + , G ) e. dom ~~> )
mertens.9 
|- ( ph -> E e. RR+ )
mertens.10 
|- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }
mertens.11 
|- ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
mertens.12 
|- ( ph -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
mertens.13 
|- ( ph -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )
Assertion mertenslem1 
|- ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )

Proof

Step Hyp Ref Expression
1 mertens.1 
 |-  ( ( ph /\ j e. NN0 ) -> ( F ` j ) = A )
2 mertens.2 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
3 mertens.3 
 |-  ( ( ph /\ j e. NN0 ) -> A e. CC )
4 mertens.4 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )
5 mertens.5 
 |-  ( ( ph /\ k e. NN0 ) -> B e. CC )
6 mertens.6 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
7 mertens.7 
 |-  ( ph -> seq 0 ( + , K ) e. dom ~~> )
8 mertens.8 
 |-  ( ph -> seq 0 ( + , G ) e. dom ~~> )
9 mertens.9 
 |-  ( ph -> E e. RR+ )
10 mertens.10 
 |-  T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }
11 mertens.11 
 |-  ( ps <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
12 mertens.12 
 |-  ( ph -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
13 mertens.13 
 |-  ( ph -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )
14 12 simpld 
 |-  ( ph -> ps )
15 14 11 sylib 
 |-  ( ph -> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
16 15 simpld 
 |-  ( ph -> s e. NN )
17 16 nnnn0d 
 |-  ( ph -> s e. NN0 )
18 12 simprd 
 |-  ( ph -> ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
19 18 simpld 
 |-  ( ph -> t e. NN0 )
20 17 19 nn0addcld 
 |-  ( ph -> ( s + t ) e. NN0 )
21 fzfid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... m ) e. Fin )
22 simpl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ph )
23 elfznn0 
 |-  ( j e. ( 0 ... m ) -> j e. NN0 )
24 22 23 3 syl2an 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> A e. CC )
25 eqid 
 |-  ( ZZ>= ` ( ( m - j ) + 1 ) ) = ( ZZ>= ` ( ( m - j ) + 1 ) )
26 fznn0sub 
 |-  ( j e. ( 0 ... m ) -> ( m - j ) e. NN0 )
27 26 adantl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( m - j ) e. NN0 )
28 peano2nn0 
 |-  ( ( m - j ) e. NN0 -> ( ( m - j ) + 1 ) e. NN0 )
29 27 28 syl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. NN0 )
30 29 nn0zd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. ZZ )
31 simplll 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
32 eluznn0 
 |-  ( ( ( ( m - j ) + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
33 29 32 sylan 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
34 31 33 4 syl2anc 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
35 31 33 5 syl2anc 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> B e. CC )
36 8 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> seq 0 ( + , G ) e. dom ~~> )
37 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
38 simpll 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ph )
39 4 5 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) e. CC )
40 38 39 sylan 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. NN0 ) -> ( G ` k ) e. CC )
41 37 29 40 iserex 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( seq 0 ( + , G ) e. dom ~~> <-> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> ) )
42 36 41 mpbid 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> )
43 25 30 34 35 42 isumcl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B e. CC )
44 24 43 mulcld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. CC )
45 21 44 fsumcl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. CC )
46 45 abscld 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
47 44 abscld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
48 21 47 fsumrecl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
49 9 rpred 
 |-  ( ph -> E e. RR )
50 49 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> E e. RR )
51 21 44 fsumabs 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
52 fzfid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) e. Fin )
53 17 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. NN0 )
54 53 nn0ge0d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 0 <_ s )
55 eluzelz 
 |-  ( m e. ( ZZ>= ` ( s + t ) ) -> m e. ZZ )
56 55 adantl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ZZ )
57 56 zred 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. RR )
58 53 nn0red 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. RR )
59 57 58 subge02d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 <_ s <-> ( m - s ) <_ m ) )
60 54 59 mpbid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) <_ m )
61 53 37 eleqtrdi 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ( ZZ>= ` 0 ) )
62 16 nnzd 
 |-  ( ph -> s e. ZZ )
63 uzid 
 |-  ( s e. ZZ -> s e. ( ZZ>= ` s ) )
64 62 63 syl 
 |-  ( ph -> s e. ( ZZ>= ` s ) )
65 uzaddcl 
 |-  ( ( s e. ( ZZ>= ` s ) /\ t e. NN0 ) -> ( s + t ) e. ( ZZ>= ` s ) )
66 64 19 65 syl2anc 
 |-  ( ph -> ( s + t ) e. ( ZZ>= ` s ) )
67 eqid 
 |-  ( ZZ>= ` s ) = ( ZZ>= ` s )
68 67 uztrn2 
 |-  ( ( ( s + t ) e. ( ZZ>= ` s ) /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` s ) )
69 66 68 sylan 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` s ) )
70 elfzuzb 
 |-  ( s e. ( 0 ... m ) <-> ( s e. ( ZZ>= ` 0 ) /\ m e. ( ZZ>= ` s ) ) )
71 61 69 70 sylanbrc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ( 0 ... m ) )
72 fznn0sub2 
 |-  ( s e. ( 0 ... m ) -> ( m - s ) e. ( 0 ... m ) )
73 71 72 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ( 0 ... m ) )
74 elfzelz 
 |-  ( ( m - s ) e. ( 0 ... m ) -> ( m - s ) e. ZZ )
75 73 74 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ZZ )
76 eluz 
 |-  ( ( ( m - s ) e. ZZ /\ m e. ZZ ) -> ( m e. ( ZZ>= ` ( m - s ) ) <-> ( m - s ) <_ m ) )
77 75 56 76 syl2anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m e. ( ZZ>= ` ( m - s ) ) <-> ( m - s ) <_ m ) )
78 60 77 mpbird 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` ( m - s ) ) )
79 fzss2 
 |-  ( m e. ( ZZ>= ` ( m - s ) ) -> ( 0 ... ( m - s ) ) C_ ( 0 ... m ) )
80 78 79 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) C_ ( 0 ... m ) )
81 80 sselda 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. ( 0 ... m ) )
82 3 abscld 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. RR )
83 22 23 82 syl2an 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` A ) e. RR )
84 43 abscld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
85 83 84 remulcld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
86 81 85 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
87 52 86 fsumrecl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
88 fzfid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( m - s ) + 1 ) ... m ) e. Fin )
89 elfznn0 
 |-  ( ( m - s ) e. ( 0 ... m ) -> ( m - s ) e. NN0 )
90 73 89 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. NN0 )
91 peano2nn0 
 |-  ( ( m - s ) e. NN0 -> ( ( m - s ) + 1 ) e. NN0 )
92 90 91 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. NN0 )
93 92 37 eleqtrdi 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` 0 ) )
94 fzss1 
 |-  ( ( ( m - s ) + 1 ) e. ( ZZ>= ` 0 ) -> ( ( ( m - s ) + 1 ) ... m ) C_ ( 0 ... m ) )
95 93 94 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( m - s ) + 1 ) ... m ) C_ ( 0 ... m ) )
96 95 sselda 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. ( 0 ... m ) )
97 96 85 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
98 88 97 fsumrecl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
99 9 rphalfcld 
 |-  ( ph -> ( E / 2 ) e. RR+ )
100 99 rpred 
 |-  ( ph -> ( E / 2 ) e. RR )
101 100 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( E / 2 ) e. RR )
102 elfznn0 
 |-  ( j e. ( 0 ... ( m - s ) ) -> j e. NN0 )
103 22 102 82 syl2an 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` A ) e. RR )
104 52 103 fsumrecl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) e. RR )
105 104 101 remulcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) e. RR )
106 0zd 
 |-  ( ph -> 0 e. ZZ )
107 eqidd 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( K ` j ) )
108 2 82 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) e. RR )
109 37 106 107 108 7 isumrecl 
 |-  ( ph -> sum_ j e. NN0 ( K ` j ) e. RR )
110 3 absge0d 
 |-  ( ( ph /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
111 110 2 breqtrrd 
 |-  ( ( ph /\ j e. NN0 ) -> 0 <_ ( K ` j ) )
112 37 106 107 108 7 111 isumge0 
 |-  ( ph -> 0 <_ sum_ j e. NN0 ( K ` j ) )
113 109 112 ge0p1rpd 
 |-  ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR+ )
114 113 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR+ )
115 105 114 rerpdivcld 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR )
116 99 113 rpdivcld 
 |-  ( ph -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR+ )
117 116 rpred 
 |-  ( ph -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR )
118 117 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR )
119 103 118 remulcld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) e. RR )
120 81 30 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) + 1 ) e. ZZ )
121 simplll 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
122 81 29 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) + 1 ) e. NN0 )
123 122 32 sylan 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
124 121 123 4 syl2anc 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
125 121 123 5 syl2anc 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> B e. CC )
126 81 42 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> )
127 25 120 124 125 126 isumcl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B e. CC )
128 127 abscld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
129 82 110 jca 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
130 22 102 129 syl2an 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
131 124 sumeq2dv 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B )
132 131 fveq2d 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
133 fvoveq1 
 |-  ( n = ( m - j ) -> ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( ( m - j ) + 1 ) ) )
134 133 sumeq1d 
 |-  ( n = ( m - j ) -> sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) )
135 134 fveq2d 
 |-  ( n = ( m - j ) -> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) )
136 135 breq1d 
 |-  ( n = ( m - j ) -> ( ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
137 15 simprd 
 |-  ( ph -> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
138 137 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
139 elfzelz 
 |-  ( j e. ( 0 ... ( m - s ) ) -> j e. ZZ )
140 139 adantl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. ZZ )
141 140 zred 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. RR )
142 55 ad2antlr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> m e. ZZ )
143 142 zred 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> m e. RR )
144 62 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s e. ZZ )
145 144 zred 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s e. RR )
146 elfzle2 
 |-  ( j e. ( 0 ... ( m - s ) ) -> j <_ ( m - s ) )
147 146 adantl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j <_ ( m - s ) )
148 141 143 145 147 lesubd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s <_ ( m - j ) )
149 142 140 zsubcld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( m - j ) e. ZZ )
150 eluz 
 |-  ( ( s e. ZZ /\ ( m - j ) e. ZZ ) -> ( ( m - j ) e. ( ZZ>= ` s ) <-> s <_ ( m - j ) ) )
151 144 149 150 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) e. ( ZZ>= ` s ) <-> s <_ ( m - j ) ) )
152 148 151 mpbird 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( m - j ) e. ( ZZ>= ` s ) )
153 136 138 152 rspcdva 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
154 132 153 eqbrtrrd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
155 128 118 154 ltled 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
156 lemul2a 
 |-  ( ( ( ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR /\ ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) /\ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
157 128 118 130 155 156 syl31anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
158 52 86 119 157 fsumle 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
159 104 recnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) e. CC )
160 99 rpcnd 
 |-  ( ph -> ( E / 2 ) e. CC )
161 160 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( E / 2 ) e. CC )
162 peano2re 
 |-  ( sum_ j e. NN0 ( K ` j ) e. RR -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
163 109 162 syl 
 |-  ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
164 163 recnd 
 |-  ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. CC )
165 164 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. CC )
166 113 rpne0d 
 |-  ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) =/= 0 )
167 166 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) =/= 0 )
168 159 161 165 167 divassd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) = ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
169 fveq2 
 |-  ( n = j -> ( K ` n ) = ( K ` j ) )
170 169 cbvsumv 
 |-  sum_ n e. NN0 ( K ` n ) = sum_ j e. NN0 ( K ` j )
171 170 oveq1i 
 |-  ( sum_ n e. NN0 ( K ` n ) + 1 ) = ( sum_ j e. NN0 ( K ` j ) + 1 )
172 171 oveq2i 
 |-  ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) = ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) )
173 172 116 eqeltrid 
 |-  ( ph -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. RR+ )
174 173 rpcnd 
 |-  ( ph -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. CC )
175 174 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. CC )
176 82 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. CC )
177 22 102 176 syl2an 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` A ) e. CC )
178 52 175 177 fsummulc1 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) )
179 172 oveq2i 
 |-  ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
180 172 oveq2i 
 |-  ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
181 180 a1i 
 |-  ( j e. ( 0 ... ( m - s ) ) -> ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
182 181 sumeq2i 
 |-  sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
183 178 179 182 3eqtr3g 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) = sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
184 168 183 eqtrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) = sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
185 158 184 breqtrrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
186 109 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) e. RR )
187 163 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
188 0zd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 0 e. ZZ )
189 fz0ssnn0 
 |-  ( 0 ... ( m - s ) ) C_ NN0
190 189 a1i 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) C_ NN0 )
191 2 adantlr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
192 82 adantlr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> ( abs ` A ) e. RR )
193 110 adantlr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
194 7 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> seq 0 ( + , K ) e. dom ~~> )
195 37 188 52 190 191 192 193 194 isumless 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) <_ sum_ j e. NN0 ( abs ` A ) )
196 2 sumeq2dv 
 |-  ( ph -> sum_ j e. NN0 ( K ` j ) = sum_ j e. NN0 ( abs ` A ) )
197 196 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) = sum_ j e. NN0 ( abs ` A ) )
198 195 197 breqtrrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) <_ sum_ j e. NN0 ( K ` j ) )
199 109 ltp1d 
 |-  ( ph -> sum_ j e. NN0 ( K ` j ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
200 199 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
201 104 186 187 198 200 lelttrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
202 99 rpregt0d 
 |-  ( ph -> ( ( E / 2 ) e. RR /\ 0 < ( E / 2 ) ) )
203 202 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) e. RR /\ 0 < ( E / 2 ) ) )
204 ltmul1 
 |-  ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) e. RR /\ ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ ( ( E / 2 ) e. RR /\ 0 < ( E / 2 ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) <-> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) < ( ( sum_ j e. NN0 ( K ` j ) + 1 ) x. ( E / 2 ) ) ) )
205 104 187 203 204 syl3anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) <-> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) < ( ( sum_ j e. NN0 ( K ` j ) + 1 ) x. ( E / 2 ) ) ) )
206 201 205 mpbid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) < ( ( sum_ j e. NN0 ( K ` j ) + 1 ) x. ( E / 2 ) ) )
207 113 rpregt0d 
 |-  ( ph -> ( ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ 0 < ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
208 207 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ 0 < ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
209 ltdivmul 
 |-  ( ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) e. RR /\ ( E / 2 ) e. RR /\ ( ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ 0 < ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) -> ( ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) < ( E / 2 ) <-> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) < ( ( sum_ j e. NN0 ( K ` j ) + 1 ) x. ( E / 2 ) ) ) )
210 105 101 208 209 syl3anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) < ( E / 2 ) <-> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) < ( ( sum_ j e. NN0 ( K ` j ) + 1 ) x. ( E / 2 ) ) ) )
211 206 210 mpbird 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) < ( E / 2 ) )
212 87 115 101 185 211 lelttrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < ( E / 2 ) )
213 13 simprd 
 |-  ( ph -> ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) )
214 suprcl 
 |-  ( ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) -> sup ( T , RR , < ) e. RR )
215 213 214 syl 
 |-  ( ph -> sup ( T , RR , < ) e. RR )
216 100 215 remulcld 
 |-  ( ph -> ( ( E / 2 ) x. sup ( T , RR , < ) ) e. RR )
217 13 simpld 
 |-  ( ph -> 0 <_ sup ( T , RR , < ) )
218 215 217 ge0p1rpd 
 |-  ( ph -> ( sup ( T , RR , < ) + 1 ) e. RR+ )
219 216 218 rerpdivcld 
 |-  ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
220 219 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
221 16 nnrpd 
 |-  ( ph -> s e. RR+ )
222 99 221 rpdivcld 
 |-  ( ph -> ( ( E / 2 ) / s ) e. RR+ )
223 222 218 rpdivcld 
 |-  ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR+ )
224 223 rpred 
 |-  ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
225 224 215 remulcld 
 |-  ( ph -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. RR )
226 225 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. RR )
227 simpll 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ph )
228 96 23 syl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. NN0 )
229 227 228 82 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) e. RR )
230 224 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
231 227 228 2 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( K ` j ) = ( abs ` A ) )
232 fveq2 
 |-  ( m = j -> ( K ` m ) = ( K ` j ) )
233 232 breq1d 
 |-  ( m = j -> ( ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> ( K ` j ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
234 18 simprd 
 |-  ( ph -> A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
235 234 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
236 elfzuz 
 |-  ( j e. ( ( ( m - s ) + 1 ) ... m ) -> j e. ( ZZ>= ` ( ( m - s ) + 1 ) ) )
237 eluzle 
 |-  ( m e. ( ZZ>= ` ( s + t ) ) -> ( s + t ) <_ m )
238 237 adantl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( s + t ) <_ m )
239 19 nn0zd 
 |-  ( ph -> t e. ZZ )
240 239 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t e. ZZ )
241 240 zred 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t e. RR )
242 58 241 57 leaddsub2d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( s + t ) <_ m <-> t <_ ( m - s ) ) )
243 238 242 mpbid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t <_ ( m - s ) )
244 eluz 
 |-  ( ( t e. ZZ /\ ( m - s ) e. ZZ ) -> ( ( m - s ) e. ( ZZ>= ` t ) <-> t <_ ( m - s ) ) )
245 240 75 244 syl2anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) e. ( ZZ>= ` t ) <-> t <_ ( m - s ) ) )
246 243 245 mpbird 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ( ZZ>= ` t ) )
247 peano2uz 
 |-  ( ( m - s ) e. ( ZZ>= ` t ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) )
248 246 247 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) )
249 uztrn 
 |-  ( ( j e. ( ZZ>= ` ( ( m - s ) + 1 ) ) /\ ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) ) -> j e. ( ZZ>= ` t ) )
250 236 248 249 syl2anr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. ( ZZ>= ` t ) )
251 233 235 250 rspcdva 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( K ` j ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
252 231 251 eqbrtrrd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
253 229 230 252 ltled 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) <_ ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
254 213 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) )
255 57 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> m e. RR )
256 peano2zm 
 |-  ( s e. ZZ -> ( s - 1 ) e. ZZ )
257 62 256 syl 
 |-  ( ph -> ( s - 1 ) e. ZZ )
258 257 zred 
 |-  ( ph -> ( s - 1 ) e. RR )
259 258 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( s - 1 ) e. RR )
260 228 nn0red 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. RR )
261 56 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. CC )
262 58 recnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. CC )
263 1cnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 1 e. CC )
264 261 262 263 subsubd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - ( s - 1 ) ) = ( ( m - s ) + 1 ) )
265 264 adantr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - ( s - 1 ) ) = ( ( m - s ) + 1 ) )
266 elfzle1 
 |-  ( j e. ( ( ( m - s ) + 1 ) ... m ) -> ( ( m - s ) + 1 ) <_ j )
267 266 adantl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( m - s ) + 1 ) <_ j )
268 265 267 eqbrtrd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - ( s - 1 ) ) <_ j )
269 255 259 260 268 subled 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) <_ ( s - 1 ) )
270 96 26 syl 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. NN0 )
271 270 37 eleqtrdi 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. ( ZZ>= ` 0 ) )
272 257 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( s - 1 ) e. ZZ )
273 elfz5 
 |-  ( ( ( m - j ) e. ( ZZ>= ` 0 ) /\ ( s - 1 ) e. ZZ ) -> ( ( m - j ) e. ( 0 ... ( s - 1 ) ) <-> ( m - j ) <_ ( s - 1 ) ) )
274 271 272 273 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( m - j ) e. ( 0 ... ( s - 1 ) ) <-> ( m - j ) <_ ( s - 1 ) ) )
275 269 274 mpbird 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. ( 0 ... ( s - 1 ) ) )
276 simplll 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
277 96 29 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( m - j ) + 1 ) e. NN0 )
278 277 32 sylan 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
279 276 278 4 syl2anc 
 |-  ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
280 279 sumeq2dv 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B )
281 280 eqcomd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) )
282 281 fveq2d 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) )
283 135 rspceeqv 
 |-  ( ( ( m - j ) e. ( 0 ... ( s - 1 ) ) /\ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) ) -> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
284 275 282 283 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
285 fvex 
 |-  ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. _V
286 eqeq1 
 |-  ( z = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) -> ( z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
287 286 rexbidv 
 |-  ( z = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) -> ( E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
288 285 287 10 elab2 
 |-  ( ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. T <-> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
289 284 288 sylibr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. T )
290 suprub 
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) /\ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. T ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ sup ( T , RR , < ) )
291 254 289 290 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ sup ( T , RR , < ) )
292 227 228 129 syl2anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
293 96 84 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
294 43 absge0d 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
295 96 294 syldan 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
296 293 295 jca 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR /\ 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
297 215 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> sup ( T , RR , < ) e. RR )
298 lemul12a 
 |-  ( ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR ) /\ ( ( ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR /\ 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) /\ sup ( T , RR , < ) e. RR ) ) -> ( ( ( abs ` A ) <_ ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) /\ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ sup ( T , RR , < ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
299 292 230 296 297 298 syl22anc 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( ( abs ` A ) <_ ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) /\ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ sup ( T , RR , < ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
300 253 291 299 mp2and 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
301 88 97 226 300 fsumle 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
302 225 recnd 
 |-  ( ph -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. CC )
303 302 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. CC )
304 fsumconst 
 |-  ( ( ( ( ( m - s ) + 1 ) ... m ) e. Fin /\ ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. CC ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) = ( ( # ` ( ( ( m - s ) + 1 ) ... m ) ) x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
305 88 303 304 syl2anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) = ( ( # ` ( ( ( m - s ) + 1 ) ... m ) ) x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
306 1zzd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 1 e. ZZ )
307 62 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ZZ )
308 fzen 
 |-  ( ( 1 e. ZZ /\ s e. ZZ /\ ( m - s ) e. ZZ ) -> ( 1 ... s ) ~~ ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) )
309 306 307 75 308 syl3anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) ~~ ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) )
310 ax-1cn 
 |-  1 e. CC
311 75 zcnd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. CC )
312 addcom 
 |-  ( ( 1 e. CC /\ ( m - s ) e. CC ) -> ( 1 + ( m - s ) ) = ( ( m - s ) + 1 ) )
313 310 311 312 sylancr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 + ( m - s ) ) = ( ( m - s ) + 1 ) )
314 262 261 pncan3d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( s + ( m - s ) ) = m )
315 313 314 oveq12d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) = ( ( ( m - s ) + 1 ) ... m ) )
316 309 315 breqtrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) )
317 fzfid 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) e. Fin )
318 hashen 
 |-  ( ( ( 1 ... s ) e. Fin /\ ( ( ( m - s ) + 1 ) ... m ) e. Fin ) -> ( ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) <-> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) ) )
319 317 88 318 syl2anc 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) <-> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) ) )
320 316 319 mpbird 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) )
321 hashfz1 
 |-  ( s e. NN0 -> ( # ` ( 1 ... s ) ) = s )
322 53 321 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( 1 ... s ) ) = s )
323 320 322 eqtr3d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( ( ( m - s ) + 1 ) ... m ) ) = s )
324 323 oveq1d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( # ` ( ( ( m - s ) + 1 ) ... m ) ) x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) = ( s x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
325 215 recnd 
 |-  ( ph -> sup ( T , RR , < ) e. CC )
326 218 rpcnne0d 
 |-  ( ph -> ( ( sup ( T , RR , < ) + 1 ) e. CC /\ ( sup ( T , RR , < ) + 1 ) =/= 0 ) )
327 div23 
 |-  ( ( ( E / 2 ) e. CC /\ sup ( T , RR , < ) e. CC /\ ( ( sup ( T , RR , < ) + 1 ) e. CC /\ ( sup ( T , RR , < ) + 1 ) =/= 0 ) ) -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
328 160 325 326 327 syl3anc 
 |-  ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
329 62 zcnd 
 |-  ( ph -> s e. CC )
330 222 rpcnd 
 |-  ( ph -> ( ( E / 2 ) / s ) e. CC )
331 divass 
 |-  ( ( s e. CC /\ ( ( E / 2 ) / s ) e. CC /\ ( ( sup ( T , RR , < ) + 1 ) e. CC /\ ( sup ( T , RR , < ) + 1 ) =/= 0 ) ) -> ( ( s x. ( ( E / 2 ) / s ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
332 329 330 326 331 syl3anc 
 |-  ( ph -> ( ( s x. ( ( E / 2 ) / s ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
333 16 nnne0d 
 |-  ( ph -> s =/= 0 )
334 160 329 333 divcan2d 
 |-  ( ph -> ( s x. ( ( E / 2 ) / s ) ) = ( E / 2 ) )
335 334 oveq1d 
 |-  ( ph -> ( ( s x. ( ( E / 2 ) / s ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) )
336 332 335 eqtr3d 
 |-  ( ph -> ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) = ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) )
337 336 oveq1d 
 |-  ( ph -> ( ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) x. sup ( T , RR , < ) ) = ( ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
338 223 rpcnd 
 |-  ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. CC )
339 329 338 325 mulassd 
 |-  ( ph -> ( ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) x. sup ( T , RR , < ) ) = ( s x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) )
340 328 337 339 3eqtr2rd 
 |-  ( ph -> ( s x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) = ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) )
341 340 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( s x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) = ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) )
342 305 324 341 3eqtrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) = ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) )
343 301 342 breqtrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) <_ ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) )
344 peano2re 
 |-  ( sup ( T , RR , < ) e. RR -> ( sup ( T , RR , < ) + 1 ) e. RR )
345 215 344 syl 
 |-  ( ph -> ( sup ( T , RR , < ) + 1 ) e. RR )
346 215 ltp1d 
 |-  ( ph -> sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) )
347 215 345 99 346 ltmul2dd 
 |-  ( ph -> ( ( E / 2 ) x. sup ( T , RR , < ) ) < ( ( E / 2 ) x. ( sup ( T , RR , < ) + 1 ) ) )
348 216 100 218 ltdivmul2d 
 |-  ( ph -> ( ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) < ( E / 2 ) <-> ( ( E / 2 ) x. sup ( T , RR , < ) ) < ( ( E / 2 ) x. ( sup ( T , RR , < ) + 1 ) ) ) )
349 347 348 mpbird 
 |-  ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) < ( E / 2 ) )
350 349 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) < ( E / 2 ) )
351 98 220 101 343 350 lelttrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < ( E / 2 ) )
352 87 98 101 101 212 351 lt2addd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) + sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) ) < ( ( E / 2 ) + ( E / 2 ) ) )
353 24 43 absmuld 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) = ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
354 353 sumeq2dv 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) = sum_ j e. ( 0 ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
355 75 zred 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. RR )
356 355 ltp1d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) < ( ( m - s ) + 1 ) )
357 fzdisj 
 |-  ( ( m - s ) < ( ( m - s ) + 1 ) -> ( ( 0 ... ( m - s ) ) i^i ( ( ( m - s ) + 1 ) ... m ) ) = (/) )
358 356 357 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( 0 ... ( m - s ) ) i^i ( ( ( m - s ) + 1 ) ... m ) ) = (/) )
359 fzsplit 
 |-  ( ( m - s ) e. ( 0 ... m ) -> ( 0 ... m ) = ( ( 0 ... ( m - s ) ) u. ( ( ( m - s ) + 1 ) ... m ) ) )
360 73 359 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... m ) = ( ( 0 ... ( m - s ) ) u. ( ( ( m - s ) + 1 ) ... m ) ) )
361 85 recnd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. CC )
362 358 360 21 361 fsumsplit 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) = ( sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) + sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) ) )
363 354 362 eqtr2d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) + sum_ j e. ( ( ( m - s ) + 1 ) ... m ) ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) ) = sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
364 9 rpcnd 
 |-  ( ph -> E e. CC )
365 364 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> E e. CC )
366 365 2halvesd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) + ( E / 2 ) ) = E )
367 352 363 366 3brtr3d 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
368 46 48 50 51 367 lelttrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
369 368 ralrimiva 
 |-  ( ph -> A. m e. ( ZZ>= ` ( s + t ) ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
370 fveq2 
 |-  ( y = ( s + t ) -> ( ZZ>= ` y ) = ( ZZ>= ` ( s + t ) ) )
371 370 raleqdv 
 |-  ( y = ( s + t ) -> ( A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E <-> A. m e. ( ZZ>= ` ( s + t ) ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E ) )
372 371 rspcev 
 |-  ( ( ( s + t ) e. NN0 /\ A. m e. ( ZZ>= ` ( s + t ) ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E ) -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
373 20 369 372 syl2anc 
 |-  ( ph -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )