Theorem mertenslem1 14616

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

Hypotheses

Ref	Expression
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

Ref	Expression
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 )

Distinct variable groups:   j, m, n, s, t, y, z, B   j, k, G, m, n, s, y, z   ph, j, k, m, y, z   t, k, A, m, n, s, y   j, E, k, m, n, s, t, y, z   j, K, k, m, n, s, t, y, z   j, F, m, n, y   ps, j, k, m, n, t, y, z   w, j, T, k, m, n, t, y, z   k, H, m, y

Allowed substitution hints:   ph( w, t, n, s)   ps( w, s)   A( z, w, j)   B( w, k)   T( s)   E( w)   F( z, w, t, k, s)   G( w, t)   H( z, w, t, j, n, s)   K( w)

Proof of Theorem mertenslem1

Step	Hyp	Ref	Expression
1		mertens.12	. . . . . . 7 |- ( ph -> ( ps /\ ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) ) )
2	1	simpld 475	. . . . . 6 |- ( ph -> ps )
3		mertens.11	. . . . . 6 |- ( 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 ) ) ) )
4	2, 3	sylib 208	. . . . 5 |- ( 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 ) ) ) )
5	4	simpld 475	. . . 4 |- ( ph -> s e. NN )
6	5	nnnn0d 11351	. . 3 |- ( ph -> s e. NN0 )
7	1	simprd 479	. . . 4 |- ( ph -> ( t e. NN0 /\ A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
8	7	simpld 475	. . 3 |- ( ph -> t e. NN0 )
9	6, 8	nn0addcld 11355	. 2 |- ( ph -> ( s + t ) e. NN0 )
10		fzfid 12772	. . . . . 6 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... m ) e. Fin )
11		simpl 473	. . . . . . . 8 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ph )
12		elfznn0 12433	. . . . . . . 8 |- ( j e. ( 0 ... m ) -> j e. NN0 )
13		mertens.3	. . . . . . . 8 |- ( ( ph /\ j e. NN0 ) -> A e. CC )
14	11, 12, 13	syl2an 494	. . . . . . 7 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> A e. CC )
15		eqid 2622	. . . . . . . 8 |- ( ZZ>= ` ( ( m - j ) + 1 ) ) = ( ZZ>= ` ( ( m - j ) + 1 ) )
16		fznn0sub 12373	. . . . . . . . . . 11 |- ( j e. ( 0 ... m ) -> ( m - j ) e. NN0 )
17	16	adantl 482	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( m - j ) e. NN0 )
18		peano2nn0 11333	. . . . . . . . . 10 |- ( ( m - j ) e. NN0 -> ( ( m - j ) + 1 ) e. NN0 )
19	17, 18	syl 17	. . . . . . . . 9 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. NN0 )
20	19	nn0zd 11480	. . . . . . . 8 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( m - j ) + 1 ) e. ZZ )
21		simplll 798	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
22		eluznn0 11757	. . . . . . . . . 10 |- ( ( ( ( m - j ) + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
23	19, 22	sylan 488	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
24		mertens.4	. . . . . . . . 9 |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) = B )
25	21, 23, 24	syl2anc 693	. . . . . . . 8 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
26		mertens.5	. . . . . . . . 9 |- ( ( ph /\ k e. NN0 ) -> B e. CC )
27	21, 23, 26	syl2anc 693	. . . . . . . 8 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> B e. CC )
28		mertens.8	. . . . . . . . . 10 |- ( ph -> seq 0 ( + , G ) e. dom ~~> )
29	28	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> seq 0 ( + , G ) e. dom ~~> )
30		nn0uz 11722	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` 0 )
31		simpll 790	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ph )
32	24, 26	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN0 ) -> ( G ` k ) e. CC )
33	31, 32	sylan 488	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) /\ k e. NN0 ) -> ( G ` k ) e. CC )
34	30, 19, 33	iserex 14387	. . . . . . . . 9 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( seq 0 ( + , G ) e. dom ~~> <-> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> ) )
35	29, 34	mpbid 222	. . . . . . . 8 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> )
36	15, 20, 25, 27, 35	isumcl 14492	. . . . . . 7 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B e. CC )
37	14, 36	mulcld 10060	. . . . . 6 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. CC )
38	10, 37	fsumcl 14464	. . . . 5 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. CC )
39	38	abscld 14175	. . . 4 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
40	37	abscld 14175	. . . . 5 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
41	10, 40	fsumrecl 14465	. . . 4 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
42		mertens.9	. . . . . 6 |- ( ph -> E e. RR+ )
43	42	rpred 11872	. . . . 5 |- ( ph -> E e. RR )
44	43	adantr 481	. . . 4 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> E e. RR )
45	10, 37	fsumabs 14533	. . . 4 |- ( ( 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 ) ) )
46		fzfid 12772	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) e. Fin )
47	6	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. NN0 )
48	47	nn0ge0d 11354	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 0 <_ s )
49		eluzelz 11697	. . . . . . . . . . . . . . 15 |- ( m e. ( ZZ>= ` ( s + t ) ) -> m e. ZZ )
50	49	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ZZ )
51	50	zred 11482	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. RR )
52	47	nn0red 11352	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. RR )
53	51, 52	subge02d 10619	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 <_ s <-> ( m - s ) <_ m ) )
54	48, 53	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) <_ m )
55	47, 30	syl6eleq 2711	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ( ZZ>= ` 0 ) )
56	5	nnzd 11481	. . . . . . . . . . . . . . . . . 18 |- ( ph -> s e. ZZ )
57		uzid 11702	. . . . . . . . . . . . . . . . . 18 |- ( s e. ZZ -> s e. ( ZZ>= ` s ) )
58	56, 57	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> s e. ( ZZ>= ` s ) )
59		uzaddcl 11744	. . . . . . . . . . . . . . . . 17 |- ( ( s e. ( ZZ>= ` s ) /\ t e. NN0 ) -> ( s + t ) e. ( ZZ>= ` s ) )
60	58, 8, 59	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ph -> ( s + t ) e. ( ZZ>= ` s ) )
61		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( ZZ>= ` s ) = ( ZZ>= ` s )
62	61	uztrn2 11705	. . . . . . . . . . . . . . . 16 |- ( ( ( s + t ) e. ( ZZ>= ` s ) /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` s ) )
63	60, 62	sylan 488	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` s ) )
64		elfzuzb 12336	. . . . . . . . . . . . . . 15 |- ( s e. ( 0 ... m ) <-> ( s e. ( ZZ>= ` 0 ) /\ m e. ( ZZ>= ` s ) ) )
65	55, 63, 64	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ( 0 ... m ) )
66		fznn0sub2 12446	. . . . . . . . . . . . . 14 |- ( s e. ( 0 ... m ) -> ( m - s ) e. ( 0 ... m ) )
67	65, 66	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ( 0 ... m ) )
68		elfzelz 12342	. . . . . . . . . . . . 13 |- ( ( m - s ) e. ( 0 ... m ) -> ( m - s ) e. ZZ )
69	67, 68	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ZZ )
70		eluz 11701	. . . . . . . . . . . 12 |- ( ( ( m - s ) e. ZZ /\ m e. ZZ ) -> ( m e. ( ZZ>= ` ( m - s ) ) <-> ( m - s ) <_ m ) )
71	69, 50, 70	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m e. ( ZZ>= ` ( m - s ) ) <-> ( m - s ) <_ m ) )
72	54, 71	mpbird 247	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. ( ZZ>= ` ( m - s ) ) )
73		fzss2 12381	. . . . . . . . . 10 |- ( m e. ( ZZ>= ` ( m - s ) ) -> ( 0 ... ( m - s ) ) C_ ( 0 ... m ) )
74	72, 73	syl 17	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) C_ ( 0 ... m ) )
75	74	sselda 3603	. . . . . . . 8 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. ( 0 ... m ) )
76	13	abscld 14175	. . . . . . . . . 10 |- ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. RR )
77	11, 12, 76	syl2an 494	. . . . . . . . 9 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` A ) e. RR )
78	36	abscld 14175	. . . . . . . . 9 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
79	77, 78	remulcld 10070	. . . . . . . 8 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. RR )
80	75, 79	syldan 487	. . . . . . 7 |- ( ( ( 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 )
81	46, 80	fsumrecl 14465	. . . . . 6 |- ( ( 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 )
82		fzfid 12772	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( m - s ) + 1 ) ... m ) e. Fin )
83		elfznn0 12433	. . . . . . . . . . . . 13 |- ( ( m - s ) e. ( 0 ... m ) -> ( m - s ) e. NN0 )
84	67, 83	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. NN0 )
85		peano2nn0 11333	. . . . . . . . . . . 12 |- ( ( m - s ) e. NN0 -> ( ( m - s ) + 1 ) e. NN0 )
86	84, 85	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. NN0 )
87	86, 30	syl6eleq 2711	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` 0 ) )
88		fzss1 12380	. . . . . . . . . 10 |- ( ( ( m - s ) + 1 ) e. ( ZZ>= ` 0 ) -> ( ( ( m - s ) + 1 ) ... m ) C_ ( 0 ... m ) )
89	87, 88	syl 17	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( m - s ) + 1 ) ... m ) C_ ( 0 ... m ) )
90	89	sselda 3603	. . . . . . . 8 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. ( 0 ... m ) )
91	90, 79	syldan 487	. . . . . . 7 |- ( ( ( 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 )
92	82, 91	fsumrecl 14465	. . . . . 6 |- ( ( 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 )
93	42	rphalfcld 11884	. . . . . . . 8 |- ( ph -> ( E / 2 ) e. RR+ )
94	93	rpred 11872	. . . . . . 7 |- ( ph -> ( E / 2 ) e. RR )
95	94	adantr 481	. . . . . 6 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( E / 2 ) e. RR )
96		elfznn0 12433	. . . . . . . . . . 11 |- ( j e. ( 0 ... ( m - s ) ) -> j e. NN0 )
97	11, 96, 76	syl2an 494	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` A ) e. RR )
98	46, 97	fsumrecl 14465	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) e. RR )
99	98, 95	remulcld 10070	. . . . . . . 8 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) x. ( E / 2 ) ) e. RR )
100		0zd 11389	. . . . . . . . . . 11 |- ( ph -> 0 e. ZZ )
101		eqidd 2623	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( K ` j ) )
102		mertens.2	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
103	102, 76	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( K ` j ) e. RR )
104		mertens.7	. . . . . . . . . . 11 |- ( ph -> seq 0 ( + , K ) e. dom ~~> )
105	30, 100, 101, 103, 104	isumrecl 14496	. . . . . . . . . 10 |- ( ph -> sum_ j e. NN0 ( K ` j ) e. RR )
106	13	absge0d 14183	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
107	106, 102	breqtrrd 4681	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> 0 <_ ( K ` j ) )
108	30, 100, 101, 103, 104, 107	isumge0 14497	. . . . . . . . . 10 |- ( ph -> 0 <_ sum_ j e. NN0 ( K ` j ) )
109	105, 108	ge0p1rpd 11902	. . . . . . . . 9 |- ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR+ )
110	109	adantr 481	. . . . . . . 8 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR+ )
111	99, 110	rerpdivcld 11903	. . . . . . 7 |- ( ( 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 )
112	93, 109	rpdivcld 11889	. . . . . . . . . . . 12 |- ( ph -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR+ )
113	112	rpred 11872	. . . . . . . . . . 11 |- ( ph -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR )
114	113	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) e. RR )
115	97, 114	remulcld 10070	. . . . . . . . 9 |- ( ( ( 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 )
116	75, 20	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) + 1 ) e. ZZ )
117		simplll 798	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
118	75, 19	syldan 487	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) + 1 ) e. NN0 )
119	118, 22	sylan 488	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
120	117, 119, 24	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
121	117, 119, 26	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> B e. CC )
122	75, 35	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> seq ( ( m - j ) + 1 ) ( + , G ) e. dom ~~> )
123	15, 116, 120, 121, 122	isumcl 14492	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B e. CC )
124	123	abscld 14175	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
125	76, 106	jca 554	. . . . . . . . . . 11 |- ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
126	11, 96, 125	syl2an 494	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
127	120	sumeq2dv 14433	. . . . . . . . . . . . 13 |- ( ( ( 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 )
128	127	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
129		elfzelz 12342	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 0 ... ( m - s ) ) -> j e. ZZ )
130	129	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. ZZ )
131	130	zred 11482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j e. RR )
132	49	ad2antlr 763	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> m e. ZZ )
133	132	zred 11482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> m e. RR )
134	56	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s e. ZZ )
135	134	zred 11482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s e. RR )
136		elfzle2 12345	. . . . . . . . . . . . . . . 16 |- ( j e. ( 0 ... ( m - s ) ) -> j <_ ( m - s ) )
137	136	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> j <_ ( m - s ) )
138	131, 133, 135, 137	lesubd 10631	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> s <_ ( m - j ) )
139	132, 130	zsubcld 11487	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( m - j ) e. ZZ )
140		eluz 11701	. . . . . . . . . . . . . . 15 |- ( ( s e. ZZ /\ ( m - j ) e. ZZ ) -> ( ( m - j ) e. ( ZZ>= ` s ) <-> s <_ ( m - j ) ) )
141	134, 139, 140	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( ( m - j ) e. ( ZZ>= ` s ) <-> s <_ ( m - j ) ) )
142	138, 141	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( m - j ) e. ( ZZ>= ` s ) )
143	4	simprd 479	. . . . . . . . . . . . . 14 |- ( ph -> A. n e. ( ZZ>= ` s ) ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) < ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
144	143	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
145		oveq1 6657	. . . . . . . . . . . . . . . . . 18 |- ( n = ( m - j ) -> ( n + 1 ) = ( ( m - j ) + 1 ) )
146	145	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( n = ( m - j ) -> ( ZZ>= ` ( n + 1 ) ) = ( ZZ>= ` ( ( m - j ) + 1 ) ) )
147	146	sumeq1d 14431	. . . . . . . . . . . . . . . 16 |- ( n = ( m - j ) -> sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) )
148	147	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( n = ( m - j ) -> ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) )
149	148	breq1d 4663	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
150	149	rspcv 3305	. . . . . . . . . . . . 13 |- ( ( m - j ) e. ( ZZ>= ` s ) -> ( A. n e. ( ZZ>= ` s ) ( 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 ) ) ) )
151	142, 144, 150	sylc 65	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
152	128, 151	eqbrtrrd 4677	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
153	124, 114, 152	ltled 10185	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
154		lemul2a 10878	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
155	124, 114, 126, 153, 154	syl31anc 1329	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
156	46, 80, 115, 155	fsumle 14531	. . . . . . . 8 |- ( ( 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 ) ) ) )
157	98	recnd 10068	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) e. CC )
158	93	rpcnd 11874	. . . . . . . . . . 11 |- ( ph -> ( E / 2 ) e. CC )
159	158	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( E / 2 ) e. CC )
160		peano2re 10209	. . . . . . . . . . . . 13 |- ( sum_ j e. NN0 ( K ` j ) e. RR -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
161	105, 160	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
162	161	recnd 10068	. . . . . . . . . . 11 |- ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. CC )
163	162	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. CC )
164	109	rpne0d 11877	. . . . . . . . . . 11 |- ( ph -> ( sum_ j e. NN0 ( K ` j ) + 1 ) =/= 0 )
165	164	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) =/= 0 )
166	157, 159, 163, 165	divassd 10836	. . . . . . . . 9 |- ( ( 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 ) ) ) )
167		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( n = j -> ( K ` n ) = ( K ` j ) )
168	167	cbvsumv 14426	. . . . . . . . . . . . . . . 16 |- sum_ n e. NN0 ( K ` n ) = sum_ j e. NN0 ( K ` j )
169	168	oveq1i 6660	. . . . . . . . . . . . . . 15 |- ( sum_ n e. NN0 ( K ` n ) + 1 ) = ( sum_ j e. NN0 ( K ` j ) + 1 )
170	169	oveq2i 6661	. . . . . . . . . . . . . 14 |- ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) = ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) )
171	170, 112	syl5eqel 2705	. . . . . . . . . . . . 13 |- ( ph -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. RR+ )
172	171	rpcnd 11874	. . . . . . . . . . . 12 |- ( ph -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. CC )
173	172	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) e. CC )
174	76	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. CC )
175	11, 96, 174	syl2an 494	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... ( m - s ) ) ) -> ( abs ` A ) e. CC )
176	46, 173, 175	fsummulc1 14517	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
177	170	oveq2i 6661	. . . . . . . . . 10 |- ( 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 ) ) )
178	170	oveq2i 6661	. . . . . . . . . . . 12 |- ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ n e. NN0 ( K ` n ) + 1 ) ) ) = ( ( abs ` A ) x. ( ( E / 2 ) / ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
179	178	a1i 11	. . . . . . . . . . 11 |- ( 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 ) ) ) )
180	179	sumeq2i 14429	. . . . . . . . . 10 |- 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 ) ) )
181	176, 177, 180	3eqtr3g 2679	. . . . . . . . 9 |- ( ( 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 ) ) ) )
182	166, 181	eqtrd 2656	. . . . . . . 8 |- ( ( 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 ) ) ) )
183	156, 182	breqtrrd 4681	. . . . . . 7 |- ( ( 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 ) ) )
184	105	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) e. RR )
185	161	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR )
186		0zd 11389	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 0 e. ZZ )
187		fz0ssnn0 12435	. . . . . . . . . . . . 13 |- ( 0 ... ( m - s ) ) C_ NN0
188	187	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... ( m - s ) ) C_ NN0 )
189	102	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> ( K ` j ) = ( abs ` A ) )
190	76	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> ( abs ` A ) e. RR )
191	106	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
192	104	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> seq 0 ( + , K ) e. dom ~~> )
193	30, 186, 46, 188, 189, 190, 191, 192	isumless 14577	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) <_ sum_ j e. NN0 ( abs ` A ) )
194	102	sumeq2dv 14433	. . . . . . . . . . . 12 |- ( ph -> sum_ j e. NN0 ( K ` j ) = sum_ j e. NN0 ( abs ` A ) )
195	194	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) = sum_ j e. NN0 ( abs ` A ) )
196	193, 195	breqtrrd 4681	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) <_ sum_ j e. NN0 ( K ` j ) )
197	105	ltp1d 10954	. . . . . . . . . . 11 |- ( ph -> sum_ j e. NN0 ( K ` j ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
198	197	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. NN0 ( K ` j ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
199	98, 184, 185, 196, 198	lelttrd 10195	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... ( m - s ) ) ( abs ` A ) < ( sum_ j e. NN0 ( K ` j ) + 1 ) )
200	93	rpregt0d 11878	. . . . . . . . . . 11 |- ( ph -> ( ( E / 2 ) e. RR /\ 0 < ( E / 2 ) ) )
201	200	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) e. RR /\ 0 < ( E / 2 ) ) )
202		ltmul1 10873	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
203	98, 185, 201, 202	syl3anc 1326	. . . . . . . . 9 |- ( ( 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 ) ) ) )
204	199, 203	mpbid 222	. . . . . . . 8 |- ( ( 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 ) ) )
205	109	rpregt0d 11878	. . . . . . . . . 10 |- ( ph -> ( ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ 0 < ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
206	205	adantr 481	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( sum_ j e. NN0 ( K ` j ) + 1 ) e. RR /\ 0 < ( sum_ j e. NN0 ( K ` j ) + 1 ) ) )
207		ltdivmul 10898	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
208	99, 95, 206, 207	syl3anc 1326	. . . . . . . 8 |- ( ( 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 ) ) ) )
209	204, 208	mpbird 247	. . . . . . 7 |- ( ( 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 ) )
210	81, 111, 95, 183, 209	lelttrd 10195	. . . . . 6 |- ( ( 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 ) )
211		mertens.13	. . . . . . . . . . . 12 |- ( ph -> ( 0 <_ sup ( T , RR , < ) /\ ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) ) )
212	211	simprd 479	. . . . . . . . . . 11 |- ( ph -> ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) )
213		suprcl 10983	. . . . . . . . . . 11 |- ( ( T C_ RR /\ T =/= (/) /\ E. z e. RR A. w e. T w <_ z ) -> sup ( T , RR , < ) e. RR )
214	212, 213	syl 17	. . . . . . . . . 10 |- ( ph -> sup ( T , RR , < ) e. RR )
215	94, 214	remulcld 10070	. . . . . . . . 9 |- ( ph -> ( ( E / 2 ) x. sup ( T , RR , < ) ) e. RR )
216	211	simpld 475	. . . . . . . . . 10 |- ( ph -> 0 <_ sup ( T , RR , < ) )
217	214, 216	ge0p1rpd 11902	. . . . . . . . 9 |- ( ph -> ( sup ( T , RR , < ) + 1 ) e. RR+ )
218	215, 217	rerpdivcld 11903	. . . . . . . 8 |- ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
219	218	adantr 481	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
220	5	nnrpd 11870	. . . . . . . . . . . . . 14 |- ( ph -> s e. RR+ )
221	93, 220	rpdivcld 11889	. . . . . . . . . . . . 13 |- ( ph -> ( ( E / 2 ) / s ) e. RR+ )
222	221, 217	rpdivcld 11889	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR+ )
223	222	rpred 11872	. . . . . . . . . . 11 |- ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
224	223, 214	remulcld 10070	. . . . . . . . . 10 |- ( ph -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. RR )
225	224	ad2antrr 762	. . . . . . . . 9 |- ( ( ( 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 )
226		simpll 790	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ph )
227	90, 12	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. NN0 )
228	226, 227, 76	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) e. RR )
229	223	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. RR )
230	226, 227, 102	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( K ` j ) = ( abs ` A ) )
231		elfzuz 12338	. . . . . . . . . . . . . 14 |- ( j e. ( ( ( m - s ) + 1 ) ... m ) -> j e. ( ZZ>= ` ( ( m - s ) + 1 ) ) )
232		eluzle 11700	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( ZZ>= ` ( s + t ) ) -> ( s + t ) <_ m )
233	232	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( s + t ) <_ m )
234	8	nn0zd 11480	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> t e. ZZ )
235	234	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t e. ZZ )
236	235	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t e. RR )
237	52, 236, 51	leaddsub2d 10629	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( s + t ) <_ m <-> t <_ ( m - s ) ) )
238	233, 237	mpbid 222	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> t <_ ( m - s ) )
239		eluz 11701	. . . . . . . . . . . . . . . . 17 |- ( ( t e. ZZ /\ ( m - s ) e. ZZ ) -> ( ( m - s ) e. ( ZZ>= ` t ) <-> t <_ ( m - s ) ) )
240	235, 69, 239	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) e. ( ZZ>= ` t ) <-> t <_ ( m - s ) ) )
241	238, 240	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. ( ZZ>= ` t ) )
242		peano2uz 11741	. . . . . . . . . . . . . . 15 |- ( ( m - s ) e. ( ZZ>= ` t ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) )
243	241, 242	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) )
244		uztrn 11704	. . . . . . . . . . . . . 14 |- ( ( j e. ( ZZ>= ` ( ( m - s ) + 1 ) ) /\ ( ( m - s ) + 1 ) e. ( ZZ>= ` t ) ) -> j e. ( ZZ>= ` t ) )
245	231, 243, 244	syl2anr 495	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. ( ZZ>= ` t ) )
246	7	simprd 479	. . . . . . . . . . . . . 14 |- ( ph -> A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
247	246	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
248		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( m = j -> ( K ` m ) = ( K ` j ) )
249	248	breq1d 4663	. . . . . . . . . . . . . 14 |- ( m = j -> ( ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) <-> ( K ` j ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
250	249	rspcv 3305	. . . . . . . . . . . . 13 |- ( j e. ( ZZ>= ` t ) -> ( A. m e. ( ZZ>= ` t ) ( K ` m ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) -> ( K ` j ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
251	245, 247, 250	sylc 65	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( K ` j ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
252	230, 251	eqbrtrrd 4677	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) < ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
253	228, 229, 252	ltled 10185	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` A ) <_ ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) )
254	212	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( 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	51	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> m e. RR )
256		peano2zm 11420	. . . . . . . . . . . . . . . . . 18 |- ( s e. ZZ -> ( s - 1 ) e. ZZ )
257	56, 256	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( s - 1 ) e. ZZ )
258	257	zred 11482	. . . . . . . . . . . . . . . 16 |- ( ph -> ( s - 1 ) e. RR )
259	258	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( s - 1 ) e. RR )
260	227	nn0red 11352	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> j e. RR )
261	50	zcnd 11483	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> m e. CC )
262	52	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. CC )
263		1cnd 10056	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 1 e. CC )
264	261, 262, 263	subsubd 10420	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - ( s - 1 ) ) = ( ( m - s ) + 1 ) )
265	264	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - ( s - 1 ) ) = ( ( m - s ) + 1 ) )
266		elfzle1 12344	. . . . . . . . . . . . . . . . 17 |- ( j e. ( ( ( m - s ) + 1 ) ... m ) -> ( ( m - s ) + 1 ) <_ j )
267	266	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( m - s ) + 1 ) <_ j )
268	265, 267	eqbrtrd 4675	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - ( s - 1 ) ) <_ j )
269	255, 259, 260, 268	subled 10630	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) <_ ( s - 1 ) )
270	90, 16	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. NN0 )
271	270, 30	syl6eleq 2711	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. ( ZZ>= ` 0 ) )
272	257	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( s - 1 ) e. ZZ )
273		elfz5 12334	. . . . . . . . . . . . . . 15 |- ( ( ( m - j ) e. ( ZZ>= ` 0 ) /\ ( s - 1 ) e. ZZ ) -> ( ( m - j ) e. ( 0 ... ( s - 1 ) ) <-> ( m - j ) <_ ( s - 1 ) ) )
274	271, 272, 273	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( 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 247	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( m - j ) e. ( 0 ... ( s - 1 ) ) )
276		simplll 798	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ph )
277	90, 19	syldan 487	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( m - j ) + 1 ) e. NN0 )
278	277, 22	sylan 488	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> k e. NN0 )
279	276, 278, 24	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) /\ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ) -> ( G ` k ) = B )
280	279	sumeq2dv 14433	. . . . . . . . . . . . . . 15 |- ( ( ( 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 2628	. . . . . . . . . . . . . 14 |- ( ( ( 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 6195	. . . . . . . . . . . . 13 |- ( ( ( 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	148	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( n = ( m - j ) -> ( ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) <-> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) = ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) ( G ` k ) ) ) )
284	283	rspcev 3309	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
285	275, 282, 284	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
286		fvex 6201	. . . . . . . . . . . . 13 |- ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. _V
287		eqeq1 2626	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
288	287	rexbidv 3052	. . . . . . . . . . . . 13 |- ( 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 ) ) ) )
289		mertens.10	. . . . . . . . . . . . 13 |- T = { z | E. n e. ( 0 ... ( s - 1 ) ) z = ( abs ` sum_ k e. ( ZZ>= ` ( n + 1 ) ) ( G ` k ) ) }
290	286, 288, 289	elab2 3354	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
291	285, 290	sylibr 224	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. T )
292		suprub 10984	. . . . . . . . . . 11 |- ( ( ( 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 , < ) )
293	254, 291, 292	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) <_ sup ( T , RR , < ) )
294	226, 227, 125	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
295	90, 78	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) e. RR )
296	36	absge0d 14183	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
297	90, 296	syldan 487	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> 0 <_ ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) )
298	295, 297	jca 554	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
299	214	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( ( ( m - s ) + 1 ) ... m ) ) -> sup ( T , RR , < ) e. RR )
300		lemul12a 10881	. . . . . . . . . . 11 |- ( ( ( ( ( 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 , < ) ) ) )
301	294, 229, 298, 299, 300	syl22anc 1327	. . . . . . . . . 10 |- ( ( ( 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 , < ) ) ) )
302	253, 293, 301	mp2and 715	. . . . . . . . 9 |- ( ( ( 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 , < ) ) )
303	82, 91, 225, 302	fsumle 14531	. . . . . . . 8 |- ( ( 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 , < ) ) )
304	224	recnd 10068	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. CC )
305	304	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) e. CC )
306		fsumconst 14522	. . . . . . . . . 10 |- ( ( ( ( ( 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 , < ) ) ) )
307	82, 305, 306	syl2anc 693	. . . . . . . . 9 |- ( ( 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 , < ) ) ) )
308		1zzd 11408	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> 1 e. ZZ )
309	56	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> s e. ZZ )
310		fzen 12358	. . . . . . . . . . . . . 14 |- ( ( 1 e. ZZ /\ s e. ZZ /\ ( m - s ) e. ZZ ) -> ( 1 ... s ) ~~ ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) )
311	308, 309, 69, 310	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) ~~ ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) )
312		ax-1cn 9994	. . . . . . . . . . . . . . 15 |- 1 e. CC
313	69	zcnd 11483	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. CC )
314		addcom 10222	. . . . . . . . . . . . . . 15 |- ( ( 1 e. CC /\ ( m - s ) e. CC ) -> ( 1 + ( m - s ) ) = ( ( m - s ) + 1 ) )
315	312, 313, 314	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 + ( m - s ) ) = ( ( m - s ) + 1 ) )
316	262, 261	pncan3d 10395	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( s + ( m - s ) ) = m )
317	315, 316	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( 1 + ( m - s ) ) ... ( s + ( m - s ) ) ) = ( ( ( m - s ) + 1 ) ... m ) )
318	311, 317	breqtrd 4679	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) )
319		fzfid 12772	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 1 ... s ) e. Fin )
320		hashen 13135	. . . . . . . . . . . . 13 |- ( ( ( 1 ... s ) e. Fin /\ ( ( ( m - s ) + 1 ) ... m ) e. Fin ) -> ( ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) <-> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) ) )
321	319, 82, 320	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) <-> ( 1 ... s ) ~~ ( ( ( m - s ) + 1 ) ... m ) ) )
322	318, 321	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( 1 ... s ) ) = ( # ` ( ( ( m - s ) + 1 ) ... m ) ) )
323		hashfz1 13134	. . . . . . . . . . . 12 |- ( s e. NN0 -> ( # ` ( 1 ... s ) ) = s )
324	47, 323	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( 1 ... s ) ) = s )
325	322, 324	eqtr3d 2658	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( # ` ( ( ( m - s ) + 1 ) ... m ) ) = s )
326	325	oveq1d 6665	. . . . . . . . 9 |- ( ( 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 , < ) ) ) )
327	214	recnd 10068	. . . . . . . . . . . 12 |- ( ph -> sup ( T , RR , < ) e. CC )
328	217	rpcnne0d 11881	. . . . . . . . . . . 12 |- ( ph -> ( ( sup ( T , RR , < ) + 1 ) e. CC /\ ( sup ( T , RR , < ) + 1 ) =/= 0 ) )
329		div23 10704	. . . . . . . . . . . 12 |- ( ( ( 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 , < ) ) )
330	158, 327, 328, 329	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
331	56	zcnd 11483	. . . . . . . . . . . . . 14 |- ( ph -> s e. CC )
332	221	rpcnd 11874	. . . . . . . . . . . . . 14 |- ( ph -> ( ( E / 2 ) / s ) e. CC )
333		divass 10703	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
334	331, 332, 328, 333	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( ( s x. ( ( E / 2 ) / s ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) )
335	5	nnne0d 11065	. . . . . . . . . . . . . . 15 |- ( ph -> s =/= 0 )
336	158, 331, 335	divcan2d 10803	. . . . . . . . . . . . . 14 |- ( ph -> ( s x. ( ( E / 2 ) / s ) ) = ( E / 2 ) )
337	336	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ph -> ( ( s x. ( ( E / 2 ) / s ) ) / ( sup ( T , RR , < ) + 1 ) ) = ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) )
338	334, 337	eqtr3d 2658	. . . . . . . . . . . 12 |- ( ph -> ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) = ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) )
339	338	oveq1d 6665	. . . . . . . . . . 11 |- ( ph -> ( ( s x. ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) ) x. sup ( T , RR , < ) ) = ( ( ( E / 2 ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) )
340	222	rpcnd 11874	. . . . . . . . . . . 12 |- ( ph -> ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) e. CC )
341	331, 340, 327	mulassd 10063	. . . . . . . . . . 11 |- ( 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 , < ) ) ) )
342	330, 339, 341	3eqtr2rd 2663	. . . . . . . . . 10 |- ( ph -> ( s x. ( ( ( ( E / 2 ) / s ) / ( sup ( T , RR , < ) + 1 ) ) x. sup ( T , RR , < ) ) ) = ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) )
343	342	adantr 481	. . . . . . . . 9 |- ( ( 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 ) ) )
344	307, 326, 343	3eqtrd 2660	. . . . . . . 8 |- ( ( 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 ) ) )
345	303, 344	breqtrd 4679	. . . . . . 7 |- ( ( 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 ) ) )
346		peano2re 10209	. . . . . . . . . . 11 |- ( sup ( T , RR , < ) e. RR -> ( sup ( T , RR , < ) + 1 ) e. RR )
347	214, 346	syl 17	. . . . . . . . . 10 |- ( ph -> ( sup ( T , RR , < ) + 1 ) e. RR )
348	214	ltp1d 10954	. . . . . . . . . 10 |- ( ph -> sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) )
349	214, 347, 93, 348	ltmul2dd 11928	. . . . . . . . 9 |- ( ph -> ( ( E / 2 ) x. sup ( T , RR , < ) ) < ( ( E / 2 ) x. ( sup ( T , RR , < ) + 1 ) ) )
350	215, 94, 217	ltdivmul2d 11924	. . . . . . . . 9 |- ( 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 ) ) ) )
351	349, 350	mpbird 247	. . . . . . . 8 |- ( ph -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) < ( E / 2 ) )
352	351	adantr 481	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( ( E / 2 ) x. sup ( T , RR , < ) ) / ( sup ( T , RR , < ) + 1 ) ) < ( E / 2 ) )
353	92, 219, 95, 345, 352	lelttrd 10195	. . . . . 6 |- ( ( 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 ) )
354	81, 92, 95, 95, 210, 353	lt2addd 10650	. . . . 5 |- ( ( 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 ) ) )
355	14, 36	absmuld 14193	. . . . . . 7 |- ( ( ( 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 ) ) )
356	355	sumeq2dv 14433	. . . . . 6 |- ( ( 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 ) ) )
357	69	zred 11482	. . . . . . . . 9 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) e. RR )
358	357	ltp1d 10954	. . . . . . . 8 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( m - s ) < ( ( m - s ) + 1 ) )
359		fzdisj 12368	. . . . . . . 8 |- ( ( m - s ) < ( ( m - s ) + 1 ) -> ( ( 0 ... ( m - s ) ) i^i ( ( ( m - s ) + 1 ) ... m ) ) = (/) )
360	358, 359	syl 17	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( 0 ... ( m - s ) ) i^i ( ( ( m - s ) + 1 ) ... m ) ) = (/) )
361		fzsplit 12367	. . . . . . . 8 |- ( ( m - s ) e. ( 0 ... m ) -> ( 0 ... m ) = ( ( 0 ... ( m - s ) ) u. ( ( ( m - s ) + 1 ) ... m ) ) )
362	67, 361	syl 17	. . . . . . 7 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( 0 ... m ) = ( ( 0 ... ( m - s ) ) u. ( ( ( m - s ) + 1 ) ... m ) ) )
363	79	recnd 10068	. . . . . . 7 |- ( ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) /\ j e. ( 0 ... m ) ) -> ( ( abs ` A ) x. ( abs ` sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) e. CC )
364	360, 362, 10, 363	fsumsplit 14471	. . . . . 6 |- ( ( 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 ) ) ) )
365	356, 364	eqtr2d 2657	. . . . 5 |- ( ( 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 ) ) )
366	42	rpcnd 11874	. . . . . . 7 |- ( ph -> E e. CC )
367	366	adantr 481	. . . . . 6 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> E e. CC )
368	367	2halvesd 11278	. . . . 5 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( ( E / 2 ) + ( E / 2 ) ) = E )
369	354, 365, 368	3brtr3d 4684	. . . 4 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> sum_ j e. ( 0 ... m ) ( abs ` ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
370	39, 41, 44, 45, 369	lelttrd 10195	. . 3 |- ( ( ph /\ m e. ( ZZ>= ` ( s + t ) ) ) -> ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
371	370	ralrimiva 2966	. 2 |- ( ph -> A. m e. ( ZZ>= ` ( s + t ) ) ( abs ` sum_ j e. ( 0 ... m ) ( A x. sum_ k e. ( ZZ>= ` ( ( m - j ) + 1 ) ) B ) ) < E )
372		fveq2 6191	. . . 4 |- ( y = ( s + t ) -> ( ZZ>= ` y ) = ( ZZ>= ` ( s + t ) ) )
373	372	raleqdv 3144	. . 3 |- ( 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 ) )
374	373	rspcev 3309	. 2 |- ( ( ( 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 )
375	9, 371, 374	syl2anc 693	1 |- ( 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 )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   class class class wbr 4653   dom cdm 5114   ` cfv 5888  (class class class)co 6650   ~~ cen 7952   Fincfn 7955   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   ...cfz 12326   seqcseq 12801   #chash 13117   abscabs 13974   ~~> cli 14215   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417

This theorem is referenced by:  mertenslem2  14617