rplogsumlem2

Description: Lemma for rplogsum . Equation 9.2.14 of Shapiro, p. 331. (Contributed by Mario Carneiro, 2-May-2016)

		Ref	Expression
	Assertion	rplogsumlem2	$⊢ A \in ℤ \to \sum_{n = 1}^{A} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n}) \leq 2$

Proof

Step	Hyp	Ref	Expression
1		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
2	1	oveq2d	$⊢ A \in ℤ \to (1 \dots ⌊A⌋) = (1 \dots A)$
3	2	sumeq1d	$⊢ A \in ℤ \to \sum_{n = 1}^{⌊A⌋} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n}) = \sum_{n = 1}^{A} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n})$
4		fveq2	$⊢ n = p^{k} \to Λ (n) = Λ (p^{k})$
5		eleq1	$⊢ n = p^{k} \to (n \in ℙ \leftrightarrow p^{k} \in ℙ)$
6		fveq2	$⊢ n = p^{k} \to \log n = \log p^{k}$
7	5 6	ifbieq1d	$⊢ n = p^{k} \to if (n \in ℙ, \log n, 0) = if (p^{k} \in ℙ, \log p^{k}, 0)$
8	4 7	oveq12d	$⊢ n = p^{k} \to Λ (n) - if (n \in ℙ, \log n, 0) = Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)$
9		id	$⊢ n = p^{k} \to n = p^{k}$
10	8 9	oveq12d	$⊢ n = p^{k} \to \frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n} = \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}$
11		zre	$⊢ A \in ℤ \to A \in ℝ$
12		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
13	12	adantl	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
14		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
15	13 14	syl	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℝ$
16	13	nnrpd	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to n \in ℝ^{+}$
17	16	relogcld	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to \log n \in ℝ$
18		0re	$⊢ 0 \in ℝ$
19		ifcl	$⊢ (\log n \in ℝ \land 0 \in ℝ) \to if (n \in ℙ, \log n, 0) \in ℝ$
20	17 18 19	sylancl	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to if (n \in ℙ, \log n, 0) \in ℝ$
21	15 20	resubcld	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) - if (n \in ℙ, \log n, 0) \in ℝ$
22	21 13	nndivred	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to \frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n} \in ℝ$
23	22	recnd	$⊢ (A \in ℤ \land n \in (1 \dots ⌊A⌋)) \to \frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n} \in ℂ$
24		simprr	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to Λ (n) = 0$
25		vmaprm	$⊢ n \in ℙ \to Λ (n) = \log n$
26		prmnn	$⊢ n \in ℙ \to n \in ℕ$
27	26	nnred	$⊢ n \in ℙ \to n \in ℝ$
28		prmgt1	$⊢ n \in ℙ \to 1 < n$
29	27 28	rplogcld	$⊢ n \in ℙ \to \log n \in ℝ^{+}$
30	25 29	eqeltrd	$⊢ n \in ℙ \to Λ (n) \in ℝ^{+}$
31	30	rpne0d	$⊢ n \in ℙ \to Λ (n) \neq 0$
32	31	necon2bi	$⊢ Λ (n) = 0 \to \neg n \in ℙ$
33	32	ad2antll	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to \neg n \in ℙ$
34	33	iffalsed	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to if (n \in ℙ, \log n, 0) = 0$
35	24 34	oveq12d	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to Λ (n) - if (n \in ℙ, \log n, 0) = 0 - 0$
36		0m0e0	$⊢ 0 - 0 = 0$
37	35 36	eqtrdi	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to Λ (n) - if (n \in ℙ, \log n, 0) = 0$
38	37	oveq1d	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to \frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n} = \frac{0}{n}$
39	12	ad2antrl	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to n \in ℕ$
40	39	nnrpd	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to n \in ℝ^{+}$
41	40	rpcnne0d	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to (n \in ℂ \land n \neq 0)$
42		div0	$⊢ (n \in ℂ \land n \neq 0) \to \frac{0}{n} = 0$
43	41 42	syl	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to \frac{0}{n} = 0$
44	38 43	eqtrd	$⊢ (A \in ℤ \land (n \in (1 \dots ⌊A⌋) \land Λ (n) = 0)) \to \frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n} = 0$
45	10 11 23 44	fsumvma2	$⊢ A \in ℤ \to \sum_{n = 1}^{⌊A⌋} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n}) = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}})$
46	3 45	eqtr3d	$⊢ A \in ℤ \to \sum_{n = 1}^{A} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n}) = \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}})$
47		fzfid	$⊢ A \in ℤ \to (2 \dots \|A\| + 1) \in Fin$
48		simpr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
49	48	elin2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
50		prmnn	$⊢ p \in ℙ \to p \in ℕ$
51	49 50	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
52	51	nnred	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ$
53	11	adantr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to A \in ℝ$
54		zcn	$⊢ A \in ℤ \to A \in ℂ$
55	54	abscld	$⊢ A \in ℤ \to \|A\| \in ℝ$
56		peano2re	$⊢ \|A\| \in ℝ \to \|A\| + 1 \in ℝ$
57	55 56	syl	$⊢ A \in ℤ \to \|A\| + 1 \in ℝ$
58	57	adantr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \|A\| + 1 \in ℝ$
59		elinel1	$⊢ p \in ([0, A] \cap ℙ) \to p \in [0, A]$
60		elicc2	$⊢ (0 \in ℝ \land A \in ℝ) \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
61	18 11 60	sylancr	$⊢ A \in ℤ \to (p \in [0, A] \leftrightarrow (p \in ℝ \land 0 \leq p \land p \leq A))$
62	59 61	imbitrid	$⊢ A \in ℤ \to (p \in ([0, A] \cap ℙ) \to (p \in ℝ \land 0 \leq p \land p \leq A))$
63	62	imp	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (p \in ℝ \land 0 \leq p \land p \leq A)$
64	63	simp3d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \leq A$
65	54	adantr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to A \in ℂ$
66	65	abscld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \|A\| \in ℝ$
67	53	leabsd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to A \leq \|A\|$
68	66	lep1d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \|A\| \leq \|A\| + 1$
69	53 66 58 67 68	letrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to A \leq \|A\| + 1$
70	52 53 58 64 69	letrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \leq \|A\| + 1$
71		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
72	49 71	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℤ_{\geq 2}$
73		nn0abscl	$⊢ A \in ℤ \to \|A\| \in ℕ_{0}$
74		nn0p1nn	$⊢ \|A\| \in ℕ_{0} \to \|A\| + 1 \in ℕ$
75	73 74	syl	$⊢ A \in ℤ \to \|A\| + 1 \in ℕ$
76	75	nnzd	$⊢ A \in ℤ \to \|A\| + 1 \in ℤ$
77	76	adantr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \|A\| + 1 \in ℤ$
78		elfz5	$⊢ (p \in ℤ_{\geq 2} \land \|A\| + 1 \in ℤ) \to (p \in (2 \dots \|A\| + 1) \leftrightarrow p \leq \|A\| + 1)$
79	72 77 78	syl2anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (p \in (2 \dots \|A\| + 1) \leftrightarrow p \leq \|A\| + 1)$
80	70 79	mpbird	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in (2 \dots \|A\| + 1)$
81	80	ex	$⊢ A \in ℤ \to (p \in ([0, A] \cap ℙ) \to p \in (2 \dots \|A\| + 1))$
82	81	ssrdv	$⊢ A \in ℤ \to [0, A] \cap ℙ \subseteq (2 \dots \|A\| + 1)$
83	47 82	ssfid	$⊢ A \in ℤ \to [0, A] \cap ℙ \in Fin$
84		fzfid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (1 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin$
85		simprl	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p \in ([0, A] \cap ℙ)$
86	85	elin2d	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p \in ℙ$
87		elfznn	$⊢ k \in (1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
88	87	ad2antll	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to k \in ℕ$
89		vmappw	$⊢ (p \in ℙ \land k \in ℕ) \to Λ (p^{k}) = \log p$
90	86 88 89	syl2anc	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to Λ (p^{k}) = \log p$
91	51	adantrr	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p \in ℕ$
92	91	nnrpd	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p \in ℝ^{+}$
93	92	relogcld	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to \log p \in ℝ$
94	90 93	eqeltrd	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to Λ (p^{k}) \in ℝ$
95	88	nnnn0d	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to k \in ℕ_{0}$
96		nnexpcl	$⊢ (p \in ℕ \land k \in ℕ_{0}) \to p^{k} \in ℕ$
97	91 95 96	syl2anc	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p^{k} \in ℕ$
98	97	nnrpd	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to p^{k} \in ℝ^{+}$
99	98	relogcld	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to \log p^{k} \in ℝ$
100		ifcl	$⊢ (\log p^{k} \in ℝ \land 0 \in ℝ) \to if (p^{k} \in ℙ, \log p^{k}, 0) \in ℝ$
101	99 18 100	sylancl	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to if (p^{k} \in ℙ, \log p^{k}, 0) \in ℝ$
102	94 101	resubcld	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0) \in ℝ$
103	102 97	nndivred	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} \in ℝ$
104	103	anassrs	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} \in ℝ$
105	84 104	fsumrecl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) \in ℝ$
106	83 105	fsumrecl	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) \in ℝ$
107	51	nnrpd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
108	107	relogcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
109		uz2m1nn	$⊢ p \in ℤ_{\geq 2} \to p - 1 \in ℕ$
110	72 109	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p - 1 \in ℕ$
111	51 110	nnmulcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p (p - 1) \in ℕ$
112	108 111	nndivred	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\log p}{p (p - 1)} \in ℝ$
113	83 112	fsumrecl	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} (\frac{\log p}{p (p - 1)}) \in ℝ$
114		2re	$⊢ 2 \in ℝ$
115	114	a1i	$⊢ A \in ℤ \to 2 \in ℝ$
116	18	a1i	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 \in ℝ$
117	51	nngt0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 < p$
118	116 52 53 117 64	ltletrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 < A$
119	53 118	elrpd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to A \in ℝ^{+}$
120	119	relogcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log A \in ℝ$
121		prmgt1	$⊢ p \in ℙ \to 1 < p$
122	49 121	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 < p$
123	52 122	rplogcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ^{+}$
124	120 123	rerpdivcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\log A}{\log p} \in ℝ$
125	123	rpcnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℂ$
126	125	mullidd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 \log p = \log p$
127	107 119	logled	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (p \leq A \leftrightarrow \log p \leq \log A)$
128	64 127	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \leq \log A$
129	126 128	eqbrtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 \log p \leq \log A$
130		1re	$⊢ 1 \in ℝ$
131	130	a1i	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 \in ℝ$
132	131 120 123	lemuldivd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (1 \log p \leq \log A \leftrightarrow 1 \leq \frac{\log A}{\log p})$
133	129 132	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 \leq \frac{\log A}{\log p}$
134		flge1nn	$⊢ (\frac{\log A}{\log p} \in ℝ \land 1 \leq \frac{\log A}{\log p}) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ$
135	124 133 134	syl2anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℕ$
136		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
137	135 136	eleqtrdi	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℤ_{\geq 1}$
138	103	recnd	$⊢ (A \in ℤ \land (p \in ([0, A] \cap ℙ) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋))) \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} \in ℂ$
139	138	anassrs	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 \dots ⌊\frac{\log A}{\log p}⌋)) \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} \in ℂ$
140		oveq2	$⊢ k = 1 \to p^{k} = p^{1}$
141	140	fveq2d	$⊢ k = 1 \to Λ (p^{k}) = Λ (p^{1})$
142	140	eleq1d	$⊢ k = 1 \to (p^{k} \in ℙ \leftrightarrow p^{1} \in ℙ)$
143	140	fveq2d	$⊢ k = 1 \to \log p^{k} = \log p^{1}$
144	142 143	ifbieq1d	$⊢ k = 1 \to if (p^{k} \in ℙ, \log p^{k}, 0) = if (p^{1} \in ℙ, \log p^{1}, 0)$
145	141 144	oveq12d	$⊢ k = 1 \to Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0) = Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)$
146	145 140	oveq12d	$⊢ k = 1 \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} = \frac{Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)}{p^{1}}$
147	137 139 146	fsum1p	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) = (\frac{Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)}{p^{1}}) + \sum_{k = 1 + 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}})$
148	51	nncnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \in ℂ$
149	148	exp1d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p^{1} = p$
150	149	fveq2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to Λ (p^{1}) = Λ (p)$
151		vmaprm	$⊢ p \in ℙ \to Λ (p) = \log p$
152	49 151	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to Λ (p) = \log p$
153	150 152	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to Λ (p^{1}) = \log p$
154	149 49	eqeltrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p^{1} \in ℙ$
155	154	iftrued	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to if (p^{1} \in ℙ, \log p^{1}, 0) = \log p^{1}$
156	149	fveq2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p^{1} = \log p$
157	155 156	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to if (p^{1} \in ℙ, \log p^{1}, 0) = \log p$
158	153 157	oveq12d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0) = \log p - \log p$
159	125	subidd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p - \log p = 0$
160	158 159	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0) = 0$
161	160 149	oveq12d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)}{p^{1}} = \frac{0}{p}$
162	107	rpcnne0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (p \in ℂ \land p \neq 0)$
163		div0	$⊢ (p \in ℂ \land p \neq 0) \to \frac{0}{p} = 0$
164	162 163	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{0}{p} = 0$
165	161 164	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)}{p^{1}} = 0$
166		1p1e2	$⊢ 1 + 1 = 2$
167	166	oveq1i	$⊢ (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋) = (2 \dots ⌊\frac{\log A}{\log p}⌋)$
168	167	a1i	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋) = (2 \dots ⌊\frac{\log A}{\log p}⌋)$
169		elfzuz	$⊢ k \in (2 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℤ_{\geq 2}$
170		eluz2nn	$⊢ k \in ℤ_{\geq 2} \to k \in ℕ$
171	169 170	syl	$⊢ k \in (2 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
172	171 167	eleq2s	$⊢ k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ$
173	49 172 89	syl2an	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to Λ (p^{k}) = \log p$
174	51	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to p \in ℕ$
175		nnq	$⊢ p \in ℕ \to p \in ℚ$
176	174 175	syl	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to p \in ℚ$
177	169 167	eleq2s	$⊢ k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℤ_{\geq 2}$
178	177	adantl	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to k \in ℤ_{\geq 2}$
179		expnprm	$⊢ (p \in ℚ \land k \in ℤ_{\geq 2}) \to \neg p^{k} \in ℙ$
180	176 178 179	syl2anc	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to \neg p^{k} \in ℙ$
181	180	iffalsed	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to if (p^{k} \in ℙ, \log p^{k}, 0) = 0$
182	173 181	oveq12d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0) = \log p - 0$
183	125	subid1d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p - 0 = \log p$
184	183	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to \log p - 0 = \log p$
185	182 184	eqtrd	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0) = \log p$
186	185	oveq1d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (1 + 1 \dots ⌊\frac{\log A}{\log p}⌋)) \to \frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}} = \frac{\log p}{p^{k}}$
187	168 186	sumeq12dv	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1 + 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) = \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}})$
188	165 187	oveq12d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{Λ (p^{1}) - if (p^{1} \in ℙ, \log p^{1}, 0)}{p^{1}}) + \sum_{k = 1 + 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) = 0 + \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}})$
189		fzfid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (2 \dots ⌊\frac{\log A}{\log p}⌋) \in Fin$
190	108	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \log p \in ℝ$
191		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
192	51 191 96	syl2an	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p^{k} \in ℕ$
193	190 192	nndivred	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \frac{\log p}{p^{k}} \in ℝ$
194	171 193	sylan2	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (2 \dots ⌊\frac{\log A}{\log p}⌋)) \to \frac{\log p}{p^{k}} \in ℝ$
195	189 194	fsumrecl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) \in ℝ$
196	195	recnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) \in ℂ$
197	196	addlidd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 + \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) = \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}})$
198	147 188 197	3eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) = \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}})$
199	107	rpreccld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p} \in ℝ^{+}$
200	124	flcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ \in ℤ$
201	200	peano2zd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℤ$
202	199 201	rpexpcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \in ℝ^{+}$
203	202	rpge0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 \leq {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}$
204	51	nnrecred	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p} \in ℝ$
205	204	resqcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{2} \in ℝ$
206	135	peano2nnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℕ$
207	206	nnnn0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℕ_{0}$
208	204 207	reexpcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \in ℝ$
209	205 208	subge02d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (0 \leq {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leftrightarrow {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leq {(\frac{1}{p})}^{2})$
210	203 209	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leq {(\frac{1}{p})}^{2}$
211	110	nnrpd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p - 1 \in ℝ^{+}$
212	211	rpcnne0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (p - 1 \in ℂ \land p - 1 \neq 0)$
213	199	rpcnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p} \in ℂ$
214		dmdcan	$⊢ ((p - 1 \in ℂ \land p - 1 \neq 0) \land (p \in ℂ \land p \neq 0) \land \frac{1}{p} \in ℂ) \to (\frac{p - 1}{p}) (\frac{\frac{1}{p}}{p - 1}) = \frac{\frac{1}{p}}{p}$
215	212 162 213 214	syl3anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{p - 1}{p}) (\frac{\frac{1}{p}}{p - 1}) = \frac{\frac{1}{p}}{p}$
216	131	recnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 \in ℂ$
217		divsubdir	$⊢ (p \in ℂ \land 1 \in ℂ \land (p \in ℂ \land p \neq 0)) \to \frac{p - 1}{p} = (\frac{p}{p}) - (\frac{1}{p})$
218	148 216 162 217	syl3anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{p - 1}{p} = (\frac{p}{p}) - (\frac{1}{p})$
219		divid	$⊢ (p \in ℂ \land p \neq 0) \to \frac{p}{p} = 1$
220	162 219	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{p}{p} = 1$
221	220	oveq1d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{p}{p}) - (\frac{1}{p}) = 1 - (\frac{1}{p})$
222	218 221	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{p - 1}{p} = 1 - (\frac{1}{p})$
223		divdiv1	$⊢ (1 \in ℂ \land (p \in ℂ \land p \neq 0) \land (p - 1 \in ℂ \land p - 1 \neq 0)) \to \frac{\frac{1}{p}}{p - 1} = \frac{1}{p (p - 1)}$
224	216 162 212 223	syl3anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\frac{1}{p}}{p - 1} = \frac{1}{p (p - 1)}$
225	222 224	oveq12d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{p - 1}{p}) (\frac{\frac{1}{p}}{p - 1}) = (1 - (\frac{1}{p})) (\frac{1}{p (p - 1)})$
226	51	nnne0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p \neq 0$
227	213 148 226	divrecd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\frac{1}{p}}{p} = (\frac{1}{p}) (\frac{1}{p})$
228	213	sqvald	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{2} = (\frac{1}{p}) (\frac{1}{p})$
229	227 228	eqtr4d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\frac{1}{p}}{p} = {(\frac{1}{p})}^{2}$
230	215 225 229	3eqtr3d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (1 - (\frac{1}{p})) (\frac{1}{p (p - 1)}) = {(\frac{1}{p})}^{2}$
231	210 230	breqtrrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leq (1 - (\frac{1}{p})) (\frac{1}{p (p - 1)})$
232	205 208	resubcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \in ℝ$
233	111	nnrecred	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p (p - 1)} \in ℝ$
234		resubcl	$⊢ (1 \in ℝ \land \frac{1}{p} \in ℝ) \to 1 - (\frac{1}{p}) \in ℝ$
235	130 204 234	sylancr	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 - (\frac{1}{p}) \in ℝ$
236		recgt1	$⊢ (p \in ℝ \land 0 < p) \to (1 < p \leftrightarrow \frac{1}{p} < 1)$
237	52 117 236	syl2anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (1 < p \leftrightarrow \frac{1}{p} < 1)$
238	122 237	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p} < 1$
239		posdif	$⊢ (\frac{1}{p} \in ℝ \land 1 \in ℝ) \to (\frac{1}{p} < 1 \leftrightarrow 0 < 1 - (\frac{1}{p}))$
240	204 130 239	sylancl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{1}{p} < 1 \leftrightarrow 0 < 1 - (\frac{1}{p}))$
241	238 240	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 0 < 1 - (\frac{1}{p})$
242		ledivmul	$⊢ ({(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \in ℝ \land \frac{1}{p (p - 1)} \in ℝ \land (1 - (\frac{1}{p}) \in ℝ \land 0 < 1 - (\frac{1}{p}))) \to (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} \leq \frac{1}{p (p - 1)} \leftrightarrow {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leq (1 - (\frac{1}{p})) (\frac{1}{p (p - 1)}))$
243	232 233 235 241 242	syl112anc	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} \leq \frac{1}{p (p - 1)} \leftrightarrow {(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1} \leq (1 - (\frac{1}{p})) (\frac{1}{p (p - 1)}))$
244	231 243	mpbird	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} \leq \frac{1}{p (p - 1)}$
245	235 241	elrpd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 1 - (\frac{1}{p}) \in ℝ^{+}$
246	232 245	rerpdivcld	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} \in ℝ$
247	246 233 123	lemul2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} \leq \frac{1}{p (p - 1)} \leftrightarrow \log p (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})}) \leq \log p (\frac{1}{p (p - 1)}))$
248	244 247	mpbid	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})}) \leq \log p (\frac{1}{p (p - 1)})$
249	125	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \log p \in ℂ$
250	192	nncnd	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p^{k} \in ℂ$
251	192	nnne0d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p^{k} \neq 0$
252	249 250 251	divrecd	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \frac{\log p}{p^{k}} = \log p (\frac{1}{p^{k}})$
253	148	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p \in ℂ$
254	51	adantr	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p \in ℕ$
255	254	nnne0d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to p \neq 0$
256		nnz	$⊢ k \in ℕ \to k \in ℤ$
257	256	adantl	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to k \in ℤ$
258	253 255 257	exprecd	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to {(\frac{1}{p})}^{k} = \frac{1}{p^{k}}$
259	258	oveq2d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \log p {(\frac{1}{p})}^{k} = \log p (\frac{1}{p^{k}})$
260	252 259	eqtr4d	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in ℕ) \to \frac{\log p}{p^{k}} = \log p {(\frac{1}{p})}^{k}$
261	171 260	sylan2	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (2 \dots ⌊\frac{\log A}{\log p}⌋)) \to \frac{\log p}{p^{k}} = \log p {(\frac{1}{p})}^{k}$
262	261	sumeq2dv	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) = \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} \log p {(\frac{1}{p})}^{k}$
263	171	nnnn0d	$⊢ k \in (2 \dots ⌊\frac{\log A}{\log p}⌋) \to k \in ℕ_{0}$
264		expcl	$⊢ (\frac{1}{p} \in ℂ \land k \in ℕ_{0}) \to {(\frac{1}{p})}^{k} \in ℂ$
265	213 263 264	syl2an	$⊢ ((A \in ℤ \land p \in ([0, A] \cap ℙ)) \land k \in (2 \dots ⌊\frac{\log A}{\log p}⌋)) \to {(\frac{1}{p})}^{k} \in ℂ$
266	189 125 265	fsummulc2	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} {(\frac{1}{p})}^{k} = \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} \log p {(\frac{1}{p})}^{k}$
267		fzval3	$⊢ ⌊\frac{\log A}{\log p}⌋ \in ℤ \to (2 \dots ⌊\frac{\log A}{\log p}⌋) = (2 ..^⌊\frac{\log A}{\log p}⌋ + 1)$
268	200 267	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to (2 \dots ⌊\frac{\log A}{\log p}⌋) = (2 ..^⌊\frac{\log A}{\log p}⌋ + 1)$
269	268	sumeq1d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} {(\frac{1}{p})}^{k} = \sum_{k \in (2 ..^⌊\frac{\log A}{\log p}⌋ + 1)} {(\frac{1}{p})}^{k}$
270	204 238	ltned	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{1}{p} \neq 1$
271		2nn0	$⊢ 2 \in ℕ_{0}$
272	271	a1i	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to 2 \in ℕ_{0}$
273		eluzp1p1	$⊢ ⌊\frac{\log A}{\log p}⌋ \in ℤ_{\geq 1} \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℤ_{\geq (1 + 1)}$
274	137 273	syl	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℤ_{\geq (1 + 1)}$
275		df-2	$⊢ 2 = 1 + 1$
276	275	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
277	274 276	eleqtrrdi	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to ⌊\frac{\log A}{\log p}⌋ + 1 \in ℤ_{\geq 2}$
278	213 270 272 277	geoserg	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k \in (2 ..^⌊\frac{\log A}{\log p}⌋ + 1)} {(\frac{1}{p})}^{k} = \frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})}$
279	269 278	eqtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} {(\frac{1}{p})}^{k} = \frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})}$
280	279	oveq2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \log p \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} {(\frac{1}{p})}^{k} = \log p (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})})$
281	262 266 280	3eqtr2d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) = \log p (\frac{{(\frac{1}{p})}^{2} - {(\frac{1}{p})}^{⌊\frac{\log A}{\log p}⌋ + 1}}{1 - (\frac{1}{p})})$
282	111	nncnd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p (p - 1) \in ℂ$
283	111	nnne0d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to p (p - 1) \neq 0$
284	125 282 283	divrecd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \frac{\log p}{p (p - 1)} = \log p (\frac{1}{p (p - 1)})$
285	248 281 284	3brtr4d	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 2}^{⌊\frac{\log A}{\log p}⌋} (\frac{\log p}{p^{k}}) \leq \frac{\log p}{p (p - 1)}$
286	198 285	eqbrtrd	$⊢ (A \in ℤ \land p \in ([0, A] \cap ℙ)) \to \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) \leq \frac{\log p}{p (p - 1)}$
287	83 105 112 286	fsumle	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) \leq \sum_{p \in [0, A] \cap ℙ} (\frac{\log p}{p (p - 1)})$
288		elfzuz	$⊢ p \in (2 \dots \|A\| + 1) \to p \in ℤ_{\geq 2}$
289		eluz2nn	$⊢ p \in ℤ_{\geq 2} \to p \in ℕ$
290	288 289	syl	$⊢ p \in (2 \dots \|A\| + 1) \to p \in ℕ$
291	290	adantl	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p \in ℕ$
292	291	nnred	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p \in ℝ$
293	288	adantl	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p \in ℤ_{\geq 2}$
294		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
295	293 294	syl	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to 1 < p$
296	292 295	rplogcld	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to \log p \in ℝ^{+}$
297	293 109	syl	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p - 1 \in ℕ$
298	291 297	nnmulcld	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p (p - 1) \in ℕ$
299	298	nnrpd	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to p (p - 1) \in ℝ^{+}$
300	296 299	rpdivcld	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to \frac{\log p}{p (p - 1)} \in ℝ^{+}$
301	300	rpred	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to \frac{\log p}{p (p - 1)} \in ℝ$
302	47 301	fsumrecl	$⊢ A \in ℤ \to \sum_{p = 2}^{\|A\| + 1} (\frac{\log p}{p (p - 1)}) \in ℝ$
303	300	rpge0d	$⊢ (A \in ℤ \land p \in (2 \dots \|A\| + 1)) \to 0 \leq \frac{\log p}{p (p - 1)}$
304	47 301 303 82	fsumless	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} (\frac{\log p}{p (p - 1)}) \leq \sum_{p = 2}^{\|A\| + 1} (\frac{\log p}{p (p - 1)})$
305		rplogsumlem1	$⊢ \|A\| + 1 \in ℕ \to \sum_{p = 2}^{\|A\| + 1} (\frac{\log p}{p (p - 1)}) \leq 2$
306	75 305	syl	$⊢ A \in ℤ \to \sum_{p = 2}^{\|A\| + 1} (\frac{\log p}{p (p - 1)}) \leq 2$
307	113 302 115 304 306	letrd	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} (\frac{\log p}{p (p - 1)}) \leq 2$
308	106 113 115 287 307	letrd	$⊢ A \in ℤ \to \sum_{p \in [0, A] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log A}{\log p}⌋} (\frac{Λ (p^{k}) - if (p^{k} \in ℙ, \log p^{k}, 0)}{p^{k}}) \leq 2$
309	46 308	eqbrtrd	$⊢ A \in ℤ \to \sum_{n = 1}^{A} (\frac{Λ (n) - if (n \in ℙ, \log n, 0)}{n}) \leq 2$

Metamath Proof Explorer

Theorem rplogsumlem2

Proof