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 \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
	pntlem1.l	$⊢ φ \to L \in (0, 1)$
	pntlem1.d	$⊢ D = A + 1$
	pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
	pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
	pntlem1.u2	$⊢ φ \to U \leq A$
	pntlem1.e	$⊢ E = \frac{U}{D}$
	pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
	pntlem1.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
	pntlem1.x	$⊢ φ \to (X \in ℝ^{+} \land Y < X)$
	pntlem1.c	$⊢ φ \to C \in ℝ^{+}$
	pntlem1.w	$⊢ W = {(Y + (\frac{4}{L E}))}^{2} + {X K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + C)}$
	pntlem1.z	$⊢ φ \to Z \in [W, +∞)$
	pntlem1.m	$⊢ M = ⌊\frac{\log X}{\log K}⌋ + 1$
	pntlem1.n	$⊢ N = ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
Assertion	pntlemh	$⊢ (φ \land J \in (M \dots N)) \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
3		pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
4		pntlem1.l	$⊢ φ \to L \in (0, 1)$
5		pntlem1.d	$⊢ D = A + 1$
6		pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
7		pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
8		pntlem1.u2	$⊢ φ \to U \leq A$
9		pntlem1.e	$⊢ E = \frac{U}{D}$
10		pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
11		pntlem1.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
12		pntlem1.x	$⊢ φ \to (X \in ℝ^{+} \land Y < X)$
13		pntlem1.c	$⊢ φ \to C \in ℝ^{+}$
14		pntlem1.w	$⊢ W = {(Y + (\frac{4}{L E}))}^{2} + {X K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + C)}$
15		pntlem1.z	$⊢ φ \to Z \in [W, +∞)$
16		pntlem1.m	$⊢ M = ⌊\frac{\log X}{\log K}⌋ + 1$
17		pntlem1.n	$⊢ N = ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
18	12	simpld	$⊢ φ \to X \in ℝ^{+}$
19	18	adantr	$⊢ (φ \land J \in (M \dots N)) \to X \in ℝ^{+}$
20	19	relogcld	$⊢ (φ \land J \in (M \dots N)) \to \log X \in ℝ$
21	1 2 3 4 5 6 7 8 9 10	pntlemc	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+}))$
22	21	simp2d	$⊢ φ \to K \in ℝ^{+}$
23	22	rpred	$⊢ φ \to K \in ℝ$
24	21	simp3d	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
25	24	simp2d	$⊢ φ \to 1 < K$
26	23 25	rplogcld	$⊢ φ \to \log K \in ℝ^{+}$
27	26	adantr	$⊢ (φ \land J \in (M \dots N)) \to \log K \in ℝ^{+}$
28	20 27	rerpdivcld	$⊢ (φ \land J \in (M \dots N)) \to \frac{\log X}{\log K} \in ℝ$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	$⊢ φ \to (M \in ℕ \land N \in ℤ_{\geq M} \land \frac{\frac{\log Z}{\log K}}{4} \leq N - M)$
30	29	simp1d	$⊢ φ \to M \in ℕ$
31	30	adantr	$⊢ (φ \land J \in (M \dots N)) \to M \in ℕ$
32	31	nnred	$⊢ (φ \land J \in (M \dots N)) \to M \in ℝ$
33		elfzuz	$⊢ J \in (M \dots N) \to J \in ℤ_{\geq M}$
34		eluznn	$⊢ (M \in ℕ \land J \in ℤ_{\geq M}) \to J \in ℕ$
35	30 33 34	syl2an	$⊢ (φ \land J \in (M \dots N)) \to J \in ℕ$
36	35	nnred	$⊢ (φ \land J \in (M \dots N)) \to J \in ℝ$
37		flltp1	$⊢ \frac{\log X}{\log K} \in ℝ \to \frac{\log X}{\log K} < ⌊\frac{\log X}{\log K}⌋ + 1$
38	28 37	syl	$⊢ (φ \land J \in (M \dots N)) \to \frac{\log X}{\log K} < ⌊\frac{\log X}{\log K}⌋ + 1$
39	38 16	breqtrrdi	$⊢ (φ \land J \in (M \dots N)) \to \frac{\log X}{\log K} < M$
40		elfzle1	$⊢ J \in (M \dots N) \to M \leq J$
41	40	adantl	$⊢ (φ \land J \in (M \dots N)) \to M \leq J$
42	28 32 36 39 41	ltletrd	$⊢ (φ \land J \in (M \dots N)) \to \frac{\log X}{\log K} < J$
43	20 36 27	ltdivmul2d	$⊢ (φ \land J \in (M \dots N)) \to (\frac{\log X}{\log K} < J \leftrightarrow \log X < J \log K)$
44	42 43	mpbid	$⊢ (φ \land J \in (M \dots N)) \to \log X < J \log K$
45	22	adantr	$⊢ (φ \land J \in (M \dots N)) \to K \in ℝ^{+}$
46		elfzelz	$⊢ J \in (M \dots N) \to J \in ℤ$
47	46	adantl	$⊢ (φ \land J \in (M \dots N)) \to J \in ℤ$
48		relogexp	$⊢ (K \in ℝ^{+} \land J \in ℤ) \to \log K^{J} = J \log K$
49	45 47 48	syl2anc	$⊢ (φ \land J \in (M \dots N)) \to \log K^{J} = J \log K$
50	44 49	breqtrrd	$⊢ (φ \land J \in (M \dots N)) \to \log X < \log K^{J}$
51	45 47	rpexpcld	$⊢ (φ \land J \in (M \dots N)) \to K^{J} \in ℝ^{+}$
52		logltb	$⊢ (X \in ℝ^{+} \land K^{J} \in ℝ^{+}) \to (X < K^{J} \leftrightarrow \log X < \log K^{J})$
53	19 51 52	syl2anc	$⊢ (φ \land J \in (M \dots N)) \to (X < K^{J} \leftrightarrow \log X < \log K^{J})$
54	50 53	mpbird	$⊢ (φ \land J \in (M \dots N)) \to X < K^{J}$
55	49	oveq2d	$⊢ (φ \land J \in (M \dots N)) \to 2 \log K^{J} = 2 J \log K$
56		2z	$⊢ 2 \in ℤ$
57		relogexp	$⊢ (K^{J} \in ℝ^{+} \land 2 \in ℤ) \to \log {(K^{J})}^{2} = 2 \log K^{J}$
58	51 56 57	sylancl	$⊢ (φ \land J \in (M \dots N)) \to \log {(K^{J})}^{2} = 2 \log K^{J}$
59		2cnd	$⊢ (φ \land J \in (M \dots N)) \to 2 \in ℂ$
60	36	recnd	$⊢ (φ \land J \in (M \dots N)) \to J \in ℂ$
61	45	relogcld	$⊢ (φ \land J \in (M \dots N)) \to \log K \in ℝ$
62	61	recnd	$⊢ (φ \land J \in (M \dots N)) \to \log K \in ℂ$
63	59 60 62	mulassd	$⊢ (φ \land J \in (M \dots N)) \to 2 \cdot J \log K = 2 J \log K$
64	55 58 63	3eqtr4d	$⊢ (φ \land J \in (M \dots N)) \to \log {(K^{J})}^{2} = 2 \cdot J \log K$
65		elfzle2	$⊢ J \in (M \dots N) \to J \leq N$
66	65	adantl	$⊢ (φ \land J \in (M \dots N)) \to J \leq N$
67	66 17	breqtrdi	$⊢ (φ \land J \in (M \dots N)) \to J \leq ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
68	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	$⊢ φ \to (Z \in ℝ^{+} \land (1 < Z \land e \leq \sqrt{Z} \land \sqrt{Z} \leq \frac{Z}{Y}) \land (\frac{4}{L E} \leq \sqrt{Z} \land (\frac{\log X}{\log K}) + 2 \leq \frac{\frac{\log Z}{\log K}}{4} \land U \cdot 3 + C \leq (U - E) (\frac{L E^{2}}{32 B}) \log Z))$
69	68	simp1d	$⊢ φ \to Z \in ℝ^{+}$
70	69	adantr	$⊢ (φ \land J \in (M \dots N)) \to Z \in ℝ^{+}$
71	70	relogcld	$⊢ (φ \land J \in (M \dots N)) \to \log Z \in ℝ$
72	71 27	rerpdivcld	$⊢ (φ \land J \in (M \dots N)) \to \frac{\log Z}{\log K} \in ℝ$
73	72	rehalfcld	$⊢ (φ \land J \in (M \dots N)) \to \frac{\frac{\log Z}{\log K}}{2} \in ℝ$
74		flge	$⊢ (\frac{\frac{\log Z}{\log K}}{2} \in ℝ \land J \in ℤ) \to (J \leq \frac{\frac{\log Z}{\log K}}{2} \leftrightarrow J \leq ⌊\frac{\frac{\log Z}{\log K}}{2}⌋)$
75	73 47 74	syl2anc	$⊢ (φ \land J \in (M \dots N)) \to (J \leq \frac{\frac{\log Z}{\log K}}{2} \leftrightarrow J \leq ⌊\frac{\frac{\log Z}{\log K}}{2}⌋)$
76	67 75	mpbird	$⊢ (φ \land J \in (M \dots N)) \to J \leq \frac{\frac{\log Z}{\log K}}{2}$
77		2re	$⊢ 2 \in ℝ$
78	77	a1i	$⊢ (φ \land J \in (M \dots N)) \to 2 \in ℝ$
79		2pos	$⊢ 0 < 2$
80	79	a1i	$⊢ (φ \land J \in (M \dots N)) \to 0 < 2$
81		lemuldiv2	$⊢ (J \in ℝ \land \frac{\log Z}{\log K} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 \cdot J \leq \frac{\log Z}{\log K} \leftrightarrow J \leq \frac{\frac{\log Z}{\log K}}{2})$
82	36 72 78 80 81	syl112anc	$⊢ (φ \land J \in (M \dots N)) \to (2 \cdot J \leq \frac{\log Z}{\log K} \leftrightarrow J \leq \frac{\frac{\log Z}{\log K}}{2})$
83	76 82	mpbird	$⊢ (φ \land J \in (M \dots N)) \to 2 \cdot J \leq \frac{\log Z}{\log K}$
84		remulcl	$⊢ (2 \in ℝ \land J \in ℝ) \to 2 \cdot J \in ℝ$
85	77 36 84	sylancr	$⊢ (φ \land J \in (M \dots N)) \to 2 \cdot J \in ℝ$
86	85 71 27	lemuldivd	$⊢ (φ \land J \in (M \dots N)) \to (2 \cdot J \log K \leq \log Z \leftrightarrow 2 \cdot J \leq \frac{\log Z}{\log K})$
87	83 86	mpbird	$⊢ (φ \land J \in (M \dots N)) \to 2 \cdot J \log K \leq \log Z$
88	64 87	eqbrtrd	$⊢ (φ \land J \in (M \dots N)) \to \log {(K^{J})}^{2} \leq \log Z$
89		rpexpcl	$⊢ (K^{J} \in ℝ^{+} \land 2 \in ℤ) \to {(K^{J})}^{2} \in ℝ^{+}$
90	51 56 89	sylancl	$⊢ (φ \land J \in (M \dots N)) \to {(K^{J})}^{2} \in ℝ^{+}$
91	90 70	logled	$⊢ (φ \land J \in (M \dots N)) \to ({(K^{J})}^{2} \leq Z \leftrightarrow \log {(K^{J})}^{2} \leq \log Z)$
92	88 91	mpbird	$⊢ (φ \land J \in (M \dots N)) \to {(K^{J})}^{2} \leq Z$
93	70	rprege0d	$⊢ (φ \land J \in (M \dots N)) \to (Z \in ℝ \land 0 \leq Z)$
94		resqrtth	$⊢ (Z \in ℝ \land 0 \leq Z) \to {\sqrt{Z}}^{2} = Z$
95	93 94	syl	$⊢ (φ \land J \in (M \dots N)) \to {\sqrt{Z}}^{2} = Z$
96	92 95	breqtrrd	$⊢ (φ \land J \in (M \dots N)) \to {(K^{J})}^{2} \leq {\sqrt{Z}}^{2}$
97	51	rprege0d	$⊢ (φ \land J \in (M \dots N)) \to (K^{J} \in ℝ \land 0 \leq K^{J})$
98	70	rpsqrtcld	$⊢ (φ \land J \in (M \dots N)) \to \sqrt{Z} \in ℝ^{+}$
99	98	rprege0d	$⊢ (φ \land J \in (M \dots N)) \to (\sqrt{Z} \in ℝ \land 0 \leq \sqrt{Z})$
100		le2sq	$⊢ ((K^{J} \in ℝ \land 0 \leq K^{J}) \land (\sqrt{Z} \in ℝ \land 0 \leq \sqrt{Z})) \to (K^{J} \leq \sqrt{Z} \leftrightarrow {(K^{J})}^{2} \leq {\sqrt{Z}}^{2})$
101	97 99 100	syl2anc	$⊢ (φ \land J \in (M \dots N)) \to (K^{J} \leq \sqrt{Z} \leftrightarrow {(K^{J})}^{2} \leq {\sqrt{Z}}^{2})$
102	96 101	mpbird	$⊢ (φ \land J \in (M \dots N)) \to K^{J} \leq \sqrt{Z}$
103	54 102	jca	$⊢ (φ \land J \in (M \dots N)) \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$

Metamath Proof Explorer

Theorem pntlemh

Proof