Metamath Proof Explorer

Theorem mertens

Description: Mertens' theorem. If A ( j ) is an absolutely convergent series and B ( k ) is convergent, then ( sum_ j e. NN0 A ( j ) x. sum_ k e. NN0 B ( k ) ) = sum_ k e. NN0 sum_ j e. ( 0 ... k ) ( A ( j ) x. B ( k - j ) ) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem . (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 ~~> )
Assertion mertens 
|- ( ph -> seq 0 ( + , H ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )

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 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 0zd 
 |-  ( ph -> 0 e. ZZ )
11 seqex 
 |-  seq 0 ( + , H ) e. _V
12 11 a1i 
 |-  ( ph -> seq 0 ( + , H ) e. _V )
13 fzfid 
 |-  ( ( ph /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
14 simpl 
 |-  ( ( ph /\ k e. NN0 ) -> ph )
15 elfznn0 
 |-  ( j e. ( 0 ... k ) -> j e. NN0 )
16 14 15 3 syl2an 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> A e. CC )
17 fveq2 
 |-  ( i = ( k - j ) -> ( G ` i ) = ( G ` ( k - j ) ) )
18 17 eleq1d 
 |-  ( i = ( k - j ) -> ( ( G ` i ) e. CC <-> ( G ` ( k - j ) ) e. CC ) )
19 4 5 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) e. CC )
20 19 ralrimiva 
 |-  ( ph -> A. k e. NN0 ( G ` k ) e. CC )
21 fveq2 
 |-  ( k = i -> ( G ` k ) = ( G ` i ) )
22 21 eleq1d 
 |-  ( k = i -> ( ( G ` k ) e. CC <-> ( G ` i ) e. CC ) )
23 22 cbvralvw 
 |-  ( A. k e. NN0 ( G ` k ) e. CC <-> A. i e. NN0 ( G ` i ) e. CC )
24 20 23 sylib 
 |-  ( ph -> A. i e. NN0 ( G ` i ) e. CC )
25 24 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> A. i e. NN0 ( G ` i ) e. CC )
26 fznn0sub 
 |-  ( j e. ( 0 ... k ) -> ( k - j ) e. NN0 )
27 26 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( k - j ) e. NN0 )
28 18 25 27 rspcdva 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( G ` ( k - j ) ) e. CC )
29 16 28 mulcld 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j e. ( 0 ... k ) ) -> ( A x. ( G ` ( k - j ) ) ) e. CC )
30 13 29 fsumcl 
 |-  ( ( ph /\ k e. NN0 ) -> sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) e. CC )
31 6 30 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( H ` k ) e. CC )
32 9 10 31 serf 
 |-  ( ph -> seq 0 ( + , H ) : NN0 --> CC )
33 32 ffvelcdmda 
 |-  ( ( ph /\ m e. NN0 ) -> ( seq 0 ( + , H ) ` m ) e. CC )
34 1 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN0 ) -> ( F ` j ) = A )
35 2 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
36 3 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN0 ) -> A e. CC )
37 4 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. NN0 ) -> ( G ` k ) = B )
38 5 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. NN0 ) -> B e. CC )
39 6 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. NN0 ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
40 7 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> seq 0 ( + , K ) e. dom ~~> )
41 8 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> seq 0 ( + , G ) e. dom ~~> )
42 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
43 fveq2 
 |-  ( l = k -> ( G ` l ) = ( G ` k ) )
44 43 cbvsumv 
 |-  sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) = sum_ k e. ( ZZ>= ` ( i + 1 ) ) ( G ` k )
45 fvoveq1 
 |-  ( i = n -> ( ZZ>= ` ( i + 1 ) ) = ( ZZ>= ` ( n + 1 ) ) )
46 45 sumeq1d 
 |-  ( i = n -> sum_ k e. ( ZZ>= ` ( i + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) )
47 44 46 eqtrid 
 |-  ( i = n -> sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) = sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) )
48 47 fveq2d 
 |-  ( i = n -> ( abs ` sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
49 48 eqeq2d 
 |-  ( i = n -> ( u = ( abs ` sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) ) <-> u = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
50 49 cbvrexvw 
 |-  ( E. i e. ( 0 ... ( s - 1 ) ) u = ( abs ` sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) ) <-> E. n e. ( 0 ... ( s - 1 ) ) u = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
51 eqeq1 
 |-  ( u = z -> ( u = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
52 51 rexbidv 
 |-  ( u = z -> ( E. n e. ( 0 ... ( s - 1 ) ) u = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
53 50 52 bitrid 
 |-  ( u = z -> ( E. i e. ( 0 ... ( s - 1 ) ) u = ( abs ` sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) ) <-> E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) ) )
54 53 cbvabv 
 |-  { u | E. i e. ( 0 ... ( s - 1 ) ) u = ( abs ` sum_ l e. ( ZZ>= ` ( i + 1 ) ) ( G ` l ) ) } = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }
55 fveq2 
 |-  ( i = j -> ( K ` i ) = ( K ` j ) )
56 55 cbvsumv 
 |-  sum_ i e. NN0 ( K ` i ) = sum_ j e. NN0 ( K ` j )
57 56 oveq1i 
 |-  ( sum_ i e. NN0 ( K ` i ) + 1 ) = ( sum_ j e. NN0 ( K ` j ) + 1 )
58 57 oveq2i 
 |-  ( ( x / 2 ) / ( sum_ i e. NN0 ( K ` i ) + 1 ) ) = ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) )
59 58 breq2i 
 |-  ( ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ i e. NN0 ( K ` i ) + 1 ) ) <-> ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
60 fveq2 
 |-  ( i = k -> ( G ` i ) = ( G ` k ) )
61 60 cbvsumv 
 |-  sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) = sum_ k e. ( ZZ>= ` ( u + 1 ) ) ( G ` k )
62 fvoveq1 
 |-  ( u = n -> ( ZZ>= ` ( u + 1 ) ) = ( ZZ>= ` ( n + 1 ) ) )
63 62 sumeq1d 
 |-  ( u = n -> sum_ k e. ( ZZ>= ` ( u + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) )
64 61 63 eqtrid 
 |-  ( u = n -> sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) = sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) )
65 64 fveq2d 
 |-  ( u = n -> ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) )
66 65 breq1d 
 |-  ( u = n -> ( ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
67 59 66 bitrid 
 |-  ( u = n -> ( ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ i e. NN0 ( K ` i ) + 1 ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
68 67 cbvralvw 
 |-  ( A. u e. ( ZZ>= ` s ) ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ i e. NN0 ( K ` i ) + 1 ) ) <-> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
69 68 anbi2i 
 |-  ( ( s e. NN /\ A. u e. ( ZZ>= ` s ) ( abs ` sum_ i e. ( ZZ>= ` ( u + 1 ) ) ( G ` i ) ) < ( ( x / 2 ) / ( sum_ i e. NN0 ( K ` i ) + 1 ) ) ) <-> ( s e. NN /\ A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( x / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) ) )
70 34 35 36 37 38 39 40 41 42 54 69 mertenslem2 
 |-  ( ( ph /\ x e. RR+ ) -> 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 ) ) < x )
71 eluznn0 
 |-  ( ( y e. NN0 /\ m e. ( ZZ>= ` y ) ) -> m e. NN0 )
72 fzfid 
 |-  ( ( ph /\ m e. NN0 ) -> ( 0 ... m ) e. Fin )
73 simpll 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ph )
74 elfznn0 
 |-  ( j e. ( 0 ... m ) -> j e. NN0 )
75 74 adantl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> j e. NN0 )
76 9 10 4 5 8 isumcl 
 |-  ( ph -> sum_ k e. NN0 B e. CC )
77 76 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. NN0 B e. CC )
78 1 3 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( F ` j ) e. CC )
79 77 78 mulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( sum_ k e. NN0 B x. ( F ` j ) ) e. CC )
80 73 75 79 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( sum_ k e. NN0 B x. ( F ` j ) ) e. CC )
81 fzfid 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( 0 ... ( m - j ) ) e. Fin )
82 simplll 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> ph )
83 74 ad2antlr 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> j e. NN0 )
84 82 83 3 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> A e. CC )
85 elfznn0 
 |-  ( k e. ( 0 ... ( m - j ) ) -> k e. NN0 )
86 85 adantl 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> k e. NN0 )
87 82 86 19 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> ( G ` k ) e. CC )
88 84 87 mulcld 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> ( A x. ( G ` k ) ) e. CC )
89 81 88 fsumcl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) e. CC )
90 72 80 89 fsumsub 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ j e. ( 0 ... m ) ( ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) = ( sum_ j e. ( 0 ... m ) ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ j e. ( 0 ... m ) sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) )
91 73 75 3 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> A e. CC )
92 76 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. NN0 B e. CC )
93 81 87 fsumcl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) e. CC )
94 91 92 93 subdid 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( A x. ( sum_ k e. NN0 B - sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) ) = ( ( A x. sum_ k e. NN0 B ) - ( A x. sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) ) )
95 eqid 
 |-  ( ZZ>= ` ( ( m - j ) + 1 ) ) = ( ZZ>= ` ( ( m - j ) + 1 ) )
96 fznn0sub 
 |-  ( j e. ( 0 ... m ) -> ( m - j ) e. NN0 )
97 96 adantl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( m - j ) e. NN0 )
98 peano2nn0 
 |-  ( ( m - j ) e. NN0 -> ( ( m - j ) + 1 ) e. NN0 )
99 97 98 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. NN0 )
100 99 nn0zd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. ZZ )
101 simplll 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
102 eluznn0 
 |-  ( ( ( ( m - j ) + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
103 99 102 sylan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
104 101 103 4 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
105 101 103 5 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> B e. CC )
106 8 ad2antrr 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> seq 0 ( + , G ) e. dom ~~> )
107 73 4 sylan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. NN0 ) -> ( G ` k ) = B )
108 73 5 sylan 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. NN0 ) -> B e. CC )
109 107 108 eqeltrd 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. NN0 ) -> ( G ` k ) e. CC )
110 9 99 109 iserex 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( seq 0 ( + , G ) e. dom ~~> <-> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> ) )
111 106 110 mpbid 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> )
112 95 100 104 105 111 isumcl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B e. CC )
113 9 95 99 107 108 106 isumsplit 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. NN0 B = ( sum_ k e. ( 0 ... ( ( ( m - j ) + 1 ) - 1 ) ) B + sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
114 97 nn0cnd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( m - j ) e. CC )
115 ax-1cn 
 |-  1 e. CC
116 pncan 
 |-  ( ( ( m - j ) e. CC /\ 1 e. CC ) -> ( ( ( m - j ) + 1 ) - 1 ) = ( m - j ) )
117 114 115 116 sylancl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( ( m - j ) + 1 ) - 1 ) = ( m - j ) )
118 117 oveq2d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( 0 ... ( ( ( m - j ) + 1 ) - 1 ) ) = ( 0 ... ( m - j ) ) )
119 118 sumeq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( 0 ... ( ( ( m - j ) + 1 ) - 1 ) ) B = sum_ k e. ( 0 ... ( m - j ) ) B )
120 82 86 4 syl2anc 
 |-  ( ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) /\ k e. ( 0 ... ( m - j ) ) ) -> ( G ` k ) = B )
121 120 sumeq2dv 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) = sum_ k e. ( 0 ... ( m - j ) ) B )
122 119 121 eqtr4d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( 0 ... ( ( ( m - j ) + 1 ) - 1 ) ) B = sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) )
123 122 oveq1d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( sum_ k e. ( 0 ... ( ( ( m - j ) + 1 ) - 1 ) ) B + sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) + sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
124 113 123 eqtrd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> sum_ k e. NN0 B = ( sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) + sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
125 93 112 124 mvrladdd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( sum_ k e. NN0 B - sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B )
126 125 oveq2d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( A x. ( sum_ k e. NN0 B - sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) ) = ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
127 3 77 mulcomd 
 |-  ( ( ph /\ j e. NN0 ) -> ( A x. sum_ k e. NN0 B ) = ( sum_ k e. NN0 B x. A ) )
128 1 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( sum_ k e. NN0 B x. ( F ` j ) ) = ( sum_ k e. NN0 B x. A ) )
129 127 128 eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( A x. sum_ k e. NN0 B ) = ( sum_ k e. NN0 B x. ( F ` j ) ) )
130 73 75 129 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( A x. sum_ k e. NN0 B ) = ( sum_ k e. NN0 B x. ( F ` j ) ) )
131 81 91 87 fsummulc2 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( A x. sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) = sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) )
132 130 131 oveq12d 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( A x. sum_ k e. NN0 B ) - ( A x. sum_ k e. ( 0 ... ( m - j ) ) ( G ` k ) ) ) = ( ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) )
133 94 126 132 3eqtr3rd 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) = ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
134 133 sumeq2dv 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ j e. ( 0 ... m ) ( ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) = sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
135 fveq2 
 |-  ( n = j -> ( F ` n ) = ( F ` j ) )
136 135 oveq2d 
 |-  ( n = j -> ( sum_ k e. NN0 B x. ( F ` n ) ) = ( sum_ k e. NN0 B x. ( F ` j ) ) )
137 eqid 
 |-  ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) = ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) )
138 ovex 
 |-  ( sum_ k e. NN0 B x. ( F ` j ) ) e. _V
139 136 137 138 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ` j ) = ( sum_ k e. NN0 B x. ( F ` j ) ) )
140 75 139 syl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ j e. ( 0 ... m ) ) -> ( ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ` j ) = ( sum_ k e. NN0 B x. ( F ` j ) ) )
141 simpr 
 |-  ( ( ph /\ m e. NN0 ) -> m e. NN0 )
142 141 9 eleqtrdi 
 |-  ( ( ph /\ m e. NN0 ) -> m e. ( ZZ>= ` 0 ) )
143 140 142 80 fsumser 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ j e. ( 0 ... m ) ( sum_ k e. NN0 B x. ( F ` j ) ) = ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) )
144 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
145 144 oveq2d 
 |-  ( n = k -> ( A x. ( G ` n ) ) = ( A x. ( G ` k ) ) )
146 fveq2 
 |-  ( n = ( k - j ) -> ( G ` n ) = ( G ` ( k - j ) ) )
147 146 oveq2d 
 |-  ( n = ( k - j ) -> ( A x. ( G ` n ) ) = ( A x. ( G ` ( k - j ) ) ) )
148 88 anasss 
 |-  ( ( ( ph /\ m e. NN0 ) /\ ( j e. ( 0 ... m ) /\ k e. ( 0 ... ( m - j ) ) ) ) -> ( A x. ( G ` k ) ) e. CC )
149 145 147 148 fsum0diag2 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ j e. ( 0 ... m ) sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) = sum_ k e. ( 0 ... m ) sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
150 simpll 
 |-  ( ( ( ph /\ m e. NN0 ) /\ k e. ( 0 ... m ) ) -> ph )
151 elfznn0 
 |-  ( k e. ( 0 ... m ) -> k e. NN0 )
152 151 adantl 
 |-  ( ( ( ph /\ m e. NN0 ) /\ k e. ( 0 ... m ) ) -> k e. NN0 )
153 150 152 6 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ k e. ( 0 ... m ) ) -> ( H ` k ) = sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) )
154 150 152 30 syl2anc 
 |-  ( ( ( ph /\ m e. NN0 ) /\ k e. ( 0 ... m ) ) -> sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) e. CC )
155 153 142 154 fsumser 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ k e. ( 0 ... m ) sum_ j e. ( 0 ... k ) ( A x. ( G ` ( k - j ) ) ) = ( seq 0 ( + , H ) ` m ) )
156 149 155 eqtrd 
 |-  ( ( ph /\ m e. NN0 ) -> sum_ j e. ( 0 ... m ) sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) = ( seq 0 ( + , H ) ` m ) )
157 143 156 oveq12d 
 |-  ( ( ph /\ m e. NN0 ) -> ( sum_ j e. ( 0 ... m ) ( sum_ k e. NN0 B x. ( F ` j ) ) - sum_ j e. ( 0 ... m ) sum_ k e. ( 0 ... ( m - j ) ) ( A x. ( G ` k ) ) ) = ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) )
158 90 134 157 3eqtr3rd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) = sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
159 158 fveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) = ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) )
160 159 breq1d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < x ) )
161 71 160 sylan2 
 |-  ( ( ph /\ ( y e. NN0 /\ m e. ( ZZ>= ` y ) ) ) -> ( ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < x ) )
162 161 anassrs 
 |-  ( ( ( ph /\ y e. NN0 ) /\ m e. ( ZZ>= ` y ) ) -> ( ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < x ) )
163 162 ralbidva 
 |-  ( ( ph /\ y e. NN0 ) -> ( A. m e. ( ZZ>= ` y ) ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> A. m e. ( ZZ>= ` y ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < x ) )
164 163 rexbidva 
 |-  ( ph -> ( E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> 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 ) ) < x ) )
165 164 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x <-> 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 ) ) < x ) )
166 70 165 mpbird 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x )
167 166 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. y e. NN0 A. m e. ( ZZ>= ` y ) ( abs ` ( ( seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ` m ) - ( seq 0 ( + , H ) ` m ) ) ) < x )
168 1 fveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` ( F ` j ) ) = ( abs ` A ) )
169 2 168 eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` ( F ` j ) ) )
170 9 10 169 78 7 abscvgcvg 
 |-  ( ph -> seq 0 ( + , F ) e. dom ~~> )
171 9 10 1 3 170 isumclim2 
 |-  ( ph -> seq 0 ( + , F ) ~~> sum_ j e. NN0 A )
172 78 ralrimiva 
 |-  ( ph -> A. j e. NN0 ( F ` j ) e. CC )
173 fveq2 
 |-  ( j = m -> ( F ` j ) = ( F ` m ) )
174 173 eleq1d 
 |-  ( j = m -> ( ( F ` j ) e. CC <-> ( F ` m ) e. CC ) )
175 174 rspccva 
 |-  ( ( A. j e. NN0 ( F ` j ) e. CC /\ m e. NN0 ) -> ( F ` m ) e. CC )
176 172 175 sylan 
 |-  ( ( ph /\ m e. NN0 ) -> ( F ` m ) e. CC )
177 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
178 177 oveq2d 
 |-  ( n = m -> ( sum_ k e. NN0 B x. ( F ` n ) ) = ( sum_ k e. NN0 B x. ( F ` m ) ) )
179 ovex 
 |-  ( sum_ k e. NN0 B x. ( F ` m ) ) e. _V
180 178 137 179 fvmpt 
 |-  ( m e. NN0 -> ( ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ` m ) = ( sum_ k e. NN0 B x. ( F ` m ) ) )
181 180 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ` m ) = ( sum_ k e. NN0 B x. ( F ` m ) ) )
182 9 10 76 171 176 181 isermulc2 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ~~> ( sum_ k e. NN0 B x. sum_ j e. NN0 A ) )
183 9 10 1 3 170 isumcl 
 |-  ( ph -> sum_ j e. NN0 A e. CC )
184 76 183 mulcomd 
 |-  ( ph -> ( sum_ k e. NN0 B x. sum_ j e. NN0 A ) = ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )
185 182 184 breqtrd 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( sum_ k e. NN0 B x. ( F ` n ) ) ) ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )
186 9 10 12 33 167 185 2clim 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( sum_ j e. NN0 A x. sum_ k e. NN0 B ) )