chpub

Description: An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016)

		Ref	Expression
	Assertion	chpub	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) \leq θ (A) + \sqrt{A} \log A$

Proof

Step	Hyp	Ref	Expression
1		chpcl	$⊢ A \in ℝ \to ψ (A) \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) \in ℝ$
3		chtcl	$⊢ A \in ℝ \to θ (A) \in ℝ$
4	3	adantr	$⊢ (A \in ℝ \land 1 \leq A) \to θ (A) \in ℝ$
5	2 4	resubcld	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) - θ (A) \in ℝ$
6		simpl	$⊢ (A \in ℝ \land 1 \leq A) \to A \in ℝ$
7		0red	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \in ℝ$
8		1red	$⊢ (A \in ℝ \land 1 \leq A) \to 1 \in ℝ$
9		0lt1	$⊢ 0 < 1$
10	9	a1i	$⊢ (A \in ℝ \land 1 \leq A) \to 0 < 1$
11		simpr	$⊢ (A \in ℝ \land 1 \leq A) \to 1 \leq A$
12	7 8 6 10 11	ltletrd	$⊢ (A \in ℝ \land 1 \leq A) \to 0 < A$
13	6 12	elrpd	$⊢ (A \in ℝ \land 1 \leq A) \to A \in ℝ^{+}$
14	13	rpge0d	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \leq A$
15	6 14	resqrtcld	$⊢ (A \in ℝ \land 1 \leq A) \to \sqrt{A} \in ℝ$
16		ppifi	$⊢ \sqrt{A} \in ℝ \to [0, \sqrt{A}] \cap ℙ \in Fin$
17	15 16	syl	$⊢ (A \in ℝ \land 1 \leq A) \to [0, \sqrt{A}] \cap ℙ \in Fin$
18	13	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to A \in ℝ^{+}$
19	18	relogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log A \in ℝ$
20	17 19	fsumrecl	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A \in ℝ$
21	13	relogcld	$⊢ (A \in ℝ \land 1 \leq A) \to \log A \in ℝ$
22	15 21	remulcld	$⊢ (A \in ℝ \land 1 \leq A) \to \sqrt{A} \log A \in ℝ$
23		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
24	23	adantr	$⊢ (A \in ℝ \land 1 \leq A) \to [0, A] \cap ℙ \in Fin$
25		simpr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
26	25	elin2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
27		prmnn	$⊢ p \in ℙ \to p \in ℕ$
28	26 27	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
29	28	nnrpd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
30	29	relogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
31	21	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ$
32	28	nnred	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ℝ$
33		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
34	26 33	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in ℤ_{\geq 2}$
35		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
36	34 35	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to 1 < p$
37	32 36	rplogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ^{+}$
38	31 37	rerpdivcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ$
39		reflcl	$⊢ \frac{\log A}{\log p} \in ℝ \to ⌊\frac{\log A}{\log p}⌋ \in ℝ$
40	38 39	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℝ$
41	30 40	remulcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ \in ℝ$
42	41	recnd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ \in ℂ$
43	30	recnd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p \in ℂ$
44	24 42 43	fsumsub	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, A] \cap ℙ} (\log p ⌊\frac{\log A}{\log p}⌋ - \log p) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋ - \sum_{p \in [0, A] \cap ℙ} \log p$
45		0le0	$⊢ 0 \leq 0$
46	45	a1i	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \leq 0$
47	8 6 6 14 11	lemul2ad	$⊢ (A \in ℝ \land 1 \leq A) \to A \cdot 1 \leq A A$
48	6	recnd	$⊢ (A \in ℝ \land 1 \leq A) \to A \in ℂ$
49	48	sqsqrtd	$⊢ (A \in ℝ \land 1 \leq A) \to {\sqrt{A}}^{2} = A$
50	48	mulid1d	$⊢ (A \in ℝ \land 1 \leq A) \to A \cdot 1 = A$
51	49 50	eqtr4d	$⊢ (A \in ℝ \land 1 \leq A) \to {\sqrt{A}}^{2} = A \cdot 1$
52	48	sqvald	$⊢ (A \in ℝ \land 1 \leq A) \to A^{2} = A A$
53	47 51 52	3brtr4d	$⊢ (A \in ℝ \land 1 \leq A) \to {\sqrt{A}}^{2} \leq A^{2}$
54	6 14	sqrtge0d	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \leq \sqrt{A}$
55	15 6 54 14	le2sqd	$⊢ (A \in ℝ \land 1 \leq A) \to (\sqrt{A} \leq A \leftrightarrow {\sqrt{A}}^{2} \leq A^{2})$
56	53 55	mpbird	$⊢ (A \in ℝ \land 1 \leq A) \to \sqrt{A} \leq A$
57		iccss	$⊢ ((0 \in ℝ \land A \in ℝ) \land (0 \leq 0 \land \sqrt{A} \leq A)) \to [0, \sqrt{A}] \subseteq [0, A]$
58	7 6 46 56 57	syl22anc	$⊢ (A \in ℝ \land 1 \leq A) \to [0, \sqrt{A}] \subseteq [0, A]$
59	58	ssrind	$⊢ (A \in ℝ \land 1 \leq A) \to [0, \sqrt{A}] \cap ℙ \subseteq [0, A] \cap ℙ$
60	59	sselda	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
61	41 30	resubcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \in ℝ$
62	61	recnd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \in ℂ$
63	60 62	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \in ℂ$
64		eldifi	$⊢ p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
65	64 43	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p \in ℂ$
66	65	mulid2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 1 \log p = \log p$
67	25	elin1d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \in [0, A]$
68		0re	$⊢ 0 \in ℝ$
69	6	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to A \in ℝ$
70		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
71	68 69 70	sylancr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
72	67 71	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to (p \in ℝ \land 0 \leq p \land p \leq A)$
73	72	simp3d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, A] \cap ℙ)) \to p \leq A$
74	64 73	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p \leq A$
75	64 29	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p \in ℝ^{+}$
76	13	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to A \in ℝ^{+}$
77	75 76	logled	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (p \leq A \leftrightarrow \log p \leq \log A)$
78	74 77	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p \leq \log A$
79	66 78	eqbrtrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 1 \log p \leq \log A$
80		1red	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 1 \in ℝ$
81	21	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log A \in ℝ$
82	64 37	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p \in ℝ^{+}$
83	80 81 82	lemuldivd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (1 \log p \leq \log A \leftrightarrow 1 \leq \frac{\log A}{\log p})$
84	79 83	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 1 \leq \frac{\log A}{\log p}$
85	6	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to A \in ℝ$
86	85	recnd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to A \in ℂ$
87	86	sqsqrtd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to {\sqrt{A}}^{2} = A$
88		eldifn	$⊢ p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ)) \to \neg p \in ([0, \sqrt{A}] \cap ℙ)$
89	88	adantl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \neg p \in ([0, \sqrt{A}] \cap ℙ)$
90	64 26	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p \in ℙ$
91		elin	$⊢ p \in ([0, \sqrt{A}] \cap ℙ) \leftrightarrow (p \in [0, \sqrt{A}] \land p \in ℙ)$
92	91	rbaib	$⊢ p \in ℙ \to (p \in ([0, \sqrt{A}] \cap ℙ) \leftrightarrow p \in [0, \sqrt{A}])$
93	90 92	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (p \in ([0, \sqrt{A}] \cap ℙ) \leftrightarrow p \in [0, \sqrt{A}])$
94		0red	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 0 \in ℝ$
95	15	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \sqrt{A} \in ℝ$
96	64 28	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p \in ℕ$
97	96	nnred	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p \in ℝ$
98	75	rpge0d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 0 \leq p$
99		elicc2	$⊢ (0 \in ℝ \land \sqrt{A} \in ℝ) \to (p \in [0, \sqrt{A}] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq \sqrt{A}))$
100		df-3an	$⊢ (p \in ℝ \land 0 \leq p \land p \leq \sqrt{A}) \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq \sqrt{A})$
101	99 100	bitrdi	$⊢ (0 \in ℝ \land \sqrt{A} \in ℝ) \to (p \in [0, \sqrt{A}] \leftrightarrow ((p \in ℝ \land 0 \leq p) \land p \leq \sqrt{A}))$
102	101	baibd	$⊢ ((0 \in ℝ \land \sqrt{A} \in ℝ) \land (p \in ℝ \land 0 \leq p)) \to (p \in [0, \sqrt{A}] \leftrightarrow p \leq \sqrt{A})$
103	94 95 97 98 102	syl22anc	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (p \in [0, \sqrt{A}] \leftrightarrow p \leq \sqrt{A})$
104	93 103	bitrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (p \in ([0, \sqrt{A}] \cap ℙ) \leftrightarrow p \leq \sqrt{A})$
105	89 104	mtbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \neg p \leq \sqrt{A}$
106	95 97	ltnled	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (\sqrt{A} < p \leftrightarrow \neg p \leq \sqrt{A})$
107	105 106	mpbird	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \sqrt{A} < p$
108	54	adantr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 0 \leq \sqrt{A}$
109	95 97 108 98	lt2sqd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (\sqrt{A} < p \leftrightarrow {\sqrt{A}}^{2} < p^{2})$
110	107 109	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to {\sqrt{A}}^{2} < p^{2}$
111	87 110	eqbrtrrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to A < p^{2}$
112	96	nnsqcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p^{2} \in ℕ$
113	112	nnrpd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to p^{2} \in ℝ^{+}$
114		logltb	$⊢ (A \in ℝ^{+} \land p^{2} \in ℝ^{+}) \to (A < p^{2} \leftrightarrow \log A < \log p^{2})$
115	76 113 114	syl2anc	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (A < p^{2} \leftrightarrow \log A < \log p^{2})$
116	111 115	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log A < \log p^{2}$
117		2z	$⊢ 2 \in ℤ$
118		relogexp	$⊢ (p \in ℝ^{+} \land 2 \in ℤ) \to \log p^{2} = 2 \log p$
119	75 117 118	sylancl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p^{2} = 2 \log p$
120	116 119	breqtrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log A < 2 \log p$
121		2re	$⊢ 2 \in ℝ$
122	121	a1i	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to 2 \in ℝ$
123	81 122 82	ltdivmul2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (\frac{\log A}{\log p} < 2 \leftrightarrow \log A < 2 \log p)$
124	120 123	mpbird	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \frac{\log A}{\log p} < 2$
125		df-2	$⊢ 2 = 1 + 1$
126	124 125	breqtrdi	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \frac{\log A}{\log p} < 1 + 1$
127	64 38	sylan2	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \frac{\log A}{\log p} \in ℝ$
128		1z	$⊢ 1 \in ℤ$
129		flbi	$⊢ (\frac{\log A}{\log p} \in ℝ \land 1 \in ℤ) \to (⌊\frac{\log A}{\log p}⌋ = 1 \leftrightarrow (1 \leq \frac{\log A}{\log p} \land \frac{\log A}{\log p} < 1 + 1))$
130	127 128 129	sylancl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to (⌊\frac{\log A}{\log p}⌋ = 1 \leftrightarrow (1 \leq \frac{\log A}{\log p} \land \frac{\log A}{\log p} < 1 + 1))$
131	84 126 130	mpbir2and	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to ⌊\frac{\log A}{\log p}⌋ = 1$
132	131	oveq2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p ⌊\frac{\log A}{\log p}⌋ = \log p \cdot 1$
133	65	mulid1d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p \cdot 1 = \log p$
134	132 133	eqtrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p ⌊\frac{\log A}{\log p}⌋ = \log p$
135	134	oveq1d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p = \log p - \log p$
136	65	subidd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p - \log p = 0$
137	135 136	eqtrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in (([0, A] \cap ℙ) ∖ ([0, \sqrt{A}] \cap ℙ))) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p = 0$
138	59 63 137 24	fsumss	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} (\log p ⌊\frac{\log A}{\log p}⌋ - \log p) = \sum_{p \in [0, A] \cap ℙ} (\log p ⌊\frac{\log A}{\log p}⌋ - \log p)$
139		chpval2	$⊢ A \in ℝ \to ψ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$
140	139	adantr	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋$
141		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
142	141	adantr	$⊢ (A \in ℝ \land 1 \leq A) \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
143	140 142	oveq12d	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) - θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p ⌊\frac{\log A}{\log p}⌋ - \sum_{p \in [0, A] \cap ℙ} \log p$
144	44 138 143	3eqtr4rd	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) - θ (A) = \sum_{p \in [0, \sqrt{A}] \cap ℙ} (\log p ⌊\frac{\log A}{\log p}⌋ - \log p)$
145	60 61	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \in ℝ$
146	60 41	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ \in ℝ$
147	60 37	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p \in ℝ^{+}$
148	147	rpge0d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to 0 \leq \log p$
149		simpr	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to p \in ([0, \sqrt{A}] \cap ℙ)$
150	149	elin2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to p \in ℙ$
151	150 27	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to p \in ℕ$
152	151	nnrpd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to p \in ℝ^{+}$
153	152	relogcld	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p \in ℝ$
154	146 153	subge02d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to (0 \leq \log p \leftrightarrow \log p ⌊\frac{\log A}{\log p}⌋ - \log p \leq \log p ⌊\frac{\log A}{\log p}⌋)$
155	148 154	mpbid	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \leq \log p ⌊\frac{\log A}{\log p}⌋$
156	60 38	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ$
157		flle	$⊢ \frac{\log A}{\log p} \in ℝ \to ⌊\frac{\log A}{\log p}⌋ \leq \frac{\log A}{\log p}$
158	156 157	syl	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \leq \frac{\log A}{\log p}$
159	60 40	syldan	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℝ$
160	159 19 147	lemuldiv2d	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to (\log p ⌊\frac{\log A}{\log p}⌋ \leq \log A \leftrightarrow ⌊\frac{\log A}{\log p}⌋ \leq \frac{\log A}{\log p})$
161	158 160	mpbird	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ \leq \log A$
162	145 146 19 155 161	letrd	$⊢ ((A \in ℝ \land 1 \leq A) \land p \in ([0, \sqrt{A}] \cap ℙ)) \to \log p ⌊\frac{\log A}{\log p}⌋ - \log p \leq \log A$
163	17 145 19 162	fsumle	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} (\log p ⌊\frac{\log A}{\log p}⌋ - \log p) \leq \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A$
164	144 163	eqbrtrd	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) - θ (A) \leq \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A$
165	21	recnd	$⊢ (A \in ℝ \land 1 \leq A) \to \log A \in ℂ$
166		fsumconst	$⊢ ([0, \sqrt{A}] \cap ℙ \in Fin \land \log A \in ℂ) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A = \|[0, \sqrt{A}] \cap ℙ\| \log A$
167	17 165 166	syl2anc	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A = \|[0, \sqrt{A}] \cap ℙ\| \log A$
168		hashcl	$⊢ [0, \sqrt{A}] \cap ℙ \in Fin \to \|[0, \sqrt{A}] \cap ℙ\| \in ℕ_{0}$
169	17 168	syl	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \in ℕ_{0}$
170	169	nn0red	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \in ℝ$
171		logge0	$⊢ (A \in ℝ \land 1 \leq A) \to 0 \leq \log A$
172		reflcl	$⊢ \sqrt{A} \in ℝ \to ⌊\sqrt{A}⌋ \in ℝ$
173	15 172	syl	$⊢ (A \in ℝ \land 1 \leq A) \to ⌊\sqrt{A}⌋ \in ℝ$
174		fzfid	$⊢ (A \in ℝ \land 1 \leq A) \to (1 \dots ⌊\sqrt{A}⌋) \in Fin$
175		ppisval	$⊢ \sqrt{A} \in ℝ \to [0, \sqrt{A}] \cap ℙ = (2 \dots ⌊\sqrt{A}⌋) \cap ℙ$
176	15 175	syl	$⊢ (A \in ℝ \land 1 \leq A) \to [0, \sqrt{A}] \cap ℙ = (2 \dots ⌊\sqrt{A}⌋) \cap ℙ$
177		inss1	$⊢ (2 \dots ⌊\sqrt{A}⌋) \cap ℙ \subseteq (2 \dots ⌊\sqrt{A}⌋)$
178		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
179		fzss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 \dots ⌊\sqrt{A}⌋) \subseteq (1 \dots ⌊\sqrt{A}⌋)$
180	178 179	mp1i	$⊢ (A \in ℝ \land 1 \leq A) \to (2 \dots ⌊\sqrt{A}⌋) \subseteq (1 \dots ⌊\sqrt{A}⌋)$
181	177 180	sstrid	$⊢ (A \in ℝ \land 1 \leq A) \to (2 \dots ⌊\sqrt{A}⌋) \cap ℙ \subseteq (1 \dots ⌊\sqrt{A}⌋)$
182	176 181	eqsstrd	$⊢ (A \in ℝ \land 1 \leq A) \to [0, \sqrt{A}] \cap ℙ \subseteq (1 \dots ⌊\sqrt{A}⌋)$
183		ssdomg	$⊢ (1 \dots ⌊\sqrt{A}⌋) \in Fin \to ([0, \sqrt{A}] \cap ℙ \subseteq (1 \dots ⌊\sqrt{A}⌋) \to ([0, \sqrt{A}] \cap ℙ) ≼ (1 \dots ⌊\sqrt{A}⌋))$
184	174 182 183	sylc	$⊢ (A \in ℝ \land 1 \leq A) \to ([0, \sqrt{A}] \cap ℙ) ≼ (1 \dots ⌊\sqrt{A}⌋)$
185		hashdom	$⊢ ([0, \sqrt{A}] \cap ℙ \in Fin \land (1 \dots ⌊\sqrt{A}⌋) \in Fin) \to (\|[0, \sqrt{A}] \cap ℙ\| \leq \|(1 \dots ⌊\sqrt{A}⌋)\| \leftrightarrow ([0, \sqrt{A}] \cap ℙ) ≼ (1 \dots ⌊\sqrt{A}⌋))$
186	17 174 185	syl2anc	$⊢ (A \in ℝ \land 1 \leq A) \to (\|[0, \sqrt{A}] \cap ℙ\| \leq \|(1 \dots ⌊\sqrt{A}⌋)\| \leftrightarrow ([0, \sqrt{A}] \cap ℙ) ≼ (1 \dots ⌊\sqrt{A}⌋))$
187	184 186	mpbird	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \leq \|(1 \dots ⌊\sqrt{A}⌋)\|$
188		flge0nn0	$⊢ (\sqrt{A} \in ℝ \land 0 \leq \sqrt{A}) \to ⌊\sqrt{A}⌋ \in ℕ_{0}$
189	15 54 188	syl2anc	$⊢ (A \in ℝ \land 1 \leq A) \to ⌊\sqrt{A}⌋ \in ℕ_{0}$
190		hashfz1	$⊢ ⌊\sqrt{A}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\sqrt{A}⌋)\| = ⌊\sqrt{A}⌋$
191	189 190	syl	$⊢ (A \in ℝ \land 1 \leq A) \to \|(1 \dots ⌊\sqrt{A}⌋)\| = ⌊\sqrt{A}⌋$
192	187 191	breqtrd	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \leq ⌊\sqrt{A}⌋$
193		flle	$⊢ \sqrt{A} \in ℝ \to ⌊\sqrt{A}⌋ \leq \sqrt{A}$
194	15 193	syl	$⊢ (A \in ℝ \land 1 \leq A) \to ⌊\sqrt{A}⌋ \leq \sqrt{A}$
195	170 173 15 192 194	letrd	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \leq \sqrt{A}$
196	170 15 21 171 195	lemul1ad	$⊢ (A \in ℝ \land 1 \leq A) \to \|[0, \sqrt{A}] \cap ℙ\| \log A \leq \sqrt{A} \log A$
197	167 196	eqbrtrd	$⊢ (A \in ℝ \land 1 \leq A) \to \sum_{p \in [0, \sqrt{A}] \cap ℙ} \log A \leq \sqrt{A} \log A$
198	5 20 22 164 197	letrd	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) - θ (A) \leq \sqrt{A} \log A$
199	2 4 22	lesubadd2d	$⊢ (A \in ℝ \land 1 \leq A) \to (ψ (A) - θ (A) \leq \sqrt{A} \log A \leftrightarrow ψ (A) \leq θ (A) + \sqrt{A} \log A)$
200	198 199	mpbid	$⊢ (A \in ℝ \land 1 \leq A) \to ψ (A) \leq θ (A) + \sqrt{A} \log A$

Metamath Proof Explorer

Theorem chpub

Proof