Theorem fsumharmonic

Description: Bound a finite sum based on the harmonic series, where the "strong" bound C only applies asymptotically, and there is a "weak" bound R for the remaining values. (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	fsumharmonic.a	|- ( ph -> A e. RR+ )
	fsumharmonic.t	|- ( ph -> ( T e. RR /\ 1 <_ T ) )
	fsumharmonic.r	|- ( ph -> ( R e. RR /\ 0 <_ R ) )
	fsumharmonic.b	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )
	fsumharmonic.c	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> C e. RR )
	fsumharmonic.0	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ C )
	fsumharmonic.1	|- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ T <_ ( A / n ) ) -> ( abs ` B ) <_ ( C x. n ) )
	fsumharmonic.2	|- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( A / n ) < T ) -> ( abs ` B ) <_ R )
Assertion	fsumharmonic	|- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fsumharmonic.a	|- ( ph -> A e. RR+ )
2		fsumharmonic.t	|- ( ph -> ( T e. RR /\ 1 <_ T ) )
3		fsumharmonic.r	|- ( ph -> ( R e. RR /\ 0 <_ R ) )
4		fsumharmonic.b	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )
5		fsumharmonic.c	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> C e. RR )
6		fsumharmonic.0	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ C )
7		fsumharmonic.1	|- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ T <_ ( A / n ) ) -> ( abs ` B ) <_ ( C x. n ) )
8		fsumharmonic.2	|- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( A / n ) < T ) -> ( abs ` B ) <_ R )
9		fzfid	|- ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin )
10		elfznn	|- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
11	10	adantl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
12	11	nncnd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. CC )
13	11	nnne0d	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n =/= 0 )
14	4 12 13	divcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( B / n ) e. CC )
15	9 14	fsumcl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) e. CC )
16	15	abscld	|- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) e. RR )
17	4	abscld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( abs ` B ) e. RR )
18	17 11	nndivred	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / n ) e. RR )
19	9 18	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( abs ` B ) / n ) e. RR )
20	9 5	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) C e. RR )
21	3	simpld	|- ( ph -> R e. RR )
22	2	simpld	|- ( ph -> T e. RR )
23		0red	|- ( ph -> 0 e. RR )
24		1red	|- ( ph -> 1 e. RR )
25		0lt1	|- 0 < 1
26	25	a1i	|- ( ph -> 0 < 1 )
27	2	simprd	|- ( ph -> 1 <_ T )
28	23 24 22 26 27	ltletrd	|- ( ph -> 0 < T )
29	22 28	elrpd	|- ( ph -> T e. RR+ )
30	29	relogcld	|- ( ph -> ( log ` T ) e. RR )
31	30 24	readdcld	|- ( ph -> ( ( log ` T ) + 1 ) e. RR )
32	21 31	remulcld	|- ( ph -> ( R x. ( ( log ` T ) + 1 ) ) e. RR )
33	20 32	readdcld	|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) e. RR )
34	9 14	fsumabs	|- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) ( abs ` ( B / n ) ) )
35	4 12 13	absdivd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( abs ` ( B / n ) ) = ( ( abs ` B ) / ( abs ` n ) ) )
36	11	nnrpd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ )
37	36	rprege0d	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( n e. RR /\ 0 <_ n ) )
38		absid	|- ( ( n e. RR /\ 0 <_ n ) -> ( abs ` n ) = n )
39	37 38	syl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( abs ` n ) = n )
40	39	oveq2d	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / ( abs ` n ) ) = ( ( abs ` B ) / n ) )
41	35 40	eqtrd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( abs ` ( B / n ) ) = ( ( abs ` B ) / n ) )
42	41	sumeq2dv	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( abs ` ( B / n ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( abs ` B ) / n ) )
43	34 42	breqtrd	|- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( abs ` B ) / n ) )
44	1 29	rpdivcld	|- ( ph -> ( A / T ) e. RR+ )
45	44	rprege0d	|- ( ph -> ( ( A / T ) e. RR /\ 0 <_ ( A / T ) ) )
46		flge0nn0	|- ( ( ( A / T ) e. RR /\ 0 <_ ( A / T ) ) -> ( |_ ` ( A / T ) ) e. NN0 )
47	45 46	syl	|- ( ph -> ( |_ ` ( A / T ) ) e. NN0 )
48	47	nn0red	|- ( ph -> ( |_ ` ( A / T ) ) e. RR )
49	48	ltp1d	|- ( ph -> ( |_ ` ( A / T ) ) < ( ( |_ ` ( A / T ) ) + 1 ) )
50		fzdisj	|- ( ( |_ ` ( A / T ) ) < ( ( |_ ` ( A / T ) ) + 1 ) -> ( ( 1 ... ( |_ ` ( A / T ) ) ) i^i ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) = (/) )
51	49 50	syl	|- ( ph -> ( ( 1 ... ( |_ ` ( A / T ) ) ) i^i ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) = (/) )
52		nn0p1nn	|- ( ( |_ ` ( A / T ) ) e. NN0 -> ( ( |_ ` ( A / T ) ) + 1 ) e. NN )
53	47 52	syl	|- ( ph -> ( ( |_ ` ( A / T ) ) + 1 ) e. NN )
54		nnuz	|- NN = ( ZZ>= ` 1 )
55	53 54	eleqtrdi	|- ( ph -> ( ( |_ ` ( A / T ) ) + 1 ) e. ( ZZ>= ` 1 ) )
56	44	rpred	|- ( ph -> ( A / T ) e. RR )
57	1	rpred	|- ( ph -> A e. RR )
58	22 28	jca	|- ( ph -> ( T e. RR /\ 0 < T ) )
59	1	rpregt0d	|- ( ph -> ( A e. RR /\ 0 < A ) )
60		lediv2	|- ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( T e. RR /\ 0 < T ) /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ T <-> ( A / T ) <_ ( A / 1 ) ) )
61	24 26 58 59 60	syl211anc	|- ( ph -> ( 1 <_ T <-> ( A / T ) <_ ( A / 1 ) ) )
62	27 61	mpbid	|- ( ph -> ( A / T ) <_ ( A / 1 ) )
63	57	recnd	|- ( ph -> A e. CC )
64	63	div1d	|- ( ph -> ( A / 1 ) = A )
65	62 64	breqtrd	|- ( ph -> ( A / T ) <_ A )
66		flword2	|- ( ( ( A / T ) e. RR /\ A e. RR /\ ( A / T ) <_ A ) -> ( |_ ` A ) e. ( ZZ>= ` ( |_ ` ( A / T ) ) ) )
67	56 57 65 66	syl3anc	|- ( ph -> ( |_ ` A ) e. ( ZZ>= ` ( |_ ` ( A / T ) ) ) )
68		fzsplit2	|- ( ( ( ( |_ ` ( A / T ) ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ( ZZ>= ` ( |_ ` ( A / T ) ) ) ) -> ( 1 ... ( |_ ` A ) ) = ( ( 1 ... ( |_ ` ( A / T ) ) ) u. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
69	55 67 68	syl2anc	|- ( ph -> ( 1 ... ( |_ ` A ) ) = ( ( 1 ... ( |_ ` ( A / T ) ) ) u. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
70	18	recnd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / n ) e. CC )
71	51 69 9 70	fsumsplit	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( abs ` B ) / n ) = ( sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( ( abs ` B ) / n ) + sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) ) )
72		fzfid	|- ( ph -> ( 1 ... ( |_ ` ( A / T ) ) ) e. Fin )
73		ssun1	|- ( 1 ... ( |_ ` ( A / T ) ) ) C_ ( ( 1 ... ( |_ ` ( A / T ) ) ) u. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) )
74	73 69	sseqtrrid	|- ( ph -> ( 1 ... ( |_ ` ( A / T ) ) ) C_ ( 1 ... ( |_ ` A ) ) )
75	74	sselda	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> n e. ( 1 ... ( |_ ` A ) ) )
76	75 18	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( ( abs ` B ) / n ) e. RR )
77	72 76	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( ( abs ` B ) / n ) e. RR )
78		fzfid	|- ( ph -> ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) e. Fin )
79		ssun2	|- ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) C_ ( ( 1 ... ( |_ ` ( A / T ) ) ) u. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) )
80	79 69	sseqtrrid	|- ( ph -> ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` A ) ) )
81	80	sselda	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> n e. ( 1 ... ( |_ ` A ) ) )
82	81 18	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / n ) e. RR )
83	78 82	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) e. RR )
84	75 5	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> C e. RR )
85	72 84	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) C e. RR )
86		fznnfl	|- ( ( A / T ) e. RR -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> ( n e. NN /\ n <_ ( A / T ) ) ) )
87	56 86	syl	|- ( ph -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> ( n e. NN /\ n <_ ( A / T ) ) ) )
88	87	simplbda	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> n <_ ( A / T ) )
89	36	rpred	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR )
90	57	adantr	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
91	58	adantr	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( T e. RR /\ 0 < T ) )
92		lemuldiv2	|- ( ( n e. RR /\ A e. RR /\ ( T e. RR /\ 0 < T ) ) -> ( ( T x. n ) <_ A <-> n <_ ( A / T ) ) )
93	89 90 91 92	syl3anc	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( T x. n ) <_ A <-> n <_ ( A / T ) ) )
94	22	adantr	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> T e. RR )
95	94 90 36	lemuldivd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( T x. n ) <_ A <-> T <_ ( A / n ) ) )
96	93 95	bitr3d	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( n <_ ( A / T ) <-> T <_ ( A / n ) ) )
97	75 96	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( n <_ ( A / T ) <-> T <_ ( A / n ) ) )
98	88 97	mpbid	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> T <_ ( A / n ) )
99	7	ex	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( T <_ ( A / n ) -> ( abs ` B ) <_ ( C x. n ) ) )
100	75 99	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( T <_ ( A / n ) -> ( abs ` B ) <_ ( C x. n ) ) )
101	98 100	mpd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( abs ` B ) <_ ( C x. n ) )
102	75 4	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> B e. CC )
103	102	abscld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( abs ` B ) e. RR )
104	75 10	syl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> n e. NN )
105	104	nnrpd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> n e. RR+ )
106	103 84 105	ledivmul2d	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( ( ( abs ` B ) / n ) <_ C <-> ( abs ` B ) <_ ( C x. n ) ) )
107	101 106	mpbird	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( ( abs ` B ) / n ) <_ C )
108	72 76 84 107	fsumle	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( ( abs ` B ) / n ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) C )
109	9 5 6 74	fsumless	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) C <_ sum_ n e. ( 1 ... ( |_ ` A ) ) C )
110	77 85 20 108 109	letrd	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( ( abs ` B ) / n ) <_ sum_ n e. ( 1 ... ( |_ ` A ) ) C )
111	81 10	syl	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> n e. NN )
112	111	nnrecred	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( 1 / n ) e. RR )
113	78 112	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) e. RR )
114	21 113	remulcld	|- ( ph -> ( R x. sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) e. RR )
115	21	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> R e. RR )
116	115	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> R e. CC )
117	111	nncnd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> n e. CC )
118	111	nnne0d	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> n =/= 0 )
119	116 117 118	divrecd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( R / n ) = ( R x. ( 1 / n ) ) )
120	115 111	nndivred	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( R / n ) e. RR )
121	119 120	eqeltrrd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( R x. ( 1 / n ) ) e. RR )
122	81 17	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( abs ` B ) e. RR )
123	81 36	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> n e. RR+ )
124		noel	|- -. n e. (/)
125		elin	|- ( n e. ( ( 1 ... ( |_ ` ( A / T ) ) ) i^i ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) <-> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
126	51	eleq2d	|- ( ph -> ( n e. ( ( 1 ... ( |_ ` ( A / T ) ) ) i^i ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) <-> n e. (/) ) )
127	125 126	bitr3id	|- ( ph -> ( ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) <-> n e. (/) ) )
128	124 127	mtbiri	|- ( ph -> -. ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
129		imnan	|- ( ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) -> -. n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) <-> -. ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
130	128 129	sylibr	|- ( ph -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) -> -. n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) )
131	130	con2d	|- ( ph -> ( n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) -> -. n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) )
132	131	imp	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> -. n e. ( 1 ... ( |_ ` ( A / T ) ) ) )
133	86	baibd	|- ( ( ( A / T ) e. RR /\ n e. NN ) -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> n <_ ( A / T ) ) )
134	56 10 133	syl2an	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> n <_ ( A / T ) ) )
135	134 96	bitrd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> T <_ ( A / n ) ) )
136	81 135	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( n e. ( 1 ... ( |_ ` ( A / T ) ) ) <-> T <_ ( A / n ) ) )
137	132 136	mtbid	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> -. T <_ ( A / n ) )
138	57	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> A e. RR )
139	138 111	nndivred	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( A / n ) e. RR )
140	22	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> T e. RR )
141	139 140	ltnled	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( ( A / n ) < T <-> -. T <_ ( A / n ) ) )
142	137 141	mpbird	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( A / n ) < T )
143	8	ex	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( A / n ) < T -> ( abs ` B ) <_ R ) )
144	81 143	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( ( A / n ) < T -> ( abs ` B ) <_ R ) )
145	142 144	mpd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( abs ` B ) <_ R )
146	122 115 123 145	lediv1dd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / n ) <_ ( R / n ) )
147	146 119	breqtrd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( ( abs ` B ) / n ) <_ ( R x. ( 1 / n ) ) )
148	78 82 121 147	fsumle	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) <_ sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( R x. ( 1 / n ) ) )
149	21	recnd	|- ( ph -> R e. CC )
150	112	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ) -> ( 1 / n ) e. CC )
151	78 149 150	fsummulc2	|- ( ph -> ( R x. sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) = sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( R x. ( 1 / n ) ) )
152	148 151	breqtrrd	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) <_ ( R x. sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) )
153	104	nnrecred	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( 1 / n ) e. RR )
154	72 153	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) e. RR )
155	154	recnd	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) e. CC )
156	113	recnd	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) e. CC )
157	11	nnrecred	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / n ) e. RR )
158	157	recnd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / n ) e. CC )
159	51 69 9 158	fsumsplit	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) = ( sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) + sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) )
160	155 156 159	mvrladdd	|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) = sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) )
161	9 157	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) e. RR )
162	161	adantr	|- ( ( ph /\ A < 1 ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) e. RR )
163	154	adantr	|- ( ( ph /\ A < 1 ) -> sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) e. RR )
164	162 163	resubcld	|- ( ( ph /\ A < 1 ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) e. RR )
165		0red	|- ( ( ph /\ A < 1 ) -> 0 e. RR )
166	31	adantr	|- ( ( ph /\ A < 1 ) -> ( ( log ` T ) + 1 ) e. RR )
167		fzfid	|- ( ( ph /\ A < 1 ) -> ( 1 ... ( |_ ` ( A / T ) ) ) e. Fin )
168	105	adantlr	|- ( ( ( ph /\ A < 1 ) /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> n e. RR+ )
169	168	rpreccld	|- ( ( ( ph /\ A < 1 ) /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( 1 / n ) e. RR+ )
170	169	rpred	|- ( ( ( ph /\ A < 1 ) /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> ( 1 / n ) e. RR )
171	169	rpge0d	|- ( ( ( ph /\ A < 1 ) /\ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ) -> 0 <_ ( 1 / n ) )
172	1	adantr	|- ( ( ph /\ A < 1 ) -> A e. RR+ )
173	172	rpge0d	|- ( ( ph /\ A < 1 ) -> 0 <_ A )
174		simpr	|- ( ( ph /\ A < 1 ) -> A < 1 )
175		0p1e1	|- ( 0 + 1 ) = 1
176	174 175	breqtrrdi	|- ( ( ph /\ A < 1 ) -> A < ( 0 + 1 ) )
177	57	adantr	|- ( ( ph /\ A < 1 ) -> A e. RR )
178		0z	|- 0 e. ZZ
179		flbi	|- ( ( A e. RR /\ 0 e. ZZ ) -> ( ( |_ ` A ) = 0 <-> ( 0 <_ A /\ A < ( 0 + 1 ) ) ) )
180	177 178 179	sylancl	|- ( ( ph /\ A < 1 ) -> ( ( |_ ` A ) = 0 <-> ( 0 <_ A /\ A < ( 0 + 1 ) ) ) )
181	173 176 180	mpbir2and	|- ( ( ph /\ A < 1 ) -> ( |_ ` A ) = 0 )
182	181	oveq2d	|- ( ( ph /\ A < 1 ) -> ( 1 ... ( |_ ` A ) ) = ( 1 ... 0 ) )
183		fz10	|- ( 1 ... 0 ) = (/)
184	182 183	eqtrdi	|- ( ( ph /\ A < 1 ) -> ( 1 ... ( |_ ` A ) ) = (/) )
185		0ss	|- (/) C_ ( 1 ... ( |_ ` ( A / T ) ) )
186	184 185	eqsstrdi	|- ( ( ph /\ A < 1 ) -> ( 1 ... ( |_ ` A ) ) C_ ( 1 ... ( |_ ` ( A / T ) ) ) )
187	167 170 171 186	fsumless	|- ( ( ph /\ A < 1 ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) )
188	162 163	suble0d	|- ( ( ph /\ A < 1 ) -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ 0 <-> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) )
189	187 188	mpbird	|- ( ( ph /\ A < 1 ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ 0 )
190	22 27	logge0d	|- ( ph -> 0 <_ ( log ` T ) )
191		0le1	|- 0 <_ 1
192	191	a1i	|- ( ph -> 0 <_ 1 )
193	30 24 190 192	addge0d	|- ( ph -> 0 <_ ( ( log ` T ) + 1 ) )
194	193	adantr	|- ( ( ph /\ A < 1 ) -> 0 <_ ( ( log ` T ) + 1 ) )
195	164 165 166 189 194	letrd	|- ( ( ph /\ A < 1 ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( log ` T ) + 1 ) )
196		harmonicubnd	|- ( ( A e. RR /\ 1 <_ A ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) )
197	57 196	sylan	|- ( ( ph /\ 1 <_ A ) -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) )
198		harmoniclbnd	|- ( ( A / T ) e. RR+ -> ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) )
199	44 198	syl	|- ( ph -> ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) )
200	199	adantr	|- ( ( ph /\ 1 <_ A ) -> ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) )
201	1	relogcld	|- ( ph -> ( log ` A ) e. RR )
202		peano2re	|- ( ( log ` A ) e. RR -> ( ( log ` A ) + 1 ) e. RR )
203	201 202	syl	|- ( ph -> ( ( log ` A ) + 1 ) e. RR )
204	44	relogcld	|- ( ph -> ( log ` ( A / T ) ) e. RR )
205		le2sub	|- ( ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) e. RR ) /\ ( ( ( log ` A ) + 1 ) e. RR /\ ( log ` ( A / T ) ) e. RR ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) /\ ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) ) )
206	161 154 203 204 205	syl22anc	|- ( ph -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) /\ ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) ) )
207	206	adantr	|- ( ( ph /\ 1 <_ A ) -> ( ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` A ) + 1 ) /\ ( log ` ( A / T ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) ) )
208	197 200 207	mp2and	|- ( ( ph /\ 1 <_ A ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) )
209	201	recnd	|- ( ph -> ( log ` A ) e. CC )
210	24	recnd	|- ( ph -> 1 e. CC )
211	30	recnd	|- ( ph -> ( log ` T ) e. CC )
212	209 210 211	pnncand	|- ( ph -> ( ( ( log ` A ) + 1 ) - ( ( log ` A ) - ( log ` T ) ) ) = ( 1 + ( log ` T ) ) )
213	1 29	relogdivd	|- ( ph -> ( log ` ( A / T ) ) = ( ( log ` A ) - ( log ` T ) ) )
214	213	oveq2d	|- ( ph -> ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) = ( ( ( log ` A ) + 1 ) - ( ( log ` A ) - ( log ` T ) ) ) )
215		ax-1cn	|- 1 e. CC
216		addcom	|- ( ( ( log ` T ) e. CC /\ 1 e. CC ) -> ( ( log ` T ) + 1 ) = ( 1 + ( log ` T ) ) )
217	211 215 216	sylancl	|- ( ph -> ( ( log ` T ) + 1 ) = ( 1 + ( log ` T ) ) )
218	212 214 217	3eqtr4d	|- ( ph -> ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) = ( ( log ` T ) + 1 ) )
219	218	adantr	|- ( ( ph /\ 1 <_ A ) -> ( ( ( log ` A ) + 1 ) - ( log ` ( A / T ) ) ) = ( ( log ` T ) + 1 ) )
220	208 219	breqtrd	|- ( ( ph /\ 1 <_ A ) -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( log ` T ) + 1 ) )
221	195 220 57 24	ltlecasei	|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( 1 / n ) - sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( 1 / n ) ) <_ ( ( log ` T ) + 1 ) )
222	160 221	eqbrtrrd	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` T ) + 1 ) )
223		lemul2a	|- ( ( ( sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) e. RR /\ ( ( log ` T ) + 1 ) e. RR /\ ( R e. RR /\ 0 <_ R ) ) /\ sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) <_ ( ( log ` T ) + 1 ) ) -> ( R x. sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) <_ ( R x. ( ( log ` T ) + 1 ) ) )
224	113 31 3 222 223	syl31anc	|- ( ph -> ( R x. sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( 1 / n ) ) <_ ( R x. ( ( log ` T ) + 1 ) ) )
225	83 114 32 152 224	letrd	|- ( ph -> sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) <_ ( R x. ( ( log ` T ) + 1 ) ) )
226	77 83 20 32 110 225	le2addd	|- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` ( A / T ) ) ) ( ( abs ` B ) / n ) + sum_ n e. ( ( ( |_ ` ( A / T ) ) + 1 ) ... ( |_ ` A ) ) ( ( abs ` B ) / n ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) )
227	71 226	eqbrtrd	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( abs ` B ) / n ) <_ ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) )
228	16 19 33 43 227	letrd	|- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) )