pntrlog2bndlem6a

	Ref	Expression
Hypotheses	pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
	pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntrlog2bnd.t	$⊢ T = (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0))$
	pntrlog2bndlem5.1	$⊢ φ \to B \in ℝ^{+}$
	pntrlog2bndlem5.2	$⊢ φ \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
	pntrlog2bndlem6.1	$⊢ φ \to A \in ℝ$
	pntrlog2bndlem6.2	$⊢ φ \to 1 \leq A$
Assertion	pntrlog2bndlem6a	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) = (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
2		pntrlog2bnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
3		pntrlog2bnd.t	$⊢ T = (a \in ℝ ⟼ if (a \in ℝ^{+}, a \log a, 0))$
4		pntrlog2bndlem5.1	$⊢ φ \to B \in ℝ^{+}$
5		pntrlog2bndlem5.2	$⊢ φ \to \forall y \in ℝ^{+} \|\frac{R (y)}{y}\| \leq B$
6		pntrlog2bndlem6.1	$⊢ φ \to A \in ℝ$
7		pntrlog2bndlem6.2	$⊢ φ \to 1 \leq A$
8		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
9	8	adantl	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
12	11	rpred	$⊢ (φ \land x \in (1, +∞)) \to 1 \in ℝ$
13		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
14	13	adantl	$⊢ (φ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
15	14	simpld	$⊢ (φ \land x \in (1, +∞)) \to 1 < x$
16	12 9 15	ltled	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq x$
17	9 11 16	rpgecld	$⊢ (φ \land x \in (1, +∞)) \to x \in ℝ^{+}$
18	10	a1i	$⊢ φ \to 1 \in ℝ^{+}$
19	6 18 7	rpgecld	$⊢ φ \to A \in ℝ^{+}$
20	19	adantr	$⊢ (φ \land x \in (1, +∞)) \to A \in ℝ^{+}$
21	17 20	rpdivcld	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \in ℝ^{+}$
22	21	rprege0d	$⊢ (φ \land x \in (1, +∞)) \to (\frac{x}{A} \in ℝ \land 0 \leq \frac{x}{A})$
23		flge0nn0	$⊢ (\frac{x}{A} \in ℝ \land 0 \leq \frac{x}{A}) \to ⌊\frac{x}{A}⌋ \in ℕ_{0}$
24		nn0p1nn	$⊢ ⌊\frac{x}{A}⌋ \in ℕ_{0} \to ⌊\frac{x}{A}⌋ + 1 \in ℕ$
25	22 23 24	3syl	$⊢ (φ \land x \in (1, +∞)) \to ⌊\frac{x}{A}⌋ + 1 \in ℕ$
26		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
27	25 26	eleqtrdi	$⊢ (φ \land x \in (1, +∞)) \to ⌊\frac{x}{A}⌋ + 1 \in ℤ_{\geq 1}$
28	21	rpred	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \in ℝ$
29	17	rpge0d	$⊢ (φ \land x \in (1, +∞)) \to 0 \leq x$
30	7	adantr	$⊢ (φ \land x \in (1, +∞)) \to 1 \leq A$
31	11 20 9 29 30	lediv2ad	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \leq \frac{x}{1}$
32	9	recnd	$⊢ (φ \land x \in (1, +∞)) \to x \in ℂ$
33	32	div1d	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{1} = x$
34	31 33	breqtrd	$⊢ (φ \land x \in (1, +∞)) \to \frac{x}{A} \leq x$
35		flword2	$⊢ (\frac{x}{A} \in ℝ \land x \in ℝ \land \frac{x}{A} \leq x) \to ⌊x⌋ \in ℤ_{\geq ⌊\frac{x}{A}⌋}$
36	28 9 34 35	syl3anc	$⊢ (φ \land x \in (1, +∞)) \to ⌊x⌋ \in ℤ_{\geq ⌊\frac{x}{A}⌋}$
37		fzsplit2	$⊢ (⌊\frac{x}{A}⌋ + 1 \in ℤ_{\geq 1} \land ⌊x⌋ \in ℤ_{\geq ⌊\frac{x}{A}⌋}) \to (1 \dots ⌊x⌋) = (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$
38	27 36 37	syl2anc	$⊢ (φ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) = (1 \dots ⌊\frac{x}{A}⌋) \cup (⌊\frac{x}{A}⌋ + 1 \dots ⌊x⌋)$

Metamath Proof Explorer

Theorem pntrlog2bndlem6a

Proof