chtppilimlem1

	Ref	Expression
Hypotheses	chtppilim.1	$⊢ φ \to A \in ℝ^{+}$
	chtppilim.2	$⊢ φ \to A < 1$
	chtppilim.3	$⊢ φ \to N \in [2, +∞)$
	chtppilim.4	$⊢ φ \to \frac{N^{A}}{\underline{π} (N)} < 1 - A$
Assertion	chtppilimlem1	$⊢ φ \to A^{2} \underline{π} (N) \log N < θ (N)$

Proof

Step	Hyp	Ref	Expression
1		chtppilim.1	$⊢ φ \to A \in ℝ^{+}$
2		chtppilim.2	$⊢ φ \to A < 1$
3		chtppilim.3	$⊢ φ \to N \in [2, +∞)$
4		chtppilim.4	$⊢ φ \to \frac{N^{A}}{\underline{π} (N)} < 1 - A$
5	1	rpred	$⊢ φ \to A \in ℝ$
6	5	recnd	$⊢ φ \to A \in ℂ$
7	6	sqvald	$⊢ φ \to A^{2} = A A$
8	7	oveq1d	$⊢ φ \to A^{2} \underline{π} (N) \log N = A A \underline{π} (N) \log N$
9		2re	$⊢ 2 \in ℝ$
10		elicopnf	$⊢ 2 \in ℝ \to (N \in [2, +∞) \leftrightarrow (N \in ℝ \land 2 \leq N))$
11	9 10	ax-mp	$⊢ N \in [2, +∞) \leftrightarrow (N \in ℝ \land 2 \leq N)$
12	3 11	sylib	$⊢ φ \to (N \in ℝ \land 2 \leq N)$
13	12	simpld	$⊢ φ \to N \in ℝ$
14		ppicl	$⊢ N \in ℝ \to \underline{π} (N) \in ℕ_{0}$
15	13 14	syl	$⊢ φ \to \underline{π} (N) \in ℕ_{0}$
16	15	nn0red	$⊢ φ \to \underline{π} (N) \in ℝ$
17	16	recnd	$⊢ φ \to \underline{π} (N) \in ℂ$
18		0red	$⊢ φ \to 0 \in ℝ$
19	9	a1i	$⊢ φ \to 2 \in ℝ$
20		2pos	$⊢ 0 < 2$
21	20	a1i	$⊢ φ \to 0 < 2$
22	12	simprd	$⊢ φ \to 2 \leq N$
23	18 19 13 21 22	ltletrd	$⊢ φ \to 0 < N$
24	13 23	elrpd	$⊢ φ \to N \in ℝ^{+}$
25	24	relogcld	$⊢ φ \to \log N \in ℝ$
26	25	recnd	$⊢ φ \to \log N \in ℂ$
27	6 6 17 26	mul4d	$⊢ φ \to A A \underline{π} (N) \log N = A \underline{π} (N) A \log N$
28	8 27	eqtrd	$⊢ φ \to A^{2} \underline{π} (N) \log N = A \underline{π} (N) A \log N$
29	5 16	remulcld	$⊢ φ \to A \underline{π} (N) \in ℝ$
30	5 25	remulcld	$⊢ φ \to A \log N \in ℝ$
31	29 30	remulcld	$⊢ φ \to A \underline{π} (N) A \log N \in ℝ$
32	24 5	rpcxpcld	$⊢ φ \to N^{A} \in ℝ^{+}$
33	32	rpred	$⊢ φ \to N^{A} \in ℝ$
34		ppicl	$⊢ N^{A} \in ℝ \to \underline{π} (N^{A}) \in ℕ_{0}$
35	33 34	syl	$⊢ φ \to \underline{π} (N^{A}) \in ℕ_{0}$
36	35	nn0red	$⊢ φ \to \underline{π} (N^{A}) \in ℝ$
37	16 36	resubcld	$⊢ φ \to \underline{π} (N) - \underline{π} (N^{A}) \in ℝ$
38	37 30	remulcld	$⊢ φ \to (\underline{π} (N) - \underline{π} (N^{A})) A \log N \in ℝ$
39		chtcl	$⊢ N \in ℝ \to θ (N) \in ℝ$
40	13 39	syl	$⊢ φ \to θ (N) \in ℝ$
41		1red	$⊢ φ \to 1 \in ℝ$
42		1lt2	$⊢ 1 < 2$
43	42	a1i	$⊢ φ \to 1 < 2$
44	41 19 13 43 22	ltletrd	$⊢ φ \to 1 < N$
45	13 44	rplogcld	$⊢ φ \to \log N \in ℝ^{+}$
46	1 45	rpmulcld	$⊢ φ \to A \log N \in ℝ^{+}$
47	16 33	resubcld	$⊢ φ \to \underline{π} (N) - N^{A} \in ℝ$
48		ppinncl	$⊢ (N \in ℝ \land 2 \leq N) \to \underline{π} (N) \in ℕ$
49	12 48	syl	$⊢ φ \to \underline{π} (N) \in ℕ$
50	33 49	nndivred	$⊢ φ \to \frac{N^{A}}{\underline{π} (N)} \in ℝ$
51	50 41 5 4	ltsub13d	$⊢ φ \to A < 1 - (\frac{N^{A}}{\underline{π} (N)})$
52	33	recnd	$⊢ φ \to N^{A} \in ℂ$
53	49	nnrpd	$⊢ φ \to \underline{π} (N) \in ℝ^{+}$
54	53	rpcnne0d	$⊢ φ \to (\underline{π} (N) \in ℂ \land \underline{π} (N) \neq 0)$
55		divsubdir	$⊢ (\underline{π} (N) \in ℂ \land N^{A} \in ℂ \land (\underline{π} (N) \in ℂ \land \underline{π} (N) \neq 0)) \to \frac{\underline{π} (N) - N^{A}}{\underline{π} (N)} = (\frac{\underline{π} (N)}{\underline{π} (N)}) - (\frac{N^{A}}{\underline{π} (N)})$
56	17 52 54 55	syl3anc	$⊢ φ \to \frac{\underline{π} (N) - N^{A}}{\underline{π} (N)} = (\frac{\underline{π} (N)}{\underline{π} (N)}) - (\frac{N^{A}}{\underline{π} (N)})$
57		divid	$⊢ (\underline{π} (N) \in ℂ \land \underline{π} (N) \neq 0) \to \frac{\underline{π} (N)}{\underline{π} (N)} = 1$
58	54 57	syl	$⊢ φ \to \frac{\underline{π} (N)}{\underline{π} (N)} = 1$
59	58	oveq1d	$⊢ φ \to (\frac{\underline{π} (N)}{\underline{π} (N)}) - (\frac{N^{A}}{\underline{π} (N)}) = 1 - (\frac{N^{A}}{\underline{π} (N)})$
60	56 59	eqtrd	$⊢ φ \to \frac{\underline{π} (N) - N^{A}}{\underline{π} (N)} = 1 - (\frac{N^{A}}{\underline{π} (N)})$
61	51 60	breqtrrd	$⊢ φ \to A < \frac{\underline{π} (N) - N^{A}}{\underline{π} (N)}$
62	5 47 53	ltmuldivd	$⊢ φ \to (A \underline{π} (N) < \underline{π} (N) - N^{A} \leftrightarrow A < \frac{\underline{π} (N) - N^{A}}{\underline{π} (N)})$
63	61 62	mpbird	$⊢ φ \to A \underline{π} (N) < \underline{π} (N) - N^{A}$
64		ppiltx	$⊢ N^{A} \in ℝ^{+} \to \underline{π} (N^{A}) < N^{A}$
65	32 64	syl	$⊢ φ \to \underline{π} (N^{A}) < N^{A}$
66	36 33 16 65	ltsub2dd	$⊢ φ \to \underline{π} (N) - N^{A} < \underline{π} (N) - \underline{π} (N^{A})$
67	29 47 37 63 66	lttrd	$⊢ φ \to A \underline{π} (N) < \underline{π} (N) - \underline{π} (N^{A})$
68	29 37 46 67	ltmul1dd	$⊢ φ \to A \underline{π} (N) A \log N < (\underline{π} (N) - \underline{π} (N^{A})) A \log N$
69		fzfid	$⊢ φ \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \in Fin$
70		inss1	$⊢ (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \subseteq (⌊N^{A}⌋ + 1 \dots ⌊N⌋)$
71		ssfi	$⊢ ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \in Fin \land (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \subseteq (⌊N^{A}⌋ + 1 \dots ⌊N⌋)) \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \in Fin$
72	69 70 71	sylancl	$⊢ φ \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \in Fin$
73		simpr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)$
74	73	elin2d	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℙ$
75		prmnn	$⊢ p \in ℙ \to p \in ℕ$
76	75	nnrpd	$⊢ p \in ℙ \to p \in ℝ^{+}$
77	74 76	syl	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℝ^{+}$
78	77	relogcld	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to \log p \in ℝ$
79	72 78	fsumrecl	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} \log p \in ℝ$
80	30	recnd	$⊢ φ \to A \log N \in ℂ$
81		fsumconst	$⊢ ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \in Fin \land A \log N \in ℂ) \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} A \log N = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\| A \log N$
82	72 80 81	syl2anc	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} A \log N = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\| A \log N$
83		ppifl	$⊢ N \in ℝ \to \underline{π} (⌊N⌋) = \underline{π} (N)$
84	13 83	syl	$⊢ φ \to \underline{π} (⌊N⌋) = \underline{π} (N)$
85		ppifl	$⊢ N^{A} \in ℝ \to \underline{π} (⌊N^{A}⌋) = \underline{π} (N^{A})$
86	33 85	syl	$⊢ φ \to \underline{π} (⌊N^{A}⌋) = \underline{π} (N^{A})$
87	84 86	oveq12d	$⊢ φ \to \underline{π} (⌊N⌋) - \underline{π} (⌊N^{A}⌋) = \underline{π} (N) - \underline{π} (N^{A})$
88	41 13 44	ltled	$⊢ φ \to 1 \leq N$
89		1re	$⊢ 1 \in ℝ$
90		ltle	$⊢ (A \in ℝ \land 1 \in ℝ) \to (A < 1 \to A \leq 1)$
91	5 89 90	sylancl	$⊢ φ \to (A < 1 \to A \leq 1)$
92	2 91	mpd	$⊢ φ \to A \leq 1$
93	13 88 5 41 92	cxplead	$⊢ φ \to N^{A} \leq N^{1}$
94	13	recnd	$⊢ φ \to N \in ℂ$
95	94	cxp1d	$⊢ φ \to N^{1} = N$
96	93 95	breqtrd	$⊢ φ \to N^{A} \leq N$
97		flword2	$⊢ (N^{A} \in ℝ \land N \in ℝ \land N^{A} \leq N) \to ⌊N⌋ \in ℤ_{\geq ⌊N^{A}⌋}$
98	33 13 96 97	syl3anc	$⊢ φ \to ⌊N⌋ \in ℤ_{\geq ⌊N^{A}⌋}$
99		ppidif	$⊢ ⌊N⌋ \in ℤ_{\geq ⌊N^{A}⌋} \to \underline{π} (⌊N⌋) - \underline{π} (⌊N^{A}⌋) = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\|$
100	98 99	syl	$⊢ φ \to \underline{π} (⌊N⌋) - \underline{π} (⌊N^{A}⌋) = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\|$
101	87 100	eqtr3d	$⊢ φ \to \underline{π} (N) - \underline{π} (N^{A}) = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\|$
102	101	oveq1d	$⊢ φ \to (\underline{π} (N) - \underline{π} (N^{A})) A \log N = \|(⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ\| A \log N$
103	82 102	eqtr4d	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} A \log N = (\underline{π} (N) - \underline{π} (N^{A})) A \log N$
104	30	adantr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to A \log N \in ℝ$
105	33	adantr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to N^{A} \in ℝ$
106		reflcl	$⊢ N^{A} \in ℝ \to ⌊N^{A}⌋ \in ℝ$
107		peano2re	$⊢ ⌊N^{A}⌋ \in ℝ \to ⌊N^{A}⌋ + 1 \in ℝ$
108	33 106 107	3syl	$⊢ φ \to ⌊N^{A}⌋ + 1 \in ℝ$
109	108	adantr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to ⌊N^{A}⌋ + 1 \in ℝ$
110	77	rpred	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℝ$
111		fllep1	$⊢ N^{A} \in ℝ \to N^{A} \leq ⌊N^{A}⌋ + 1$
112	33 111	syl	$⊢ φ \to N^{A} \leq ⌊N^{A}⌋ + 1$
113	112	adantr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to N^{A} \leq ⌊N^{A}⌋ + 1$
114	73	elin1d	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋)$
115		elfzle1	$⊢ p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \to ⌊N^{A}⌋ + 1 \leq p$
116	114 115	syl	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to ⌊N^{A}⌋ + 1 \leq p$
117	105 109 110 113 116	letrd	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to N^{A} \leq p$
118	24	rpne0d	$⊢ φ \to N \neq 0$
119	94 118 6	cxpefd	$⊢ φ \to N^{A} = e^{A \log N}$
120	119	eqcomd	$⊢ φ \to e^{A \log N} = N^{A}$
121	120	adantr	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to e^{A \log N} = N^{A}$
122	77	reeflogd	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to e^{\log p} = p$
123	117 121 122	3brtr4d	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to e^{A \log N} \leq e^{\log p}$
124		efle	$⊢ (A \log N \in ℝ \land \log p \in ℝ) \to (A \log N \leq \log p \leftrightarrow e^{A \log N} \leq e^{\log p})$
125	104 78 124	syl2anc	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to (A \log N \leq \log p \leftrightarrow e^{A \log N} \leq e^{\log p})$
126	123 125	mpbird	$⊢ (φ \land p \in ((⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ)) \to A \log N \leq \log p$
127	72 104 78 126	fsumle	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} A \log N \leq \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} \log p$
128	103 127	eqbrtrrd	$⊢ φ \to (\underline{π} (N) - \underline{π} (N^{A})) A \log N \leq \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} \log p$
129		fzfid	$⊢ φ \to (1 \dots ⌊N⌋) \in Fin$
130		inss1	$⊢ (1 \dots ⌊N⌋) \cap ℙ \subseteq (1 \dots ⌊N⌋)$
131		ssfi	$⊢ ((1 \dots ⌊N⌋) \in Fin \land (1 \dots ⌊N⌋) \cap ℙ \subseteq (1 \dots ⌊N⌋)) \to (1 \dots ⌊N⌋) \cap ℙ \in Fin$
132	129 130 131	sylancl	$⊢ φ \to (1 \dots ⌊N⌋) \cap ℙ \in Fin$
133		simpr	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to p \in ((1 \dots ⌊N⌋) \cap ℙ)$
134	133	elin2d	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℙ$
135		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
136	134 135	syl	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℤ_{\geq 2}$
137		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
138	136 137	sylib	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to (p \in ℕ \land 1 < p)$
139	138	simpld	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℕ$
140	139	nnred	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to p \in ℝ$
141	138	simprd	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to 1 < p$
142	140 141	rplogcld	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to \log p \in ℝ^{+}$
143	142	rpred	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to \log p \in ℝ$
144	142	rpge0d	$⊢ (φ \land p \in ((1 \dots ⌊N⌋) \cap ℙ)) \to 0 \leq \log p$
145	32	rpge0d	$⊢ φ \to 0 \leq N^{A}$
146		flge0nn0	$⊢ (N^{A} \in ℝ \land 0 \leq N^{A}) \to ⌊N^{A}⌋ \in ℕ_{0}$
147	33 145 146	syl2anc	$⊢ φ \to ⌊N^{A}⌋ \in ℕ_{0}$
148		nn0p1nn	$⊢ ⌊N^{A}⌋ \in ℕ_{0} \to ⌊N^{A}⌋ + 1 \in ℕ$
149	147 148	syl	$⊢ φ \to ⌊N^{A}⌋ + 1 \in ℕ$
150		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
151	149 150	eleqtrdi	$⊢ φ \to ⌊N^{A}⌋ + 1 \in ℤ_{\geq 1}$
152		fzss1	$⊢ ⌊N^{A}⌋ + 1 \in ℤ_{\geq 1} \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \subseteq (1 \dots ⌊N⌋)$
153		ssrin	$⊢ (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \subseteq (1 \dots ⌊N⌋) \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \subseteq (1 \dots ⌊N⌋) \cap ℙ$
154	151 152 153	3syl	$⊢ φ \to (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ \subseteq (1 \dots ⌊N⌋) \cap ℙ$
155	132 143 144 154	fsumless	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} \log p \leq \sum_{p \in (1 \dots ⌊N⌋) \cap ℙ} \log p$
156		chtval	$⊢ N \in ℝ \to θ (N) = \sum_{p \in [0, N] \cap ℙ} \log p$
157	13 156	syl	$⊢ φ \to θ (N) = \sum_{p \in [0, N] \cap ℙ} \log p$
158		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
159		ppisval2	$⊢ (N \in ℝ \land 2 \in ℤ_{\geq 1}) \to [0, N] \cap ℙ = (1 \dots ⌊N⌋) \cap ℙ$
160	13 158 159	sylancl	$⊢ φ \to [0, N] \cap ℙ = (1 \dots ⌊N⌋) \cap ℙ$
161	160	sumeq1d	$⊢ φ \to \sum_{p \in [0, N] \cap ℙ} \log p = \sum_{p \in (1 \dots ⌊N⌋) \cap ℙ} \log p$
162	157 161	eqtrd	$⊢ φ \to θ (N) = \sum_{p \in (1 \dots ⌊N⌋) \cap ℙ} \log p$
163	155 162	breqtrrd	$⊢ φ \to \sum_{p \in (⌊N^{A}⌋ + 1 \dots ⌊N⌋) \cap ℙ} \log p \leq θ (N)$
164	38 79 40 128 163	letrd	$⊢ φ \to (\underline{π} (N) - \underline{π} (N^{A})) A \log N \leq θ (N)$
165	31 38 40 68 164	ltletrd	$⊢ φ \to A \underline{π} (N) A \log N < θ (N)$
166	28 165	eqbrtrd	$⊢ φ \to A^{2} \underline{π} (N) \log N < θ (N)$

Metamath Proof Explorer

Theorem chtppilimlem1

Proof