Theorem pntlema

Description: Lemma for pnt . Closure for the constants used in the proof. The mammoth expression W is a number large enough to satisfy all the lower bounds needed for Z . For comparison with Equation 10.6.27 of Shapiro, p. 434, Y is x_2, X is x_1, C is the big-O constant in Equation 10.6.29 of Shapiro, p. 435, and W is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of Shapiro, p. 436. (Contributed by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Hypotheses	pntlem1.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
	pntlem1.a	$$⊢\phi \to A\in {ℝ}^{+}$$
	pntlem1.b	$$⊢\phi \to B\in {ℝ}^{+}$$
	pntlem1.l	$$⊢\phi \to L\in \left(0,1\right)$$
	pntlem1.d	$$⊢D=A+1$$
	pntlem1.f	$$⊢F=\left(1-\left(\frac{1}{D}\right)\right)\left(\frac{\frac{L}{32B}}{D^2}\right)$$
	pntlem1.u	$$⊢\phi \to U\in {ℝ}^{+}$$
	pntlem1.u2	$$⊢\phi \to U\le A$$
	pntlem1.e	$$⊢E=\frac{U}{D}$$
	pntlem1.k	$$⊢K={\mathrm{e}}^{\frac{B}{E}}$$
	pntlem1.y	$$⊢\phi \to \left(Y\in {ℝ}^{+}\wedge 1\le Y\right)$$
	pntlem1.x	$$⊢\phi \to \left(X\in {ℝ}^{+}\wedge Y<X\right)$$
	pntlem1.c	$$⊢\phi \to C\in {ℝ}^{+}$$
	pntlem1.w	$$⊢W={\left(Y+\left(\frac{4}{LE}\right)\right)}^2+{X{K}^2}^4+{\mathrm{e}}^{\left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)}$$
Assertion	pntlema	$$⊢\phi \to W\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
2		pntlem1.a	$$⊢\phi \to A\in {ℝ}^{+}$$
3		pntlem1.b	$$⊢\phi \to B\in {ℝ}^{+}$$
4		pntlem1.l	$$⊢\phi \to L\in \left(0,1\right)$$
5		pntlem1.d	$$⊢D=A+1$$
6		pntlem1.f	$$⊢F=\left(1-\left(\frac{1}{D}\right)\right)\left(\frac{\frac{L}{32B}}{D^2}\right)$$
7		pntlem1.u	$$⊢\phi \to U\in {ℝ}^{+}$$
8		pntlem1.u2	$$⊢\phi \to U\le A$$
9		pntlem1.e	$$⊢E=\frac{U}{D}$$
10		pntlem1.k	$$⊢K={\mathrm{e}}^{\frac{B}{E}}$$
11		pntlem1.y	$$⊢\phi \to \left(Y\in {ℝ}^{+}\wedge 1\le Y\right)$$
12		pntlem1.x	$$⊢\phi \to \left(X\in {ℝ}^{+}\wedge Y<X\right)$$
13		pntlem1.c	$$⊢\phi \to C\in {ℝ}^{+}$$
14		pntlem1.w	$$⊢W={\left(Y+\left(\frac{4}{LE}\right)\right)}^2+{X{K}^2}^4+{\mathrm{e}}^{\left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)}$$
15	11	simpld	$$⊢\phi \to Y\in {ℝ}^{+}$$
16		4nn	$$⊢4\in \mathbb{N}$$
17		nnrp	$$⊢4\in \mathbb{N}\to 4\in {ℝ}^{+}$$
18	16 17	ax-mp	$$⊢4\in {ℝ}^{+}$$
19	1 2 3 4 5 6	pntlemd	$$⊢\phi \to \left(L\in {ℝ}^{+}\wedge D\in {ℝ}^{+}\wedge F\in {ℝ}^{+}\right)$$
20	19	simp1d	$$⊢\phi \to L\in {ℝ}^{+}$$
21	1 2 3 4 5 6 7 8 9 10	pntlemc	$$⊢\phi \to \left(E\in {ℝ}^{+}\wedge K\in {ℝ}^{+}\wedge \left(E\in \left(0,1\right)\wedge 1<K\wedge U-E\in {ℝ}^{+}\right)\right)$$
22	21	simp1d	$$⊢\phi \to E\in {ℝ}^{+}$$
23	20 22	rpmulcld	$$⊢\phi \to LE\in {ℝ}^{+}$$
24		rpdivcl	$$⊢\left(4\in {ℝ}^{+}\wedge LE\in {ℝ}^{+}\right)\to \frac{4}{LE}\in {ℝ}^{+}$$
25	18 23 24	sylancr	$$⊢\phi \to \frac{4}{LE}\in {ℝ}^{+}$$
26	15 25	rpaddcld	$$⊢\phi \to Y+\left(\frac{4}{LE}\right)\in {ℝ}^{+}$$
27		2z	$$⊢2\in \mathbb{Z}$$
28		rpexpcl	$$⊢\left(Y+\left(\frac{4}{LE}\right)\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to {\left(Y+\left(\frac{4}{LE}\right)\right)}^2\in {ℝ}^{+}$$
29	26 27 28	sylancl	$$⊢\phi \to {\left(Y+\left(\frac{4}{LE}\right)\right)}^2\in {ℝ}^{+}$$
30	12	simpld	$$⊢\phi \to X\in {ℝ}^{+}$$
31	21	simp2d	$$⊢\phi \to K\in {ℝ}^{+}$$
32		rpexpcl	$$⊢\left(K\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to K^2\in {ℝ}^{+}$$
33	31 27 32	sylancl	$$⊢\phi \to K^2\in {ℝ}^{+}$$
34	30 33	rpmulcld	$$⊢\phi \to X{K}^2\in {ℝ}^{+}$$
35		4z	$$⊢4\in \mathbb{Z}$$
36		rpexpcl	$$⊢\left(X{K}^2\in {ℝ}^{+}\wedge 4\in \mathbb{Z}\right)\to {X{K}^2}^4\in {ℝ}^{+}$$
37	34 35 36	sylancl	$$⊢\phi \to {X{K}^2}^4\in {ℝ}^{+}$$
38		3nn0	$$⊢3\in {\mathbb{N}}_0$$
39		2nn	$$⊢2\in \mathbb{N}$$
40	38 39	decnncl	$$⊢32\in \mathbb{N}$$
41		nnrp	$$⊢32\in \mathbb{N}\to 32\in {ℝ}^{+}$$
42	40 41	ax-mp	$$⊢32\in {ℝ}^{+}$$
43		rpmulcl	$$⊢\left(32\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to 32B\in {ℝ}^{+}$$
44	42 3 43	sylancr	$$⊢\phi \to 32B\in {ℝ}^{+}$$
45	21	simp3d	$$⊢\phi \to \left(E\in \left(0,1\right)\wedge 1<K\wedge U-E\in {ℝ}^{+}\right)$$
46	45	simp3d	$$⊢\phi \to U-E\in {ℝ}^{+}$$
47		rpexpcl	$$⊢\left(E\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to E^2\in {ℝ}^{+}$$
48	22 27 47	sylancl	$$⊢\phi \to E^2\in {ℝ}^{+}$$
49	20 48	rpmulcld	$$⊢\phi \to L{E}^2\in {ℝ}^{+}$$
50	46 49	rpmulcld	$$⊢\phi \to \left(U-E\right)L{E}^2\in {ℝ}^{+}$$
51	44 50	rpdivcld	$$⊢\phi \to \frac{32B}{\left(U-E\right)L{E}^2}\in {ℝ}^{+}$$
52		3rp	$$⊢3\in {ℝ}^{+}$$
53		rpmulcl	$$⊢\left(U\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to U\cdot 3\in {ℝ}^{+}$$
54	7 52 53	sylancl	$$⊢\phi \to U\cdot 3\in {ℝ}^{+}$$
55	54 13	rpaddcld	$$⊢\phi \to U\cdot 3+C\in {ℝ}^{+}$$
56	51 55	rpmulcld	$$⊢\phi \to \left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)\in {ℝ}^{+}$$
57	56	rpred	$$⊢\phi \to \left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)\in ℝ$$
58	57	rpefcld	$$⊢\phi \to {\mathrm{e}}^{\left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)}\in {ℝ}^{+}$$
59	37 58	rpaddcld	$$⊢\phi \to {X{K}^2}^4+{\mathrm{e}}^{\left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)}\in {ℝ}^{+}$$
60	29 59	rpaddcld	$$⊢\phi \to {\left(Y+\left(\frac{4}{LE}\right)\right)}^2+{X{K}^2}^4+{\mathrm{e}}^{\left(\frac{32B}{\left(U-E\right)L{E}^2}\right)\left(U\cdot 3+C\right)}\in {ℝ}^{+}$$
61	14 60	eqeltrid	$$⊢\phi \to W\in {ℝ}^{+}$$