rpvmasumlem

Description: Lemma for rpvmasum . Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n ) Lam ( n ) / n ) = log x + O(1) , where .1. ( x ) is the principal Dirichlet character. Equation 9.4.7 of Shapiro, p. 376. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
Assertion	rpvmasumlem	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		reex	$⊢ ℝ \in V$
8		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
9	7 8	ssexi	$⊢ ℝ^{+} \in V$
10	9	a1i	$⊢ φ \to ℝ^{+} \in V$
11		fzfid	$⊢ φ \to (1 \dots ⌊x⌋) \in Fin$
12		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
13	12	adantl	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
14		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
15	13 14	syl	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
16	15 13	nndivred	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
17	16	recnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
18	11 17	fsumcl	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
19	18	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \in ℂ$
20		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
21	20	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
22	21	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
23	19 22	subcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x \in ℂ$
24		1re	$⊢ 1 \in ℝ$
25		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
26	4 1 6 25 3	dchr1re	$⊢ φ \to \underset{˙}{1} : {Base}_{Z} ⟶ ℝ$
27	26	adantr	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} : {Base}_{Z} ⟶ ℝ$
28	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
29	1 25 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
30		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
31	28 29 30	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
32		elfzelz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ$
33		ffvelrn	$⊢ (L : ℤ ⟶ {Base}_{Z} \land n \in ℤ) \to L (n) \in {Base}_{Z}$
34	31 32 33	syl2an	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to L (n) \in {Base}_{Z}$
35	27 34	ffvelrnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} (L (n)) \in ℝ$
36		resubcl	$⊢ (1 \in ℝ \land \underset{˙}{1} (L (n)) \in ℝ) \to 1 - \underset{˙}{1} (L (n)) \in ℝ$
37	24 35 36	sylancr	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 - \underset{˙}{1} (L (n)) \in ℝ$
38	37 16	remulcld	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℝ$
39	38	recnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℂ$
40	11 39	fsumcl	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℂ$
41	40	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℂ$
42		eqidd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x)$
43		eqidd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}))$
44	10 23 41 42 43	offval2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}))$
45	19 22 41	sub32d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) - \log x$
46	11 17 39	fsumsub	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
47		1cnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
48	37	recnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 - \underset{˙}{1} (L (n)) \in ℂ$
49	47 48 17	subdird	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to (1 - (1 - \underset{˙}{1} (L (n)))) (\frac{Λ (n)}{n}) = 1 (\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
50		ax-1cn	$⊢ 1 \in ℂ$
51	35	recnd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} (L (n)) \in ℂ$
52		nncan	$⊢ (1 \in ℂ \land \underset{˙}{1} (L (n)) \in ℂ) \to 1 - (1 - \underset{˙}{1} (L (n))) = \underset{˙}{1} (L (n))$
53	50 51 52	sylancr	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 - (1 - \underset{˙}{1} (L (n))) = \underset{˙}{1} (L (n))$
54	53	oveq1d	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to (1 - (1 - \underset{˙}{1} (L (n)))) (\frac{Λ (n)}{n}) = \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
55	17	mulid2d	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 (\frac{Λ (n)}{n}) = \frac{Λ (n)}{n}$
56	55	oveq1d	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to 1 (\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = (\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
57	49 54 56	3eqtr3rd	$⊢ (φ \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
58	57	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} ((\frac{Λ (n)}{n}) - (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
59	46 58	eqtr3d	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
60	59	oveq1d	$⊢ φ \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) - \log x = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x$
61	60	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) - \log x = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x$
62	45 61	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x$
63	62	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x - \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x)$
64	44 63	eqtrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x)$
65		vmadivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
66	8	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
67		1red	$⊢ φ \to 1 \in ℝ$
68		prmdvdsfi	$⊢ N \in ℕ \to \{q \in ℙ \| q ∥ N\} \in Fin$
69	3 68	syl	$⊢ φ \to \{q \in ℙ \| q ∥ N\} \in Fin$
70		elrabi	$⊢ p \in \{q \in ℙ \| q ∥ N\} \to p \in ℙ$
71		prmnn	$⊢ p \in ℙ \to p \in ℕ$
72	71	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℕ$
73	72	nnrpd	$⊢ (φ \land p \in ℙ) \to p \in ℝ^{+}$
74	73	relogcld	$⊢ (φ \land p \in ℙ) \to \log p \in ℝ$
75		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
76	75	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℤ_{\geq 2}$
77		uz2m1nn	$⊢ p \in ℤ_{\geq 2} \to p - 1 \in ℕ$
78	76 77	syl	$⊢ (φ \land p \in ℙ) \to p - 1 \in ℕ$
79	74 78	nndivred	$⊢ (φ \land p \in ℙ) \to \frac{\log p}{p - 1} \in ℝ$
80	70 79	sylan2	$⊢ (φ \land p \in \{q \in ℙ \| q ∥ N\}) \to \frac{\log p}{p - 1} \in ℝ$
81	69 80	fsumrecl	$⊢ φ \to \sum_{p \in \{q \in ℙ \| q ∥ N\}} (\frac{\log p}{p - 1}) \in ℝ$
82		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
83		simpr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) = 0) \to \underset{˙}{1} (L (n)) = 0$
84		0re	$⊢ 0 \in ℝ$
85	83 84	eqeltrdi	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) = 0) \to \underset{˙}{1} (L (n)) \in ℝ$
86		eqid	$⊢ Unit (Z) = Unit (Z)$
87	3	ad3antrrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) \neq 0) \to N \in ℕ$
88	4	dchrabl	$⊢ N \in ℕ \to G \in Abel$
89		ablgrp	$⊢ G \in Abel \to G \in Grp$
90	5 6	grpidcl	$⊢ G \in Grp \to \underset{˙}{1} \in D$
91	3 88 89 90	4syl	$⊢ φ \to \underset{˙}{1} \in D$
92	91	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} \in D$
93	34	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to L (n) \in {Base}_{Z}$
94	4 1 5 25 86 92 93	dchrn0	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to (\underset{˙}{1} (L (n)) \neq 0 \leftrightarrow L (n) \in Unit (Z))$
95	94	biimpa	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) \neq 0) \to L (n) \in Unit (Z)$
96	4 1 6 86 87 95	dchr1	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) \neq 0) \to \underset{˙}{1} (L (n)) = 1$
97	96 24	eqeltrdi	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) \neq 0) \to \underset{˙}{1} (L (n)) \in ℝ$
98	85 97	pm2.61dane	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} (L (n)) \in ℝ$
99	24 98 36	sylancr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 1 - \underset{˙}{1} (L (n)) \in ℝ$
100	16	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
101	99 100	remulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℝ$
102	82 101	fsumrecl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℝ$
103		0le1	$⊢ 0 \leq 1$
104	83 103	eqbrtrdi	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) = 0) \to \underset{˙}{1} (L (n)) \leq 1$
105	24	leidi	$⊢ 1 \leq 1$
106	96 105	eqbrtrdi	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \land \underset{˙}{1} (L (n)) \neq 0) \to \underset{˙}{1} (L (n)) \leq 1$
107	104 106	pm2.61dane	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \underset{˙}{1} (L (n)) \leq 1$
108		subge0	$⊢ (1 \in ℝ \land \underset{˙}{1} (L (n)) \in ℝ) \to (0 \leq 1 - \underset{˙}{1} (L (n)) \leftrightarrow \underset{˙}{1} (L (n)) \leq 1)$
109	24 98 108	sylancr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to (0 \leq 1 - \underset{˙}{1} (L (n)) \leftrightarrow \underset{˙}{1} (L (n)) \leq 1)$
110	107 109	mpbird	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq 1 - \underset{˙}{1} (L (n))$
111	15	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
112	12	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
113		vmage0	$⊢ n \in ℕ \to 0 \leq Λ (n)$
114	112 113	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq Λ (n)$
115	112	nnred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
116	112	nngt0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 0 < n$
117		divge0	$⊢ ((Λ (n) \in ℝ \land 0 \leq Λ (n)) \land (n \in ℝ \land 0 < n)) \to 0 \leq \frac{Λ (n)}{n}$
118	111 114 115 116 117	syl22anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{Λ (n)}{n}$
119	99 100 110 118	mulge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
120	82 101 119	fsumge0	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
121	102 120	absidd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})\| = \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})$
122	69	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \{q \in ℙ \| q ∥ N\} \in Fin$
123		inss2	$⊢ [0, x] \cap ℙ \subseteq ℙ$
124		rabss2	$⊢ [0, x] \cap ℙ \subseteq ℙ \to \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \subseteq \{q \in ℙ \| q ∥ N\}$
125	123 124	mp1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \subseteq \{q \in ℙ \| q ∥ N\}$
126	122 125	ssfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \in Fin$
127		ssrab2	$⊢ \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \subseteq [0, x] \cap ℙ$
128	127 123	sstri	$⊢ \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \subseteq ℙ$
129	128	sseli	$⊢ p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \to p \in ℙ$
130	79	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{\log p}{p - 1} \in ℝ$
131	129 130	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}) \to \frac{\log p}{p - 1} \in ℝ$
132	126 131	fsumrecl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} (\frac{\log p}{p - 1}) \in ℝ$
133	81	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{p \in \{q \in ℙ \| q ∥ N\}} (\frac{\log p}{p - 1}) \in ℝ$
134		2fveq3	$⊢ n = p^{k} \to \underset{˙}{1} (L (n)) = \underset{˙}{1} (L (p^{k}))$
135	134	oveq2d	$⊢ n = p^{k} \to 1 - \underset{˙}{1} (L (n)) = 1 - \underset{˙}{1} (L (p^{k}))$
136		fveq2	$⊢ n = p^{k} \to Λ (n) = Λ (p^{k})$
137		id	$⊢ n = p^{k} \to n = p^{k}$
138	136 137	oveq12d	$⊢ n = p^{k} \to \frac{Λ (n)}{n} = \frac{Λ (p^{k})}{p^{k}}$
139	135 138	oveq12d	$⊢ n = p^{k} \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}})$
140		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
141	140	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
142	39	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \in ℂ$
143		simprr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to Λ (n) = 0$
144	143	oveq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to \frac{Λ (n)}{n} = \frac{0}{n}$
145	12	ad2antrl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to n \in ℕ$
146	145	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to n \in ℂ$
147	145	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to n \neq 0$
148	146 147	div0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to \frac{0}{n} = 0$
149	144 148	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to \frac{Λ (n)}{n} = 0$
150	149	oveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = (1 - \underset{˙}{1} (L (n))) \cdot 0$
151	48	ad2ant2r	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to 1 - \underset{˙}{1} (L (n)) \in ℂ$
152	151	mul01d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to (1 - \underset{˙}{1} (L (n))) \cdot 0 = 0$
153	150 152	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land Λ (n) = 0)) \to (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = 0$
154	139 141 142 153	fsumvma2	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \sum_{p \in [0, x] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}})$
155	127	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \{q \in ([0, x] \cap ℙ) \| q ∥ N\} \subseteq [0, x] \cap ℙ$
156		fzfid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (1 \dots ⌊\frac{\log x}{\log p}⌋) \in Fin$
157	26	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \underset{˙}{1} : {Base}_{Z} ⟶ ℝ$
158	31	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to L : ℤ ⟶ {Base}_{Z}$
159	71	ad2antrl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p \in ℕ$
160		elfznn	$⊢ k \in (1 \dots ⌊\frac{\log x}{\log p}⌋) \to k \in ℕ$
161	160	ad2antll	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to k \in ℕ$
162	161	nnnn0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to k \in ℕ_{0}$
163	159 162	nnexpcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p^{k} \in ℕ$
164	163	nnzd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p^{k} \in ℤ$
165	158 164	ffvelrnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to L (p^{k}) \in {Base}_{Z}$
166	157 165	ffvelrnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \underset{˙}{1} (L (p^{k})) \in ℝ$
167		resubcl	$⊢ (1 \in ℝ \land \underset{˙}{1} (L (p^{k})) \in ℝ) \to 1 - \underset{˙}{1} (L (p^{k})) \in ℝ$
168	24 166 167	sylancr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 1 - \underset{˙}{1} (L (p^{k})) \in ℝ$
169		vmacl	$⊢ p^{k} \in ℕ \to Λ (p^{k}) \in ℝ$
170	163 169	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to Λ (p^{k}) \in ℝ$
171	170 163	nndivred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{Λ (p^{k})}{p^{k}} \in ℝ$
172	168 171	remulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℝ$
173	172	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℝ$
174	173	recnd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℂ$
175	156 174	fsumcl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℂ$
176	129 175	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℂ$
177		breq1	$⊢ q = p \to (q ∥ N \leftrightarrow p ∥ N)$
178	177	notbid	$⊢ q = p \to (\neg q ∥ N \leftrightarrow \neg p ∥ N)$
179		notrab	$⊢ ([0, x] \cap ℙ) ∖ \{q \in ([0, x] \cap ℙ) \| q ∥ N\} = \{q \in ([0, x] \cap ℙ) \| \neg q ∥ N\}$
180	178 179	elrab2	$⊢ p \in (([0, x] \cap ℙ) ∖ \{q \in ([0, x] \cap ℙ) \| q ∥ N\}) \leftrightarrow (p \in ([0, x] \cap ℙ) \land \neg p ∥ N)$
181	123	sseli	$⊢ p \in ([0, x] \cap ℙ) \to p \in ℙ$
182	3	ad3antrrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to N \in ℕ$
183		simplrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to \neg p ∥ N$
184		simplrl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p \in ℙ$
185	182	nnzd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to N \in ℤ$
186		coprm	$⊢ (p \in ℙ \land N \in ℤ) \to (\neg p ∥ N \leftrightarrow p \gcd N = 1)$
187	184 185 186	syl2anc	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (\neg p ∥ N \leftrightarrow p \gcd N = 1)$
188	183 187	mpbid	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p \gcd N = 1$
189		prmz	$⊢ p \in ℙ \to p \in ℤ$
190	184 189	syl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p \in ℤ$
191	160	adantl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to k \in ℕ$
192	191	nnnn0d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to k \in ℕ_{0}$
193		rpexp1i	$⊢ (p \in ℤ \land N \in ℤ \land k \in ℕ_{0}) \to (p \gcd N = 1 \to p^{k} \gcd N = 1)$
194	190 185 192 193	syl3anc	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (p \gcd N = 1 \to p^{k} \gcd N = 1)$
195	188 194	mpd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p^{k} \gcd N = 1$
196	182	nnnn0d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to N \in ℕ_{0}$
197	164	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p^{k} \in ℤ$
198	197	adantlrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to p^{k} \in ℤ$
199	1 86 2	znunit	$⊢ (N \in ℕ_{0} \land p^{k} \in ℤ) \to (L (p^{k}) \in Unit (Z) \leftrightarrow p^{k} \gcd N = 1)$
200	196 198 199	syl2anc	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (L (p^{k}) \in Unit (Z) \leftrightarrow p^{k} \gcd N = 1)$
201	195 200	mpbird	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to L (p^{k}) \in Unit (Z)$
202	4 1 6 86 182 201	dchr1	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to \underset{˙}{1} (L (p^{k})) = 1$
203	202	oveq2d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to 1 - \underset{˙}{1} (L (p^{k})) = 1 - 1$
204		1m1e0	$⊢ 1 - 1 = 0$
205	203 204	syl6eq	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to 1 - \underset{˙}{1} (L (p^{k})) = 0$
206	205	oveq1d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = 0 \cdot (\frac{Λ (p^{k})}{p^{k}})$
207	171	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{Λ (p^{k})}{p^{k}} \in ℂ$
208	207	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to \frac{Λ (p^{k})}{p^{k}} \in ℂ$
209	208	adantlrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to \frac{Λ (p^{k})}{p^{k}} \in ℂ$
210	209	mul02d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to 0 \cdot (\frac{Λ (p^{k})}{p^{k}}) = 0$
211	206 210	eqtrd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = 0$
212	211	sumeq2dv	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} 0$
213		fzfid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \to (1 \dots ⌊\frac{\log x}{\log p}⌋) \in Fin$
214	213	olcd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \to ((1 \dots ⌊\frac{\log x}{\log p}⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊\frac{\log x}{\log p}⌋) \in Fin)$
215		sumz	$⊢ ((1 \dots ⌊\frac{\log x}{\log p}⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊\frac{\log x}{\log p}⌋) \in Fin) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} 0 = 0$
216	214 215	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} 0 = 0$
217	212 216	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land \neg p ∥ N)) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = 0$
218	181 217	sylanr1	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ([0, x] \cap ℙ) \land \neg p ∥ N)) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = 0$
219	180 218	sylan2b	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in (([0, x] \cap ℙ) ∖ \{q \in ([0, x] \cap ℙ) \| q ∥ N\})) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = 0$
220		ppifi	$⊢ x \in ℝ \to [0, x] \cap ℙ \in Fin$
221	141 220	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to [0, x] \cap ℙ \in Fin$
222	155 176 219 221	fsumss	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) = \sum_{p \in [0, x] \cap ℙ} \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}})$
223	154 222	eqtr4d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) = \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}})$
224	156 173	fsumrecl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℝ$
225	129 224	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \in ℝ$
226	74	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p \in ℝ$
227	71	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p \in ℕ$
228	227	nnrecred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p} \in ℝ$
229	227	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p \in ℝ^{+}$
230	229	rpreccld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p} \in ℝ^{+}$
231		simplrl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to x \in ℝ^{+}$
232	231	relogcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log x \in ℝ$
233	227	nnred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p \in ℝ$
234	75	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p \in ℤ_{\geq 2}$
235		eluz2gt1	$⊢ p \in ℤ_{\geq 2} \to 1 < p$
236	234 235	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 1 < p$
237	233 236	rplogcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p \in ℝ^{+}$
238	232 237	rerpdivcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{\log x}{\log p} \in ℝ$
239	238	flcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to ⌊\frac{\log x}{\log p}⌋ \in ℤ$
240	239	peano2zd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to ⌊\frac{\log x}{\log p}⌋ + 1 \in ℤ$
241	230 240	rpexpcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \in ℝ^{+}$
242	241	rpred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \in ℝ$
243	228 242	resubcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \in ℝ$
244	234 77	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p - 1 \in ℕ$
245	244	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p - 1 \in ℝ^{+}$
246	245 229	rpdivcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{p - 1}{p} \in ℝ^{+}$
247	243 246	rerpdivcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}} \in ℝ$
248	226 247	remulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}) \in ℝ$
249	170	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to Λ (p^{k}) \in ℂ$
250	163	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p^{k} \in ℂ$
251	163	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p^{k} \neq 0$
252	249 250 251	divrecd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{Λ (p^{k})}{p^{k}} = Λ (p^{k}) (\frac{1}{p^{k}})$
253		simprl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p \in ℙ$
254		vmappw	$⊢ (p \in ℙ \land k \in ℕ) \to Λ (p^{k}) = \log p$
255	253 161 254	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to Λ (p^{k}) = \log p$
256	159	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p \in ℂ$
257	159	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p \neq 0$
258		elfzelz	$⊢ k \in (1 \dots ⌊\frac{\log x}{\log p}⌋) \to k \in ℤ$
259	258	ad2antll	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to k \in ℤ$
260	256 257 259	exprecd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to {(\frac{1}{p})}^{k} = \frac{1}{p^{k}}$
261	260	eqcomd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{1}{p^{k}} = {(\frac{1}{p})}^{k}$
262	255 261	oveq12d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to Λ (p^{k}) (\frac{1}{p^{k}}) = \log p {(\frac{1}{p})}^{k}$
263	252 262	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{Λ (p^{k})}{p^{k}} = \log p {(\frac{1}{p})}^{k}$
264	263 171	eqeltrrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \log p {(\frac{1}{p})}^{k} \in ℝ$
265	264	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to \log p {(\frac{1}{p})}^{k} \in ℝ$
266		1red	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 1 \in ℝ$
267		vmage0	$⊢ p^{k} \in ℕ \to 0 \leq Λ (p^{k})$
268	163 267	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 0 \leq Λ (p^{k})$
269	163	nnred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to p^{k} \in ℝ$
270	163	nngt0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 0 < p^{k}$
271		divge0	$⊢ ((Λ (p^{k}) \in ℝ \land 0 \leq Λ (p^{k})) \land (p^{k} \in ℝ \land 0 < p^{k})) \to 0 \leq \frac{Λ (p^{k})}{p^{k}}$
272	170 268 269 270 271	syl22anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 0 \leq \frac{Λ (p^{k})}{p^{k}}$
273	84	leidi	$⊢ 0 \leq 0$
274		simpr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) = 0) \to \underset{˙}{1} (L (p^{k})) = 0$
275	273 274	breqtrrid	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) = 0) \to 0 \leq \underset{˙}{1} (L (p^{k}))$
276	3	ad3antrrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) \neq 0) \to N \in ℕ$
277	91	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \underset{˙}{1} \in D$
278	4 1 5 25 86 277 165	dchrn0	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to (\underset{˙}{1} (L (p^{k})) \neq 0 \leftrightarrow L (p^{k}) \in Unit (Z))$
279	278	biimpa	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) \neq 0) \to L (p^{k}) \in Unit (Z)$
280	4 1 6 86 276 279	dchr1	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) \neq 0) \to \underset{˙}{1} (L (p^{k})) = 1$
281	103 280	breqtrrid	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \land \underset{˙}{1} (L (p^{k})) \neq 0) \to 0 \leq \underset{˙}{1} (L (p^{k}))$
282	275 281	pm2.61dane	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 0 \leq \underset{˙}{1} (L (p^{k}))$
283		subge02	$⊢ (1 \in ℝ \land \underset{˙}{1} (L (p^{k})) \in ℝ) \to (0 \leq \underset{˙}{1} (L (p^{k})) \leftrightarrow 1 - \underset{˙}{1} (L (p^{k})) \leq 1)$
284	24 166 283	sylancr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to (0 \leq \underset{˙}{1} (L (p^{k})) \leftrightarrow 1 - \underset{˙}{1} (L (p^{k})) \leq 1)$
285	282 284	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 1 - \underset{˙}{1} (L (p^{k})) \leq 1$
286	168 266 171 272 285	lemul1ad	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq 1 (\frac{Λ (p^{k})}{p^{k}})$
287	207	mulid2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 1 (\frac{Λ (p^{k})}{p^{k}}) = \frac{Λ (p^{k})}{p^{k}}$
288	287 263	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to 1 (\frac{Λ (p^{k})}{p^{k}}) = \log p {(\frac{1}{p})}^{k}$
289	286 288	breqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \log p {(\frac{1}{p})}^{k}$
290	289	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \log p {(\frac{1}{p})}^{k}$
291	156 173 265 290	fsumle	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} \log p {(\frac{1}{p})}^{k}$
292	226	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p \in ℂ$
293	159	nnrecred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to \frac{1}{p} \in ℝ$
294	293 162	reexpcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to {(\frac{1}{p})}^{k} \in ℝ$
295	294	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (p \in ℙ \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋))) \to {(\frac{1}{p})}^{k} \in ℂ$
296	295	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \land k \in (1 \dots ⌊\frac{\log x}{\log p}⌋)) \to {(\frac{1}{p})}^{k} \in ℂ$
297	156 292 296	fsummulc2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} {(\frac{1}{p})}^{k} = \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} \log p {(\frac{1}{p})}^{k}$
298		fzval3	$⊢ ⌊\frac{\log x}{\log p}⌋ \in ℤ \to (1 \dots ⌊\frac{\log x}{\log p}⌋) = (1 ..^⌊\frac{\log x}{\log p}⌋ + 1)$
299	239 298	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (1 \dots ⌊\frac{\log x}{\log p}⌋) = (1 ..^⌊\frac{\log x}{\log p}⌋ + 1)$
300	299	sumeq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} {(\frac{1}{p})}^{k} = \sum_{k \in (1 ..^⌊\frac{\log x}{\log p}⌋ + 1)} {(\frac{1}{p})}^{k}$
301	228	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p} \in ℂ$
302	227	nngt0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 0 < p$
303		recgt1	$⊢ (p \in ℝ \land 0 < p) \to (1 < p \leftrightarrow \frac{1}{p} < 1)$
304	233 302 303	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (1 < p \leftrightarrow \frac{1}{p} < 1)$
305	236 304	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p} < 1$
306	228 305	ltned	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p} \neq 1$
307		1nn0	$⊢ 1 \in ℕ_{0}$
308	307	a1i	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 1 \in ℕ_{0}$
309		log1	$⊢ \log 1 = 0$
310		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
311		1rp	$⊢ 1 \in ℝ^{+}$
312		simprl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
313		logleb	$⊢ (1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
314	311 312 313	sylancr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
315	310 314	mpbid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log 1 \leq \log x$
316	309 315	eqbrtrrid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \log x$
317	316	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 0 \leq \log x$
318	232 237 317	divge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 0 \leq \frac{\log x}{\log p}$
319		flge0nn0	$⊢ (\frac{\log x}{\log p} \in ℝ \land 0 \leq \frac{\log x}{\log p}) \to ⌊\frac{\log x}{\log p}⌋ \in ℕ_{0}$
320	238 318 319	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to ⌊\frac{\log x}{\log p}⌋ \in ℕ_{0}$
321		nn0p1nn	$⊢ ⌊\frac{\log x}{\log p}⌋ \in ℕ_{0} \to ⌊\frac{\log x}{\log p}⌋ + 1 \in ℕ$
322	320 321	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to ⌊\frac{\log x}{\log p}⌋ + 1 \in ℕ$
323		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
324	322 323	eleqtrdi	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to ⌊\frac{\log x}{\log p}⌋ + 1 \in ℤ_{\geq 1}$
325	301 306 308 324	geoserg	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k \in (1 ..^⌊\frac{\log x}{\log p}⌋ + 1)} {(\frac{1}{p})}^{k} = \frac{{(\frac{1}{p})}^{1} - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{1 - (\frac{1}{p})}$
326	301	exp1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to {(\frac{1}{p})}^{1} = \frac{1}{p}$
327	326	oveq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to {(\frac{1}{p})}^{1} - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} = (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}$
328	227	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p \in ℂ$
329		1cnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 1 \in ℂ$
330	229	rpcnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (p \in ℂ \land p \neq 0)$
331		divsubdir	$⊢ (p \in ℂ \land 1 \in ℂ \land (p \in ℂ \land p \neq 0)) \to \frac{p - 1}{p} = (\frac{p}{p}) - (\frac{1}{p})$
332	328 329 330 331	syl3anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{p - 1}{p} = (\frac{p}{p}) - (\frac{1}{p})$
333		divid	$⊢ (p \in ℂ \land p \neq 0) \to \frac{p}{p} = 1$
334	330 333	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{p}{p} = 1$
335	334	oveq1d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{p}{p}) - (\frac{1}{p}) = 1 - (\frac{1}{p})$
336	332 335	eqtr2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 1 - (\frac{1}{p}) = \frac{p - 1}{p}$
337	327 336	oveq12d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{{(\frac{1}{p})}^{1} - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{1 - (\frac{1}{p})} = \frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}$
338	300 325 337	3eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} {(\frac{1}{p})}^{k} = \frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}$
339	338	oveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} {(\frac{1}{p})}^{k} = \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}})$
340	297 339	eqtr3d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} \log p {(\frac{1}{p})}^{k} = \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}})$
341	291 340	breqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}})$
342	241	rpge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 0 \leq {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}$
343	228 242	subge02d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (0 \leq {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \leftrightarrow (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \leq \frac{1}{p})$
344	342 343	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \leq \frac{1}{p}$
345	245	rpcnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (p - 1 \in ℂ \land p - 1 \neq 0)$
346		dmdcan	$⊢ ((p - 1 \in ℂ \land p - 1 \neq 0) \land (p \in ℂ \land p \neq 0) \land 1 \in ℂ) \to (\frac{p - 1}{p}) (\frac{1}{p - 1}) = \frac{1}{p}$
347	345 330 329 346	syl3anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{p - 1}{p}) (\frac{1}{p - 1}) = \frac{1}{p}$
348	344 347	breqtrrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \leq (\frac{p - 1}{p}) (\frac{1}{p - 1})$
349	244	nnrecred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{1}{p - 1} \in ℝ$
350	243 349 246	ledivmuld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}} \leq \frac{1}{p - 1} \leftrightarrow (\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1} \leq (\frac{p - 1}{p}) (\frac{1}{p - 1}))$
351	348 350	mpbird	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}} \leq \frac{1}{p - 1}$
352	247 349 237	lemul2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}} \leq \frac{1}{p - 1} \leftrightarrow \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}) \leq \log p (\frac{1}{p - 1}))$
353	351 352	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}) \leq \log p (\frac{1}{p - 1})$
354	244	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p - 1 \in ℂ$
355	244	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to p - 1 \neq 0$
356	292 354 355	divrecd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{\log p}{p - 1} = \log p (\frac{1}{p - 1})$
357	353 356	breqtrrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \log p (\frac{(\frac{1}{p}) - {(\frac{1}{p})}^{⌊\frac{\log x}{\log p}⌋ + 1}}{\frac{p - 1}{p}}) \leq \frac{\log p}{p - 1}$
358	224 248 130 341 357	letrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \frac{\log p}{p - 1}$
359	129 358	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}) \to \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \frac{\log p}{p - 1}$
360	126 225 131 359	fsumle	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} \sum_{k = 1}^{⌊\frac{\log x}{\log p}⌋} (1 - \underset{˙}{1} (L (p^{k}))) (\frac{Λ (p^{k})}{p^{k}}) \leq \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} (\frac{\log p}{p - 1})$
361	223 360	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \leq \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} (\frac{\log p}{p - 1})$
362	80	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ℙ \| q ∥ N\}) \to \frac{\log p}{p - 1} \in ℝ$
363	237 245	rpdivcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to \frac{\log p}{p - 1} \in ℝ^{+}$
364	363	rpge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in ℙ) \to 0 \leq \frac{\log p}{p - 1}$
365	70 364	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land p \in \{q \in ℙ \| q ∥ N\}) \to 0 \leq \frac{\log p}{p - 1}$
366	122 362 365 125	fsumless	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{p \in \{q \in ([0, x] \cap ℙ) \| q ∥ N\}} (\frac{\log p}{p - 1}) \leq \sum_{p \in \{q \in ℙ \| q ∥ N\}} (\frac{\log p}{p - 1})$
367	102 132 133 361 366	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n}) \leq \sum_{p \in \{q \in ℙ \| q ∥ N\}} (\frac{\log p}{p - 1})$
368	121 367	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})\| \leq \sum_{p \in \{q \in ℙ \| q ∥ N\}} (\frac{\log p}{p - 1})$
369	66 41 67 81 368	elo1d	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) \in 𝑂 (1)$
370		o1sub	$⊢ ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) \in 𝑂 (1)$
371	65 369 370	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) - \log x) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (1 - \underset{˙}{1} (L (n))) (\frac{Λ (n)}{n})) \in 𝑂 (1)$
372	64 371	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem rpvmasumlem

Proof