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 = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
	pntlem1.a	|- ( ph -> A e. RR+ )
	pntlem1.b	|- ( ph -> B e. RR+ )
	pntlem1.l	|- ( ph -> L e. ( 0 (,) 1 ) )
	pntlem1.d	|- D = ( A + 1 )
	pntlem1.f	|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
	pntlem1.u	|- ( ph -> U e. RR+ )
	pntlem1.u2	|- ( ph -> U <_ A )
	pntlem1.e	|- E = ( U / D )
	pntlem1.k	|- K = ( exp ` ( B / E ) )
	pntlem1.y	|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
	pntlem1.x	|- ( ph -> ( X e. RR+ /\ Y < X ) )
	pntlem1.c	|- ( ph -> C e. RR+ )
	pntlem1.w	|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
	pntlem1.z	|- ( ph -> Z e. ( W [,) +oo ) )
	pntlem1.m	|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
	pntlem1.n	|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
Assertion	pntlemg	|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		pntlem1.a	|- ( ph -> A e. RR+ )
3		pntlem1.b	|- ( ph -> B e. RR+ )
4		pntlem1.l	|- ( ph -> L e. ( 0 (,) 1 ) )
5		pntlem1.d	|- D = ( A + 1 )
6		pntlem1.f	|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7		pntlem1.u	|- ( ph -> U e. RR+ )
8		pntlem1.u2	|- ( ph -> U <_ A )
9		pntlem1.e	|- E = ( U / D )
10		pntlem1.k	|- K = ( exp ` ( B / E ) )
11		pntlem1.y	|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12		pntlem1.x	|- ( ph -> ( X e. RR+ /\ Y < X ) )
13		pntlem1.c	|- ( ph -> C e. RR+ )
14		pntlem1.w	|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15		pntlem1.z	|- ( ph -> Z e. ( W [,) +oo ) )
16		pntlem1.m	|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
17		pntlem1.n	|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
18	12	simpld	|- ( ph -> X e. RR+ )
19	18	rpred	|- ( ph -> X e. RR )
20		1red	|- ( ph -> 1 e. RR )
21	11	simpld	|- ( ph -> Y e. RR+ )
22	21	rpred	|- ( ph -> Y e. RR )
23	11	simprd	|- ( ph -> 1 <_ Y )
24	12	simprd	|- ( ph -> Y < X )
25	20 22 19 23 24	lelttrd	|- ( ph -> 1 < X )
26	19 25	rplogcld	|- ( ph -> ( log ` X ) e. RR+ )
27	1 2 3 4 5 6 7 8 9 10	pntlemc	|- ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
28	27	simp2d	|- ( ph -> K e. RR+ )
29	28	rpred	|- ( ph -> K e. RR )
30	27	simp3d	|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
31	30	simp2d	|- ( ph -> 1 < K )
32	29 31	rplogcld	|- ( ph -> ( log ` K ) e. RR+ )
33	26 32	rpdivcld	|- ( ph -> ( ( log ` X ) / ( log ` K ) ) e. RR+ )
34	33	rprege0d	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) e. RR /\ 0 <_ ( ( log ` X ) / ( log ` K ) ) ) )
35		flge0nn0	|- ( ( ( ( log ` X ) / ( log ` K ) ) e. RR /\ 0 <_ ( ( log ` X ) / ( log ` K ) ) ) -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) e. NN0 )
36		nn0p1nn	|- ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) e. NN0 -> ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) e. NN )
37	34 35 36	3syl	|- ( ph -> ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) e. NN )
38	16 37	eqeltrid	|- ( ph -> M e. NN )
39	38	nnzd	|- ( ph -> M e. ZZ )
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
41	40	simp1d	|- ( ph -> Z e. RR+ )
42	41	relogcld	|- ( ph -> ( log ` Z ) e. RR )
43	42 32	rerpdivcld	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR )
44	43	rehalfcld	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) e. RR )
45	44	flcld	|- ( ph -> ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) e. ZZ )
46	17 45	eqeltrid	|- ( ph -> N e. ZZ )
47		0red	|- ( ph -> 0 e. RR )
48		4nn	|- 4 e. NN
49		nndivre	|- ( ( ( ( log ` Z ) / ( log ` K ) ) e. RR /\ 4 e. NN ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
50	43 48 49	sylancl	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
51	46	zred	|- ( ph -> N e. RR )
52	38	nnred	|- ( ph -> M e. RR )
53	51 52	resubcld	|- ( ph -> ( N - M ) e. RR )
54	41	rpred	|- ( ph -> Z e. RR )
55	40	simp2d	|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
56	55	simp1d	|- ( ph -> 1 < Z )
57	54 56	rplogcld	|- ( ph -> ( log ` Z ) e. RR+ )
58	57 32	rpdivcld	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR+ )
59		4re	|- 4 e. RR
60		4pos	|- 0 < 4
61	59 60	elrpii	|- 4 e. RR+
62		rpdivcl	|- ( ( ( ( log ` Z ) / ( log ` K ) ) e. RR+ /\ 4 e. RR+ ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR+ )
63	58 61 62	sylancl	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR+ )
64	63	rpge0d	|- ( ph -> 0 <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
65	50	recnd	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. CC )
66	38	nncnd	|- ( ph -> M e. CC )
67		1cnd	|- ( ph -> 1 e. CC )
68	65 66 67	addassd	|- ( ph -> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) + 1 ) = ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( M + 1 ) ) )
69	52 20	readdcld	|- ( ph -> ( M + 1 ) e. RR )
70	50 69	readdcld	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( M + 1 ) ) e. RR )
71		peano2re	|- ( N e. RR -> ( N + 1 ) e. RR )
72	51 71	syl	|- ( ph -> ( N + 1 ) e. RR )
73	33	rpred	|- ( ph -> ( ( log ` X ) / ( log ` K ) ) e. RR )
74		2re	|- 2 e. RR
75	74	a1i	|- ( ph -> 2 e. RR )
76	73 75	readdcld	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) e. RR )
77		reflcl	|- ( ( ( log ` X ) / ( log ` K ) ) e. RR -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) e. RR )
78	73 77	syl	|- ( ph -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) e. RR )
79	78	recnd	|- ( ph -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) e. CC )
80	79 67 67	addassd	|- ( ph -> ( ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) + 1 ) = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + ( 1 + 1 ) ) )
81	16	oveq1i	|- ( M + 1 ) = ( ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) + 1 )
82		df-2	|- 2 = ( 1 + 1 )
83	82	oveq2i	|- ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 2 ) = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + ( 1 + 1 ) )
84	80 81 83	3eqtr4g	|- ( ph -> ( M + 1 ) = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 2 ) )
85		flle	|- ( ( ( log ` X ) / ( log ` K ) ) e. RR -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) <_ ( ( log ` X ) / ( log ` K ) ) )
86	73 85	syl	|- ( ph -> ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) <_ ( ( log ` X ) / ( log ` K ) ) )
87	78 73 75 86	leadd1dd	|- ( ph -> ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 2 ) <_ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
88	84 87	eqbrtrd	|- ( ph -> ( M + 1 ) <_ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
89	40	simp3d	|- ( ph -> ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) )
90	89	simp2d	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
91	69 76 50 88 90	letrd	|- ( ph -> ( M + 1 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
92	69 50 50 91	leadd2dd	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( M + 1 ) ) <_ ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) )
93	43	recnd	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. CC )
94		2cnd	|- ( ph -> 2 e. CC )
95		2ne0	|- 2 =/= 0
96	95	a1i	|- ( ph -> 2 =/= 0 )
97	93 94 94 96 96	divdiv1d	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) / 2 ) = ( ( ( log ` Z ) / ( log ` K ) ) / ( 2 x. 2 ) ) )
98		2t2e4	|- ( 2 x. 2 ) = 4
99	98	oveq2i	|- ( ( ( log ` Z ) / ( log ` K ) ) / ( 2 x. 2 ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 )
100	97 99	eqtrdi	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) / 2 ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
101	100	oveq2d	|- ( ph -> ( 2 x. ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) / 2 ) ) = ( 2 x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) )
102	44	recnd	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) e. CC )
103	102 94 96	divcan2d	|- ( ph -> ( 2 x. ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) / 2 ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
104	65	2timesd	|- ( ph -> ( 2 x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) )
105	101 103 104	3eqtr3d	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) = ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) )
106	92 105	breqtrrd	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( M + 1 ) ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
107		fllep1	|- ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) e. RR -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) <_ ( ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) + 1 ) )
108	44 107	syl	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) <_ ( ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) + 1 ) )
109	17	oveq1i	|- ( N + 1 ) = ( ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) + 1 )
110	108 109	breqtrrdi	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) <_ ( N + 1 ) )
111	70 44 72 106 110	letrd	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + ( M + 1 ) ) <_ ( N + 1 ) )
112	68 111	eqbrtrd	|- ( ph -> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) + 1 ) <_ ( N + 1 ) )
113	50 52	readdcld	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) e. RR )
114	113 51 20	leadd1d	|- ( ph -> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) <_ N <-> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) + 1 ) <_ ( N + 1 ) ) )
115	112 114	mpbird	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) <_ N )
116		leaddsub	|- ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR /\ M e. RR /\ N e. RR ) -> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) <_ N <-> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
117	50 52 51 116	syl3anc	|- ( ph -> ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) + M ) <_ N <-> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
118	115 117	mpbid	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) )
119	47 50 53 64 118	letrd	|- ( ph -> 0 <_ ( N - M ) )
120	51 52	subge0d	|- ( ph -> ( 0 <_ ( N - M ) <-> M <_ N ) )
121	119 120	mpbid	|- ( ph -> M <_ N )
122		eluz2	|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
123	39 46 121 122	syl3anbrc	|- ( ph -> N e. ( ZZ>= ` M ) )
124	38 123 118	3jca	|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )