Theorem pntlemg

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, M is j^* and N is ĵ. (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)}$$
	pntlem1.z	$$⊢\phi \to Z\in \left[W,\mathrm{+\infty }\right)$$
	pntlem1.m	$$⊢M=⌊\frac{\log X}{\log K}⌋+1$$
	pntlem1.n	$$⊢N=⌊\frac{\frac{\log Z}{\log K}}{2}⌋$$
Assertion	pntlemg	$$⊢\phi \to \left(M\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge M}\wedge \frac{\frac{\log Z}{\log K}}{4}\le N-M\right)$$

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		pntlem1.z	$$⊢\phi \to Z\in \left[W,\mathrm{+\infty }\right)$$
16		pntlem1.m	$$⊢M=⌊\frac{\log X}{\log K}⌋+1$$
17		pntlem1.n	$$⊢N=⌊\frac{\frac{\log Z}{\log K}}{2}⌋$$
18	12	simpld	$$⊢\phi \to X\in {ℝ}^{+}$$
19	18	rpred	$$⊢\phi \to X\in ℝ$$
20		1red	$$⊢\phi \to 1\in ℝ$$
21	11	simpld	$$⊢\phi \to Y\in {ℝ}^{+}$$
22	21	rpred	$$⊢\phi \to Y\in ℝ$$
23	11	simprd	$$⊢\phi \to 1\le Y$$
24	12	simprd	$$⊢\phi \to Y<X$$
25	20 22 19 23 24	lelttrd	$$⊢\phi \to 1<X$$
26	19 25	rplogcld	$$⊢\phi \to \log X\in {ℝ}^{+}$$
27	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)$$
28	27	simp2d	$$⊢\phi \to K\in {ℝ}^{+}$$
29	28	rpred	$$⊢\phi \to K\in ℝ$$
30	27	simp3d	$$⊢\phi \to \left(E\in \left(0,1\right)\wedge 1<K\wedge U-E\in {ℝ}^{+}\right)$$
31	30	simp2d	$$⊢\phi \to 1<K$$
32	29 31	rplogcld	$$⊢\phi \to \log K\in {ℝ}^{+}$$
33	26 32	rpdivcld	$$⊢\phi \to \frac{\log X}{\log K}\in {ℝ}^{+}$$
34	33	rprege0d	$$⊢\phi \to \left(\frac{\log X}{\log K}\in ℝ\wedge 0\le \frac{\log X}{\log K}\right)$$
35		flge0nn0	$$⊢\left(\frac{\log X}{\log K}\in ℝ\wedge 0\le \frac{\log X}{\log K}\right)\to ⌊\frac{\log X}{\log K}⌋\in {\mathbb{N}}_0$$
36		nn0p1nn	$$⊢⌊\frac{\log X}{\log K}⌋\in {\mathbb{N}}_0\to ⌊\frac{\log X}{\log K}⌋+1\in \mathbb{N}$$
37	34 35 36	3syl	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋+1\in \mathbb{N}$$
38	16 37	eqeltrid	$$⊢\phi \to M\in \mathbb{N}$$
39	38	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	$$⊢\phi \to \left(Z\in {ℝ}^{+}\wedge \left(1<Z\wedge \mathrm{e}\le \sqrt{Z}\wedge \sqrt{Z}\le \frac{Z}{Y}\right)\wedge \left(\frac{4}{LE}\le \sqrt{Z}\wedge \left(\frac{\log X}{\log K}\right)+2\le \frac{\frac{\log Z}{\log K}}{4}\wedge U\cdot 3+C\le \left(U-E\right)\left(\frac{L{E}^2}{32B}\right)\log Z\right)\right)$$
41	40	simp1d	$$⊢\phi \to Z\in {ℝ}^{+}$$
42	41	relogcld	$$⊢\phi \to \log Z\in ℝ$$
43	42 32	rerpdivcld	$$⊢\phi \to \frac{\log Z}{\log K}\in ℝ$$
44	43	rehalfcld	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{2}\in ℝ$$
45	44	flcld	$$⊢\phi \to ⌊\frac{\frac{\log Z}{\log K}}{2}⌋\in \mathbb{Z}$$
46	17 45	eqeltrid	$$⊢\phi \to N\in \mathbb{Z}$$
47		0red	$$⊢\phi \to 0\in ℝ$$
48		4nn	$$⊢4\in \mathbb{N}$$
49		nndivre	$$⊢\left(\frac{\log Z}{\log K}\in ℝ\wedge 4\in \mathbb{N}\right)\to \frac{\frac{\log Z}{\log K}}{4}\in ℝ$$
50	43 48 49	sylancl	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{4}\in ℝ$$
51	46	zred	$$⊢\phi \to N\in ℝ$$
52	38	nnred	$$⊢\phi \to M\in ℝ$$
53	51 52	resubcld	$$⊢\phi \to N-M\in ℝ$$
54	41	rpred	$$⊢\phi \to Z\in ℝ$$
55	40	simp2d	$$⊢\phi \to \left(1<Z\wedge \mathrm{e}\le \sqrt{Z}\wedge \sqrt{Z}\le \frac{Z}{Y}\right)$$
56	55	simp1d	$$⊢\phi \to 1<Z$$
57	54 56	rplogcld	$$⊢\phi \to \log Z\in {ℝ}^{+}$$
58	57 32	rpdivcld	$$⊢\phi \to \frac{\log Z}{\log K}\in {ℝ}^{+}$$
59		4re	$$⊢4\in ℝ$$
60		4pos	$$⊢0<4$$
61	59 60	elrpii	$$⊢4\in {ℝ}^{+}$$
62		rpdivcl	$$⊢\left(\frac{\log Z}{\log K}\in {ℝ}^{+}\wedge 4\in {ℝ}^{+}\right)\to \frac{\frac{\log Z}{\log K}}{4}\in {ℝ}^{+}$$
63	58 61 62	sylancl	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{4}\in {ℝ}^{+}$$
64	63	rpge0d	$$⊢\phi \to 0\le \frac{\frac{\log Z}{\log K}}{4}$$
65	50	recnd	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{4}\in ℂ$$
66	38	nncnd	$$⊢\phi \to M\in ℂ$$
67		1cnd	$$⊢\phi \to 1\in ℂ$$
68	65 66 67	addassd	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1=\left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1$$
69	52 20	readdcld	$$⊢\phi \to M+1\in ℝ$$
70	50 69	readdcld	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\in ℝ$$
71		peano2re	$$⊢N\in ℝ\to N+1\in ℝ$$
72	51 71	syl	$$⊢\phi \to N+1\in ℝ$$
73	33	rpred	$$⊢\phi \to \frac{\log X}{\log K}\in ℝ$$
74		2re	$$⊢2\in ℝ$$
75	74	a1i	$$⊢\phi \to 2\in ℝ$$
76	73 75	readdcld	$$⊢\phi \to \left(\frac{\log X}{\log K}\right)+2\in ℝ$$
77		reflcl	$$⊢\frac{\log X}{\log K}\in ℝ\to ⌊\frac{\log X}{\log K}⌋\in ℝ$$
78	73 77	syl	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋\in ℝ$$
79	78	recnd	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋\in ℂ$$
80	79 67 67	addassd	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋+1+1=⌊\frac{\log X}{\log K}⌋+1+1$$
81	16	oveq1i	$$⊢M+1=⌊\frac{\log X}{\log K}⌋+1+1$$
82		df-2	$$⊢2=1+1$$
83	82	oveq2i	$$⊢⌊\frac{\log X}{\log K}⌋+2=⌊\frac{\log X}{\log K}⌋+1+1$$
84	80 81 83	3eqtr4g	$$⊢\phi \to M+1=⌊\frac{\log X}{\log K}⌋+2$$
85		flle	$$⊢\frac{\log X}{\log K}\in ℝ\to ⌊\frac{\log X}{\log K}⌋\le \frac{\log X}{\log K}$$
86	73 85	syl	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋\le \frac{\log X}{\log K}$$
87	78 73 75 86	leadd1dd	$$⊢\phi \to ⌊\frac{\log X}{\log K}⌋+2\le \left(\frac{\log X}{\log K}\right)+2$$
88	84 87	eqbrtrd	$$⊢\phi \to M+1\le \left(\frac{\log X}{\log K}\right)+2$$
89	40	simp3d	$$⊢\phi \to \left(\frac{4}{LE}\le \sqrt{Z}\wedge \left(\frac{\log X}{\log K}\right)+2\le \frac{\frac{\log Z}{\log K}}{4}\wedge U\cdot 3+C\le \left(U-E\right)\left(\frac{L{E}^2}{32B}\right)\log Z\right)$$
90	89	simp2d	$$⊢\phi \to \left(\frac{\log X}{\log K}\right)+2\le \frac{\frac{\log Z}{\log K}}{4}$$
91	69 76 50 88 90	letrd	$$⊢\phi \to M+1\le \frac{\frac{\log Z}{\log K}}{4}$$
92	69 50 50 91	leadd2dd	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\le \left(\frac{\frac{\log Z}{\log K}}{4}\right)+\left(\frac{\frac{\log Z}{\log K}}{4}\right)$$
93	43	recnd	$$⊢\phi \to \frac{\log Z}{\log K}\in ℂ$$
94		2cnd	$$⊢\phi \to 2\in ℂ$$
95		2ne0	$$⊢2\ne 0$$
96	95	a1i	$$⊢\phi \to 2\ne 0$$
97	93 94 94 96 96	divdiv1d	$$⊢\phi \to \frac{\frac{\frac{\log Z}{\log K}}{2}}{2}=\frac{\frac{\log Z}{\log K}}{2\cdot 2}$$
98		2t2e4	$$⊢2\cdot 2=4$$
99	98	oveq2i	$$⊢\frac{\frac{\log Z}{\log K}}{2\cdot 2}=\frac{\frac{\log Z}{\log K}}{4}$$
100	97 99	eqtrdi	$$⊢\phi \to \frac{\frac{\frac{\log Z}{\log K}}{2}}{2}=\frac{\frac{\log Z}{\log K}}{4}$$
101	100	oveq2d	$$⊢\phi \to 2\left(\frac{\frac{\frac{\log Z}{\log K}}{2}}{2}\right)=2\left(\frac{\frac{\log Z}{\log K}}{4}\right)$$
102	44	recnd	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{2}\in ℂ$$
103	102 94 96	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{\frac{\log Z}{\log K}}{2}}{2}\right)=\frac{\frac{\log Z}{\log K}}{2}$$
104	65	2timesd	$$⊢\phi \to 2\left(\frac{\frac{\log Z}{\log K}}{4}\right)=\left(\frac{\frac{\log Z}{\log K}}{4}\right)+\left(\frac{\frac{\log Z}{\log K}}{4}\right)$$
105	101 103 104	3eqtr3d	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{2}=\left(\frac{\frac{\log Z}{\log K}}{4}\right)+\left(\frac{\frac{\log Z}{\log K}}{4}\right)$$
106	92 105	breqtrrd	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\le \frac{\frac{\log Z}{\log K}}{2}$$
107		fllep1	$$⊢\frac{\frac{\log Z}{\log K}}{2}\in ℝ\to \frac{\frac{\log Z}{\log K}}{2}\le ⌊\frac{\frac{\log Z}{\log K}}{2}⌋+1$$
108	44 107	syl	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{2}\le ⌊\frac{\frac{\log Z}{\log K}}{2}⌋+1$$
109	17	oveq1i	$$⊢N+1=⌊\frac{\frac{\log Z}{\log K}}{2}⌋+1$$
110	108 109	breqtrrdi	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{2}\le N+1$$
111	70 44 72 106 110	letrd	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\le N+1$$
112	68 111	eqbrtrd	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\le N+1$$
113	50 52	readdcld	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M\in ℝ$$
114	113 51 20	leadd1d	$$⊢\phi \to \left(\left(\frac{\frac{\log Z}{\log K}}{4}\right)+M\le N\leftrightarrow \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M+1\le N+1\right)$$
115	112 114	mpbird	$$⊢\phi \to \left(\frac{\frac{\log Z}{\log K}}{4}\right)+M\le N$$
116		leaddsub	$$⊢\left(\frac{\frac{\log Z}{\log K}}{4}\in ℝ\wedge M\in ℝ\wedge N\in ℝ\right)\to \left(\left(\frac{\frac{\log Z}{\log K}}{4}\right)+M\le N\leftrightarrow \frac{\frac{\log Z}{\log K}}{4}\le N-M\right)$$
117	50 52 51 116	syl3anc	$$⊢\phi \to \left(\left(\frac{\frac{\log Z}{\log K}}{4}\right)+M\le N\leftrightarrow \frac{\frac{\log Z}{\log K}}{4}\le N-M\right)$$
118	115 117	mpbid	$$⊢\phi \to \frac{\frac{\log Z}{\log K}}{4}\le N-M$$
119	47 50 53 64 118	letrd	$$⊢\phi \to 0\le N-M$$
120	51 52	subge0d	$$⊢\phi \to \left(0\le N-M\leftrightarrow M\le N\right)$$
121	119 120	mpbid	$$⊢\phi \to M\le N$$
122		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\le N\right)$$
123	39 46 121 122	syl3anbrc	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
124	38 123 118	3jca	$$⊢\phi \to \left(M\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge M}\wedge \frac{\frac{\log Z}{\log K}}{4}\le N-M\right)$$