Theorem pntibndlem2a

Description: Lemma for pntibndlem2 . (Contributed by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Hypotheses	pntibnd.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
	pntibndlem1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	pntibndlem1.l	$$⊢L=\frac{\frac{1}{4}}{A+3}$$
	pntibndlem3.2	$$⊢\phi \to \forall x\in {ℝ}^{+}\left|\frac{R\left(x\right)}{x}\right|\le A$$
	pntibndlem3.3	$$⊢\phi \to B\in {ℝ}^{+}$$
	pntibndlem3.k	$$⊢K={\mathrm{e}}^{\frac{B}{\frac{E}{2}}}$$
	pntibndlem3.c	$$⊢C=2B+\log 2$$
	pntibndlem3.4	$$⊢\phi \to E\in \left(0,1\right)$$
	pntibndlem3.6	$$⊢\phi \to Z\in {ℝ}^{+}$$
	pntibndlem2.10	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	pntibndlem2a	$$⊢\left(\phi \wedge u\in \left[N,\left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right]\right)\to \left(u\in ℝ\wedge N\le u\wedge u\le \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
2		pntibndlem1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
3		pntibndlem1.l	$$⊢L=\frac{\frac{1}{4}}{A+3}$$
4		pntibndlem3.2	$$⊢\phi \to \forall x\in {ℝ}^{+}\left|\frac{R\left(x\right)}{x}\right|\le A$$
5		pntibndlem3.3	$$⊢\phi \to B\in {ℝ}^{+}$$
6		pntibndlem3.k	$$⊢K={\mathrm{e}}^{\frac{B}{\frac{E}{2}}}$$
7		pntibndlem3.c	$$⊢C=2B+\log 2$$
8		pntibndlem3.4	$$⊢\phi \to E\in \left(0,1\right)$$
9		pntibndlem3.6	$$⊢\phi \to Z\in {ℝ}^{+}$$
10		pntibndlem2.10	$$⊢\phi \to N\in \mathbb{N}$$
11	10	nnred	$$⊢\phi \to N\in ℝ$$
12		1red	$$⊢\phi \to 1\in ℝ$$
13		ioossre	$$⊢\left(0,1\right)\subseteq ℝ$$
14	1 2 3	pntibndlem1	$$⊢\phi \to L\in \left(0,1\right)$$
15	13 14	sselid	$$⊢\phi \to L\in ℝ$$
16	13 8	sselid	$$⊢\phi \to E\in ℝ$$
17	15 16	remulcld	$$⊢\phi \to LE\in ℝ$$
18	12 17	readdcld	$$⊢\phi \to 1+LE\in ℝ$$
19	18 11	remulcld	$$⊢\phi \to \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
20		elicc2	$$⊢\left(N\in ℝ\wedge \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ\right)\to \left(u\in \left[N,\left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right]\leftrightarrow \left(u\in ℝ\wedge N\le u\wedge u\le \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
21	11 19 20	syl2anc	$$⊢\phi \to \left(u\in \left[N,\left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right]\leftrightarrow \left(u\in ℝ\wedge N\le u\wedge u\le \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
22	21	biimpa	$$⊢\left(\phi \wedge u\in \left[N,\left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right]\right)\to \left(u\in ℝ\wedge N\le u\wedge u\le \left(1+LE\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$