Theorem pntlemh

Description: Lemma for pnt . Bounds on the subintervals in the induction. (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	pntlemh	|- ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )

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	adantr	|- ( ( ph /\ J e. ( M ... N ) ) -> X e. RR+ )
20	19	relogcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` X ) e. RR )
21	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+ ) ) )
22	21	simp2d	|- ( ph -> K e. RR+ )
23	22	rpred	|- ( ph -> K e. RR )
24	21	simp3d	|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
25	24	simp2d	|- ( ph -> 1 < K )
26	23 25	rplogcld	|- ( ph -> ( log ` K ) e. RR+ )
27	26	adantr	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` K ) e. RR+ )
28	20 27	rerpdivcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( log ` X ) / ( log ` K ) ) e. RR )
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
30	29	simp1d	|- ( ph -> M e. NN )
31	30	adantr	|- ( ( ph /\ J e. ( M ... N ) ) -> M e. NN )
32	31	nnred	|- ( ( ph /\ J e. ( M ... N ) ) -> M e. RR )
33		elfzuz	|- ( J e. ( M ... N ) -> J e. ( ZZ>= ` M ) )
34		eluznn	|- ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN )
35	30 33 34	syl2an	|- ( ( ph /\ J e. ( M ... N ) ) -> J e. NN )
36	35	nnred	|- ( ( ph /\ J e. ( M ... N ) ) -> J e. RR )
37		flltp1	|- ( ( ( log ` X ) / ( log ` K ) ) e. RR -> ( ( log ` X ) / ( log ` K ) ) < ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) )
38	28 37	syl	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( log ` X ) / ( log ` K ) ) < ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) )
39	38 16	breqtrrdi	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( log ` X ) / ( log ` K ) ) < M )
40		elfzle1	|- ( J e. ( M ... N ) -> M <_ J )
41	40	adantl	|- ( ( ph /\ J e. ( M ... N ) ) -> M <_ J )
42	28 32 36 39 41	ltletrd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( log ` X ) / ( log ` K ) ) < J )
43	20 36 27	ltdivmul2d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( ( log ` X ) / ( log ` K ) ) < J <-> ( log ` X ) < ( J x. ( log ` K ) ) ) )
44	42 43	mpbid	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` X ) < ( J x. ( log ` K ) ) )
45	22	adantr	|- ( ( ph /\ J e. ( M ... N ) ) -> K e. RR+ )
46		elfzelz	|- ( J e. ( M ... N ) -> J e. ZZ )
47	46	adantl	|- ( ( ph /\ J e. ( M ... N ) ) -> J e. ZZ )
48		relogexp	|- ( ( K e. RR+ /\ J e. ZZ ) -> ( log ` ( K ^ J ) ) = ( J x. ( log ` K ) ) )
49	45 47 48	syl2anc	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` ( K ^ J ) ) = ( J x. ( log ` K ) ) )
50	44 49	breqtrrd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` X ) < ( log ` ( K ^ J ) ) )
51	45 47	rpexpcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( K ^ J ) e. RR+ )
52		logltb	|- ( ( X e. RR+ /\ ( K ^ J ) e. RR+ ) -> ( X < ( K ^ J ) <-> ( log ` X ) < ( log ` ( K ^ J ) ) ) )
53	19 51 52	syl2anc	|- ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) <-> ( log ` X ) < ( log ` ( K ^ J ) ) ) )
54	50 53	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> X < ( K ^ J ) )
55	49	oveq2d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( 2 x. ( log ` ( K ^ J ) ) ) = ( 2 x. ( J x. ( log ` K ) ) ) )
56		2z	|- 2 e. ZZ
57		relogexp	|- ( ( ( K ^ J ) e. RR+ /\ 2 e. ZZ ) -> ( log ` ( ( K ^ J ) ^ 2 ) ) = ( 2 x. ( log ` ( K ^ J ) ) ) )
58	51 56 57	sylancl	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` ( ( K ^ J ) ^ 2 ) ) = ( 2 x. ( log ` ( K ^ J ) ) ) )
59		2cnd	|- ( ( ph /\ J e. ( M ... N ) ) -> 2 e. CC )
60	36	recnd	|- ( ( ph /\ J e. ( M ... N ) ) -> J e. CC )
61	45	relogcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` K ) e. RR )
62	61	recnd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` K ) e. CC )
63	59 60 62	mulassd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( 2 x. J ) x. ( log ` K ) ) = ( 2 x. ( J x. ( log ` K ) ) ) )
64	55 58 63	3eqtr4d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` ( ( K ^ J ) ^ 2 ) ) = ( ( 2 x. J ) x. ( log ` K ) ) )
65		elfzle2	|- ( J e. ( M ... N ) -> J <_ N )
66	65	adantl	|- ( ( ph /\ J e. ( M ... N ) ) -> J <_ N )
67	66 17	breqtrdi	|- ( ( ph /\ J e. ( M ... N ) ) -> J <_ ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) )
68	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 ) ) ) ) )
69	68	simp1d	|- ( ph -> Z e. RR+ )
70	69	adantr	|- ( ( ph /\ J e. ( M ... N ) ) -> Z e. RR+ )
71	70	relogcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` Z ) e. RR )
72	71 27	rerpdivcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( log ` Z ) / ( log ` K ) ) e. RR )
73	72	rehalfcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) e. RR )
74		flge	|- ( ( ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) e. RR /\ J e. ZZ ) -> ( J <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) <-> J <_ ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) ) )
75	73 47 74	syl2anc	|- ( ( ph /\ J e. ( M ... N ) ) -> ( J <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) <-> J <_ ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) ) )
76	67 75	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> J <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
77		2re	|- 2 e. RR
78	77	a1i	|- ( ( ph /\ J e. ( M ... N ) ) -> 2 e. RR )
79		2pos	|- 0 < 2
80	79	a1i	|- ( ( ph /\ J e. ( M ... N ) ) -> 0 < 2 )
81		lemuldiv2	|- ( ( J e. RR /\ ( ( log ` Z ) / ( log ` K ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. J ) <_ ( ( log ` Z ) / ( log ` K ) ) <-> J <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) )
82	36 72 78 80 81	syl112anc	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( 2 x. J ) <_ ( ( log ` Z ) / ( log ` K ) ) <-> J <_ ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) ) )
83	76 82	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> ( 2 x. J ) <_ ( ( log ` Z ) / ( log ` K ) ) )
84		remulcl	|- ( ( 2 e. RR /\ J e. RR ) -> ( 2 x. J ) e. RR )
85	77 36 84	sylancr	|- ( ( ph /\ J e. ( M ... N ) ) -> ( 2 x. J ) e. RR )
86	85 71 27	lemuldivd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( ( 2 x. J ) x. ( log ` K ) ) <_ ( log ` Z ) <-> ( 2 x. J ) <_ ( ( log ` Z ) / ( log ` K ) ) ) )
87	83 86	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( 2 x. J ) x. ( log ` K ) ) <_ ( log ` Z ) )
88	64 87	eqbrtrd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( log ` ( ( K ^ J ) ^ 2 ) ) <_ ( log ` Z ) )
89		rpexpcl	|- ( ( ( K ^ J ) e. RR+ /\ 2 e. ZZ ) -> ( ( K ^ J ) ^ 2 ) e. RR+ )
90	51 56 89	sylancl	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( K ^ J ) ^ 2 ) e. RR+ )
91	90 70	logled	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( ( K ^ J ) ^ 2 ) <_ Z <-> ( log ` ( ( K ^ J ) ^ 2 ) ) <_ ( log ` Z ) ) )
92	88 91	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( K ^ J ) ^ 2 ) <_ Z )
93	70	rprege0d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( Z e. RR /\ 0 <_ Z ) )
94		resqrtth	|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) ^ 2 ) = Z )
95	93 94	syl	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( sqrt ` Z ) ^ 2 ) = Z )
96	92 95	breqtrrd	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( K ^ J ) ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) )
97	51	rprege0d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( K ^ J ) e. RR /\ 0 <_ ( K ^ J ) ) )
98	70	rpsqrtcld	|- ( ( ph /\ J e. ( M ... N ) ) -> ( sqrt ` Z ) e. RR+ )
99	98	rprege0d	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) )
100		le2sq	|- ( ( ( ( K ^ J ) e. RR /\ 0 <_ ( K ^ J ) ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( ( K ^ J ) <_ ( sqrt ` Z ) <-> ( ( K ^ J ) ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) )
101	97 99 100	syl2anc	|- ( ( ph /\ J e. ( M ... N ) ) -> ( ( K ^ J ) <_ ( sqrt ` Z ) <-> ( ( K ^ J ) ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) )
102	96 101	mpbird	|- ( ( ph /\ J e. ( M ... N ) ) -> ( K ^ J ) <_ ( sqrt ` Z ) )
103	54 102	jca	|- ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )