pntlemn

Description: Lemma for pnt . The "naive" base bound, which we will slightly improve. (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}⌋$
	pntlem1.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
Assertion	pntlemn	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to 0 \leq ((\frac{U}{J}) - \|\frac{R (\frac{Z}{J})}{Z}\|) \log J$

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		pntlem1.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
19	7	adantr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to U \in ℝ^{+}$
20	19	rpred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to U \in ℝ$
21		simprl	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to J \in ℕ$
22	20 21	nndivred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{U}{J} \in ℝ$
23	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))$
24	23	simp1d	$⊢ φ \to Z \in ℝ^{+}$
25	24	adantr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Z \in ℝ^{+}$
26	21	nnrpd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to J \in ℝ^{+}$
27	25 26	rpdivcld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{Z}{J} \in ℝ^{+}$
28	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
29	28	ffvelrni	$⊢ \frac{Z}{J} \in ℝ^{+} \to R (\frac{Z}{J}) \in ℝ$
30	27 29	syl	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to R (\frac{Z}{J}) \in ℝ$
31	30 25	rerpdivcld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{R (\frac{Z}{J})}{Z} \in ℝ$
32	31	recnd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{R (\frac{Z}{J})}{Z} \in ℂ$
33	32	abscld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{Z}\| \in ℝ$
34	22 33	resubcld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (\frac{U}{J}) - \|\frac{R (\frac{Z}{J})}{Z}\| \in ℝ$
35	26	relogcld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \log J \in ℝ$
36	30	recnd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to R (\frac{Z}{J}) \in ℂ$
37	25	rpcnne0d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (Z \in ℂ \land Z \neq 0)$
38	26	rpcnne0d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (J \in ℂ \land J \neq 0)$
39		divdiv2	$⊢ (R (\frac{Z}{J}) \in ℂ \land (Z \in ℂ \land Z \neq 0) \land (J \in ℂ \land J \neq 0)) \to \frac{R (\frac{Z}{J})}{\frac{Z}{J}} = \frac{R (\frac{Z}{J}) \cdot J}{Z}$
40	36 37 38 39	syl3anc	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{R (\frac{Z}{J})}{\frac{Z}{J}} = \frac{R (\frac{Z}{J}) \cdot J}{Z}$
41	21	nncnd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to J \in ℂ$
42		div23	$⊢ (R (\frac{Z}{J}) \in ℂ \land J \in ℂ \land (Z \in ℂ \land Z \neq 0)) \to \frac{R (\frac{Z}{J}) \cdot J}{Z} = (\frac{R (\frac{Z}{J})}{Z}) \cdot J$
43	36 41 37 42	syl3anc	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{R (\frac{Z}{J}) \cdot J}{Z} = (\frac{R (\frac{Z}{J})}{Z}) \cdot J$
44	40 43	eqtrd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{R (\frac{Z}{J})}{\frac{Z}{J}} = (\frac{R (\frac{Z}{J})}{Z}) \cdot J$
45	44	fveq2d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{\frac{Z}{J}}\| = \|(\frac{R (\frac{Z}{J})}{Z}) \cdot J\|$
46	32 41	absmuld	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|(\frac{R (\frac{Z}{J})}{Z}) \cdot J\| = \|\frac{R (\frac{Z}{J})}{Z}\| \|J\|$
47	26	rprege0d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (J \in ℝ \land 0 \leq J)$
48		absid	$⊢ (J \in ℝ \land 0 \leq J) \to \|J\| = J$
49	47 48	syl	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|J\| = J$
50	49	oveq2d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{Z}\| \|J\| = \|\frac{R (\frac{Z}{J})}{Z}\| \cdot J$
51	45 46 50	3eqtrd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{\frac{Z}{J}}\| = \|\frac{R (\frac{Z}{J})}{Z}\| \cdot J$
52		fveq2	$⊢ z = \frac{Z}{J} \to R (z) = R (\frac{Z}{J})$
53		id	$⊢ z = \frac{Z}{J} \to z = \frac{Z}{J}$
54	52 53	oveq12d	$⊢ z = \frac{Z}{J} \to \frac{R (z)}{z} = \frac{R (\frac{Z}{J})}{\frac{Z}{J}}$
55	54	fveq2d	$⊢ z = \frac{Z}{J} \to \|\frac{R (z)}{z}\| = \|\frac{R (\frac{Z}{J})}{\frac{Z}{J}}\|$
56	55	breq1d	$⊢ z = \frac{Z}{J} \to (\|\frac{R (z)}{z}\| \leq U \leftrightarrow \|\frac{R (\frac{Z}{J})}{\frac{Z}{J}}\| \leq U)$
57	18	adantr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
58	27	rpred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{Z}{J} \in ℝ$
59		simprr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to J \leq \frac{Z}{Y}$
60	26	rpred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to J \in ℝ$
61	25	rpred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Z \in ℝ$
62	11	simpld	$⊢ φ \to Y \in ℝ^{+}$
63	62	adantr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Y \in ℝ^{+}$
64	60 61 63	lemuldiv2d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (Y \cdot J \leq Z \leftrightarrow J \leq \frac{Z}{Y})$
65	59 64	mpbird	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Y \cdot J \leq Z$
66	63	rpred	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Y \in ℝ$
67	66 61 26	lemuldivd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (Y \cdot J \leq Z \leftrightarrow Y \leq \frac{Z}{J})$
68	65 67	mpbid	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to Y \leq \frac{Z}{J}$
69		elicopnf	$⊢ Y \in ℝ \to (\frac{Z}{J} \in [Y, +∞) \leftrightarrow (\frac{Z}{J} \in ℝ \land Y \leq \frac{Z}{J}))$
70	66 69	syl	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (\frac{Z}{J} \in [Y, +∞) \leftrightarrow (\frac{Z}{J} \in ℝ \land Y \leq \frac{Z}{J}))$
71	58 68 70	mpbir2and	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \frac{Z}{J} \in [Y, +∞)$
72	56 57 71	rspcdva	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{\frac{Z}{J}}\| \leq U$
73	51 72	eqbrtrrd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{Z}\| \cdot J \leq U$
74	33 20 26	lemuldivd	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (\|\frac{R (\frac{Z}{J})}{Z}\| \cdot J \leq U \leftrightarrow \|\frac{R (\frac{Z}{J})}{Z}\| \leq \frac{U}{J})$
75	73 74	mpbid	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \|\frac{R (\frac{Z}{J})}{Z}\| \leq \frac{U}{J}$
76	22 33	subge0d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (0 \leq (\frac{U}{J}) - \|\frac{R (\frac{Z}{J})}{Z}\| \leftrightarrow \|\frac{R (\frac{Z}{J})}{Z}\| \leq \frac{U}{J})$
77	75 76	mpbird	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to 0 \leq (\frac{U}{J}) - \|\frac{R (\frac{Z}{J})}{Z}\|$
78		log1	$⊢ \log 1 = 0$
79		nnge1	$⊢ J \in ℕ \to 1 \leq J$
80	79	ad2antrl	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to 1 \leq J$
81		1rp	$⊢ 1 \in ℝ^{+}$
82		logleb	$⊢ (1 \in ℝ^{+} \land J \in ℝ^{+}) \to (1 \leq J \leftrightarrow \log 1 \leq \log J)$
83	81 26 82	sylancr	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to (1 \leq J \leftrightarrow \log 1 \leq \log J)$
84	80 83	mpbid	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to \log 1 \leq \log J$
85	78 84	eqbrtrrid	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to 0 \leq \log J$
86	34 35 77 85	mulge0d	$⊢ (φ \land (J \in ℕ \land J \leq \frac{Z}{Y})) \to 0 \leq ((\frac{U}{J}) - \|\frac{R (\frac{Z}{J})}{Z}\|) \log J$

Metamath Proof Explorer

Theorem pntlemn

Proof