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	$⊢ φ \to A \in ℝ^{+}$
	fsumharmonic.t	$⊢ φ \to (T \in ℝ \land 1 \leq T)$
	fsumharmonic.r	$⊢ φ \to (R \in ℝ \land 0 \leq R)$
	fsumharmonic.b	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to B \in ℂ$
	fsumharmonic.c	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to C \in ℝ$
	fsumharmonic.0	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to 0 \leq C$
	fsumharmonic.1	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land T \leq \frac{A}{n}) \to \|B\| \leq C n$
	fsumharmonic.2	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land \frac{A}{n} < T) \to \|B\| \leq R$
Assertion	fsumharmonic	$⊢ φ \to \|\sum_{n = 1}^{⌊A⌋} (\frac{B}{n})\| \leq \sum_{n = 1}^{⌊A⌋} C + R (\log T + 1)$

Proof

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

Metamath Proof Explorer

Theorem fsumharmonic

Proof