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

Metamath Proof Explorer

Theorem mertenslem2

Description: Lemma for mertens . (Contributed by Mario Carneiro, 28-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 ) ) ) )
Assertion mertenslem2 
|- ( 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 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 1zzd 
 |-  ( ph -> 1 e. ZZ )
14 9 rphalfcld 
 |-  ( ph -> ( E / 2 ) e. RR+ )
15 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
16 0zd 
 |-  ( ph -> 0 e. ZZ )
17 eqidd 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( K ` j ) )
18 3 abscld 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. RR )
19 2 18 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) e. RR )
20 15 16 17 19 7 isumrecl 
 |-  ( ph -> sum_ j e. NN0 ( K ` j ) e. RR )
21 3 absge0d 
 |-  ( ( ph /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
22 21 2 breqtrrd 
 |-  ( ( ph /\ j e. NN0 ) -> 0 <_ ( K ` j ) )
23 15 16 17 19 7 22 isumge0 
 |-  ( ph -> 0 <_ sum_ j e. NN0 ( K ` j ) )
24 20 23 ge0p1rpd 
 |-  ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR+ )
25 14 24 rpdivcld 
 |-  ( ph -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR+ )
26 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( seq 0 ( + , G ) ` m ) = ( seq 0 ( + , G ) ` m ) )
27 15 16 4 5 8 isumclim2 
 |-  ( ph -> seq 0 ( + , G ) ~~> sum_ k e. NN0 B )
28 12 13 25 26 27 climi2 
 |-  ( ph -> E. s e. NN A. m e. ( ZZ>= ` s ) ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
29 eluznn 
 |-  ( ( s e. NN /\ m e. ( ZZ>= ` s ) ) -> m e. NN )
30 4 5 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) e. CC )
31 15 16 30 serf 
 |-  ( ph -> seq 0 ( + , G ) : NN0 --> CC )
32 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
33 ffvelcdm 
 |-  ( ( seq 0 ( + , G ) : NN0 --> CC /\ m e. NN0 ) -> ( seq 0 ( + , G ) ` m ) e. CC )
34 31 32 33 syl2an 
 |-  ( ( ph /\ m e. NN ) -> ( seq 0 ( + , G ) ` m ) e. CC )
35 15 16 4 5 8 isumcl 
 |-  ( ph -> sum_ k e. NN0 B e. CC )
36 35 adantr 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. NN0 B e. CC )
37 34 36 abssubd 
 |-  ( ( ph /\ m e. NN ) -> ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) = ( abs ` ( sum_ k e. NN0 B - ( seq 0 ( + , G ) ` m ) ) ) )
38 eqid 
 |-  ( ZZ>= ` ( m + 1 ) ) = ( ZZ>= ` ( m + 1 ) )
39 32 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. NN0 )
40 peano2nn0 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN0 )
41 39 40 syl 
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. NN0 )
42 41 nn0zd 
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. ZZ )
43 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> ph )
44 eluznn0 
 |-  ( ( ( m + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> k e. NN0 )
45 41 44 sylan 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> k e. NN0 )
46 43 45 4 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> ( G ` k ) = B )
47 43 45 5 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( ZZ>= ` ( m + 1 ) ) ) -> B e. CC )
48 8 adantr 
 |-  ( ( ph /\ m e. NN ) -> seq 0 ( + , G ) e. dom ~~> )
49 30 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. NN0 ) -> ( G ` k ) e. CC )
50 15 41 49 iserex 
 |-  ( ( ph /\ m e. NN ) -> ( seq 0 ( + , G ) e. dom ~~> <-> seq ( m + 1 ) ( + , G ) e. dom ~~> ) )
51 48 50 mpbid 
 |-  ( ( ph /\ m e. NN ) -> seq ( m + 1 ) ( + , G ) e. dom ~~> )
52 38 42 46 47 51 isumcl 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( ZZ>= ` ( m + 1 ) ) B e. CC )
53 34 52 pncan2d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( seq 0 ( + , G ) ` m ) + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) - ( seq 0 ( + , G ) ` m ) ) = sum_ k e. ( ZZ>= ` ( m + 1 ) ) B )
54 4 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. NN0 ) -> ( G ` k ) = B )
55 5 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. NN0 ) -> B e. CC )
56 15 38 41 54 55 48 isumsplit 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. NN0 B = ( sum_ k e. ( 0 ... ( ( m + 1 ) - 1 ) ) B + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) )
57 nncn 
 |-  ( m e. NN -> m e. CC )
58 57 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
59 ax-1cn 
 |-  1 e. CC
60 pncan 
 |-  ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
61 58 59 60 sylancl 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) - 1 ) = m )
62 61 oveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( 0 ... ( ( m + 1 ) - 1 ) ) = ( 0 ... m ) )
63 62 sumeq1d 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 0 ... ( ( m + 1 ) - 1 ) ) B = sum_ k e. ( 0 ... m ) B )
64 simpl 
 |-  ( ( ph /\ m e. NN ) -> ph )
65 elfznn0 
 |-  ( k e. ( 0 ... m ) -> k e. NN0 )
66 64 65 4 syl2an 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... m ) ) -> ( G ` k ) = B )
67 39 15 eleqtrdi 
 |-  ( ( ph /\ m e. NN ) -> m e. ( ZZ>= ` 0 ) )
68 64 65 5 syl2an 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... m ) ) -> B e. CC )
69 66 67 68 fsumser 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 0 ... m ) B = ( seq 0 ( + , G ) ` m ) )
70 63 69 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 0 ... ( ( m + 1 ) - 1 ) ) B = ( seq 0 ( + , G ) ` m ) )
71 70 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( sum_ k e. ( 0 ... ( ( m + 1 ) - 1 ) ) B + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) = ( ( seq 0 ( + , G ) ` m ) + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) )
72 56 71 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. NN0 B = ( ( seq 0 ( + , G ) ` m ) + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) )
73 72 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( sum_ k e. NN0 B - ( seq 0 ( + , G ) ` m ) ) = ( ( ( seq 0 ( + , G ) ` m ) + sum_ k e. ( ZZ>= ` ( m + 1 ) ) B ) - ( seq 0 ( + , G ) ` m ) ) )
74 46 sumeq2dv 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( m + 1 ) ) B )
75 53 73 74 3eqtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( sum_ k e. NN0 B - ( seq 0 ( + , G ) ` m ) ) = sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) )
76 75 fveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( abs ` ( sum_ k e. NN0 B - ( seq 0 ( + , G ) ` m ) ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) )
77 37 76 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) )
78 77 breq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
79 29 78 sylan2 
 |-  ( ( ph /\ ( s e. NN /\ m e. ( ZZ>= ` s ) ) ) -> ( ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
80 79 anassrs 
 |-  ( ( ( ph /\ s e. NN ) /\ m e. ( ZZ>= ` s ) ) -> ( ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
81 80 ralbidva 
 |-  ( ( ph /\ s e. NN ) -> ( A. m e. ( ZZ>= ` s ) ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> A. m e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
82 fvoveq1 
 |-  ( m = n -> ( ZZ>= ` ( m + 1 ) ) = ( ZZ>= ` ( n + 1 ) ) )
83 82 sumeq1d 
 |-  ( m = n -> sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) )
84 83 fveq2d 
 |-  ( m = n -> ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
85 84 breq1d 
 |-  ( m = n -> ( ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
86 85 cbvralvw 
 |-  ( A. m e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( m + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
87 81 86 bitrdi 
 |-  ( ( ph /\ s e. NN ) -> ( A. m e. ( ZZ>= ` s ) ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
88 0zd 
 |-  ( ( ph /\ ps ) -> 0 e. ZZ )
89 14 adantr 
 |-  ( ( ph /\ ps ) -> ( E / 2 ) e. RR+ )
90 11 simplbi 
 |-  ( ps -> s e. NN )
91 90 adantl 
 |-  ( ( ph /\ ps ) -> s e. NN )
92 91 nnrpd 
 |-  ( ( ph /\ ps ) -> s e. RR+ )
93 89 92 rpdivcld 
 |-  ( ( ph /\ ps ) -> ( ( E / 2 ) / s ) e. RR+ )
94 eqid 
 |-  ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( n + 1 ) )
95 elfznn0 
 |-  ( n e. ( 0 ... ( s - 1 ) ) -> n e. NN0 )
96 95 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> n e. NN0 )
97 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
98 96 97 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> ( n + 1 ) e. NN0 )
99 98 nn0zd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> ( n + 1 ) e. ZZ )
100 eqidd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) /\ k e. ( ZZ>= ` ( n + 1 ) ) ) -> ( G ` k ) = ( G ` k ) )
101 simplll 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) /\ k e. ( ZZ>= ` ( n + 1 ) ) ) -> ph )
102 eluznn0 
 |-  ( ( ( n + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( n + 1 ) ) ) -> k e. NN0 )
103 98 102 sylan 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) /\ k e. ( ZZ>= ` ( n + 1 ) ) ) -> k e. NN0 )
104 101 103 30 syl2anc 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) /\ k e. ( ZZ>= ` ( n + 1 ) ) ) -> ( G ` k ) e. CC )
105 8 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> seq 0 ( + , G ) e. dom ~~> )
106 30 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) /\ k e. NN0 ) -> ( G ` k ) e. CC )
107 15 98 106 iserex 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> ( seq 0 ( + , G ) e. dom ~~> <-> seq ( n + 1 ) ( + , G ) e. dom ~~> ) )
108 105 107 mpbid 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> seq ( n + 1 ) ( + , G ) e. dom ~~> )
109 94 99 100 104 108 isumcl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) e. CC )
110 109 abscld 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) e. RR )
111 eleq1a 
 |-  ( ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) e. RR -> ( z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) -> z e. RR ) )
112 110 111 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( 0 ... ( s - 1 ) ) ) -> ( z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) -> z e. RR ) )
113 112 rexlimdva 
 |-  ( ( ph /\ ps ) -> ( E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) -> z e. RR ) )
114 113 abssdv 
 |-  ( ( ph /\ ps ) -> { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) } C_ RR )
115 10 114 eqsstrid 
 |-  ( ( ph /\ ps ) -> T C_ RR )
116 fzfid 
 |-  ( ( ph /\ ps ) -> ( 0 ... ( s - 1 ) ) e. Fin )
117 abrexfi 
 |-  ( ( 0 ... ( s - 1 ) ) e. Fin -> { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) } e. Fin )
118 116 117 syl 
 |-  ( ( ph /\ ps ) -> { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) } e. Fin )
119 10 118 eqeltrid 
 |-  ( ( ph /\ ps ) -> T e. Fin )
120 nnm1nn0 
 |-  ( s e. NN -> ( s - 1 ) e. NN0 )
121 91 120 syl 
 |-  ( ( ph /\ ps ) -> ( s - 1 ) e. NN0 )
122 121 15 eleqtrdi 
 |-  ( ( ph /\ ps ) -> ( s - 1 ) e. ( ZZ>= ` 0 ) )
123 eluzfz1 
 |-  ( ( s - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( s - 1 ) ) )
124 122 123 syl 
 |-  ( ( ph /\ ps ) -> 0 e. ( 0 ... ( s - 1 ) ) )
125 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
126 125 4 sylan2 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) = B )
127 126 sumeq2dv 
 |-  ( ph -> sum_ k e. NN ( G ` k ) = sum_ k e. NN B )
128 127 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. NN ( G ` k ) = sum_ k e. NN B )
129 128 fveq2d 
 |-  ( ( ph /\ ps ) -> ( abs ` sum_ k e. NN ( G ` k ) ) = ( abs ` sum_ k e. NN B ) )
130 129 eqcomd 
 |-  ( ( ph /\ ps ) -> ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. NN ( G ` k ) ) )
131 fv0p1e1 
 |-  ( n = 0 -> ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` 1 ) )
132 131 12 eqtr4di 
 |-  ( n = 0 -> ( ZZ>= ` ( n + 1 ) ) = NN )
133 132 sumeq1d 
 |-  ( n = 0 -> sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) = sum_ k e. NN ( G ` k ) )
134 133 fveq2d 
 |-  ( n = 0 -> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) = ( abs ` sum_ k e. NN ( G ` k ) ) )
135 134 rspceeqv 
 |-  ( ( 0 e. ( 0 ... ( s - 1 ) ) /\ ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. NN ( G ` k ) ) ) -> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
136 124 130 135 syl2anc 
 |-  ( ( ph /\ ps ) -> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
137 fvex 
 |-  ( abs ` sum_ k e. NN B ) e. _V
138 eqeq1 
 |-  ( z = ( abs ` sum_ k e. NN B ) -> ( z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
139 138 rexbidv 
 |-  ( z = ( abs ` sum_ k e. NN 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. NN B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
140 137 139 10 elab2 
 |-  ( ( abs ` sum_ k e. NN B ) e. T <-> E. n e. ( 0 ... ( s - 1 ) ) ( abs ` sum_ k e. NN B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
141 136 140 sylibr 
 |-  ( ( ph /\ ps ) -> ( abs ` sum_ k e. NN B ) e. T )
142 141 ne0d 
 |-  ( ( ph /\ ps ) -> T =/= (/) )
143 ltso 
 |-  < Or RR
144 fisupcl 
 |-  ( ( < Or RR /\ ( T e. Fin /\ T =/= (/) /\ T C_ RR ) ) -> sup ( T , RR , < ) e. T )
145 143 144 mpan 
 |-  ( ( T e. Fin /\ T =/= (/) /\ T C_ RR ) -> sup ( T , RR , < ) e. T )
146 119 142 115 145 syl3anc 
 |-  ( ( ph /\ ps ) -> sup ( T , RR , < ) e. T )
147 115 146 sseldd 
 |-  ( ( ph /\ ps ) -> sup ( T , RR , < ) e. RR )
148 0red 
 |-  ( ( ph /\ ps ) -> 0 e. RR )
149 125 5 sylan2 
 |-  ( ( ph /\ k e. NN ) -> B e. CC )
150 1nn0 
 |-  1 e. NN0
151 150 a1i 
 |-  ( ph -> 1 e. NN0 )
152 15 151 30 iserex 
 |-  ( ph -> ( seq 0 ( + , G ) e. dom ~~> <-> seq 1 ( + , G ) e. dom ~~> ) )
153 8 152 mpbid 
 |-  ( ph -> seq 1 ( + , G ) e. dom ~~> )
154 12 13 126 149 153 isumcl 
 |-  ( ph -> sum_ k e. NN B e. CC )
155 154 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. NN B e. CC )
156 155 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` sum_ k e. NN B ) e. RR )
157 155 absge0d 
 |-  ( ( ph /\ ps ) -> 0 <_ ( abs ` sum_ k e. NN B ) )
158 fimaxre2 
 |-  ( ( T C_ RR /\ T e. Fin ) -> E. z e. RR A. w e. T w <_ z )
159 115 119 158 syl2anc 
 |-  ( ( ph /\ ps ) -> E. z e. RR A. w e. T w <_ z )
160 115 142 159 141 suprubd 
 |-  ( ( ph /\ ps ) -> ( abs ` sum_ k e. NN B ) <_ sup ( T , RR , < ) )
161 148 156 147 157 160 letrd 
 |-  ( ( ph /\ ps ) -> 0 <_ sup ( T , RR , < ) )
162 147 161 ge0p1rpd 
 |-  ( ( ph /\ ps ) -> ( sup ( T , RR , < ) + 1 ) e. RR+ )
163 93 162 rpdivcld 
 |-  ( ( ph /\ ps ) -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR+ )
164 fveq2 
 |-  ( n = m -> ( K ` n ) = ( K ` m ) )
165 eqid 
 |-  ( n e. NN0 |-> ( K ` n ) ) = ( n e. NN0 |-> ( K ` n ) )
166 fvex 
 |-  ( K ` m ) e. _V
167 164 165 166 fvmpt 
 |-  ( m e. NN0 -> ( ( n e. NN0 |-> ( K ` n ) ) ` m ) = ( K ` m ) )
168 167 adantl 
 |-  ( ( ( ph /\ ps ) /\ m e. NN0 ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` m ) = ( K ` m ) )
169 nn0ex 
 |-  NN0 e. _V
170 169 mptex 
 |-  ( n e. NN0 |-> ( K ` n ) ) e. _V
171 170 a1i 
 |-  ( ph -> ( n e. NN0 |-> ( K ` n ) ) e. _V )
172 elnn0uz 
 |-  ( j e. NN0 <-> j e. ( ZZ>= ` 0 ) )
173 fveq2 
 |-  ( n = j -> ( K ` n ) = ( K ` j ) )
174 fvex 
 |-  ( K ` j ) e. _V
175 173 165 174 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) = ( K ` j ) )
176 175 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) = ( K ` j ) )
177 172 176 sylan2br 
 |-  ( ( ph /\ j e. ( ZZ>= ` 0 ) ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) = ( K ` j ) )
178 16 177 seqfeq 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( K ` n ) ) ) = seq 0 ( + , K ) )
179 178 7 eqeltrd 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( K ` n ) ) ) e. dom ~~> )
180 176 2 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) = ( abs ` A ) )
181 180 18 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) e. RR )
182 181 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( K ` n ) ) ` j ) e. CC )
183 15 16 171 179 182 serf0 
 |-  ( ph -> ( n e. NN0 |-> ( K ` n ) ) ~~> 0 )
184 183 adantr 
 |-  ( ( ph /\ ps ) -> ( n e. NN0 |-> ( K ` n ) ) ~~> 0 )
185 15 88 163 168 184 climi0 
 |-  ( ( ph /\ ps ) -> E. t e. NN0 A. m e. ( ZZ>= ` t ) ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
186 simplll 
 |-  ( ( ( ( ph /\ ps ) /\ t e. NN0 ) /\ m e. ( ZZ>= ` t ) ) -> ph )
187 eluznn0 
 |-  ( ( t e. NN0 /\ m e. ( ZZ>= ` t ) ) -> m e. NN0 )
188 187 adantll 
 |-  ( ( ( ( ph /\ ps ) /\ t e. NN0 ) /\ m e. ( ZZ>= ` t ) ) -> m e. NN0 )
189 19 22 absidd 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` ( K ` j ) ) = ( K ` j ) )
190 189 ralrimiva 
 |-  ( ph -> A. j e. NN0 ( abs ` ( K ` j ) ) = ( K ` j ) )
191 fveq2 
 |-  ( j = m -> ( K ` j ) = ( K ` m ) )
192 191 fveq2d 
 |-  ( j = m -> ( abs ` ( K ` j ) ) = ( abs ` ( K ` m ) ) )
193 192 191 eqeq12d 
 |-  ( j = m -> ( ( abs ` ( K ` j ) ) = ( K ` j ) <-> ( abs ` ( K ` m ) ) = ( K ` m ) ) )
194 193 rspccva 
 |-  ( ( A. j e. NN0 ( abs ` ( K ` j ) ) = ( K ` j ) /\ m e. NN0 ) -> ( abs ` ( K ` m ) ) = ( K ` m ) )
195 190 194 sylan 
 |-  ( ( ph /\ m e. NN0 ) -> ( abs ` ( K ` m ) ) = ( K ` m ) )
196 186 188 195 syl2anc 
 |-  ( ( ( ( ph /\ ps ) /\ t e. NN0 ) /\ m e. ( ZZ>= ` t ) ) -> ( abs ` ( K ` m ) ) = ( K ` m ) )
197 196 breq1d 
 |-  ( ( ( ( ph /\ ps ) /\ t e. NN0 ) /\ m e. ( ZZ>= ` t ) ) -> ( ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
198 197 ralbidva 
 |-  ( ( ( ph /\ ps ) /\ t e. NN0 ) -> ( A. m e. ( ZZ>= ` t ) ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
199 164 breq1d 
 |-  ( n = m -> ( ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
200 199 cbvralvw 
 |-  ( A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
201 198 200 bitr4di 
 |-  ( ( ( ph /\ ps ) /\ t e. NN0 ) -> ( A. m e. ( ZZ>= ` t ) ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
202 1 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ j e. NN0 ) -> ( F ` j ) = A )
203 2 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
204 3 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ j e. NN0 ) -> A e. CC )
205 4 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ k e. NN0 ) -> ( G ` k ) = B )
206 5 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ k e. NN0 ) -> B e. CC )
207 6 ad4ant14 
 |-  ( ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
208 7 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> seq 0 ( + , K ) e. dom ~~> )
209 8 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> seq 0 ( + , G ) e. dom ~~> )
210 9 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> E e. RR+ )
211 200 anbi2i 
 |-  ( ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) <-> ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
212 211 anbi2i 
 |-  ( ( ps /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) <-> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
213 212 biimpi 
 |-  ( ( ps /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
214 213 adantll 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
215 115 142 159 3jca 
 |-  ( ( ph /\ ps ) -> ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) )
216 161 215 jca 
 |-  ( ( ph /\ ps ) -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )
217 216 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )
218 202 203 204 205 206 207 208 209 210 10 11 214 217 mertenslem1 
 |-  ( ( ( ph /\ ps ) /\ ( t e. NN0 /\ A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) -> 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 )
219 218 expr 
 |-  ( ( ( ph /\ ps ) /\ t e. NN0 ) -> ( A. n e. ( ZZ>= ` t ) ( K ` n ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) -> 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 ) )
220 201 219 sylbid 
 |-  ( ( ( ph /\ ps ) /\ t e. NN0 ) -> ( A. m e. ( ZZ>= ` t ) ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) -> 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 ) )
221 220 rexlimdva 
 |-  ( ( ph /\ ps ) -> ( E. t e. NN0 A. m e. ( ZZ>= ` t ) ( abs ` ( K ` m ) ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) -> 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 ) )
222 185 221 mpd 
 |-  ( ( ph /\ ps ) -> 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 )
223 222 ex 
 |-  ( ph -> ( ps -> 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 ) )
224 11 223 biimtrrid 
 |-  ( 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 ) ) ) -> 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 ) )
225 224 expdimp 
 |-  ( ( 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 ) ) -> 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 ) )
226 87 225 sylbid 
 |-  ( ( ph /\ s e. NN ) -> ( A. m e. ( ZZ>= ` s ) ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) -> 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 ) )
227 226 rexlimdva 
 |-  ( ph -> ( E. s e. NN A. m e. ( ZZ>= ` s ) ( abs ` ( ( seq 0 ( + , G ) ` m ) - sum_ k e. NN0 B ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) -> 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 ) )
228 28 227 mpd 
 |-  ( 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 )