rpvmasum2

Description: A partial result along the lines of rpvmasum . The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to ( 1 - M ) ( log x / phi ( x ) ) + O(1) , where M is the number of non-principal Dirichlet characters with sum_ n e. NN , X ( n ) / n = 0 . Our goal is to show this set is empty. Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum2.g	$⊢ G = DChr (N)$
	rpvmasum2.d	$⊢ D = {Base}_{G}$
	rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
	rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
	rpvmasum2.u	$⊢ U = Unit (Z)$
	rpvmasum2.b	$⊢ φ \to A \in U$
	rpvmasum2.t	$⊢ T = L^{-1} [\{A\}]$
	rpvmasum2.z1	$⊢ (φ \land f \in W) \to A = 1_{Z}$
Assertion	rpvmasum2	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)) \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		rpvmasum2.g	$⊢ G = DChr (N)$
5		rpvmasum2.d	$⊢ D = {Base}_{G}$
6		rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
7		rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
8		rpvmasum2.u	$⊢ U = Unit (Z)$
9		rpvmasum2.b	$⊢ φ \to A \in U$
10		rpvmasum2.t	$⊢ T = L^{-1} [\{A\}]$
11		rpvmasum2.z1	$⊢ (φ \land f \in W) \to A = 1_{Z}$
12	3	adantr	$⊢ (φ \land x \in ℝ^{+}) \to N \in ℕ$
13	4 5	dchrfi	$⊢ N \in ℕ \to D \in Fin$
14	12 13	syl	$⊢ (φ \land x \in ℝ^{+}) \to D \in Fin$
15		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to (1 \dots ⌊x⌋) \in Fin$
16		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
17		simpr	$⊢ (φ \land f \in D) \to f \in D$
18	4 1 5 16 17	dchrf	$⊢ (φ \land f \in D) \to f : {Base}_{Z} ⟶ ℂ$
19	16 8	unitss	$⊢ U \subseteq {Base}_{Z}$
20	19 9	sseldi	$⊢ φ \to A \in {Base}_{Z}$
21	20	adantr	$⊢ (φ \land f \in D) \to A \in {Base}_{Z}$
22	18 21	ffvelrnd	$⊢ (φ \land f \in D) \to f (A) \in ℂ$
23	22	cjcld	$⊢ (φ \land f \in D) \to \overline{f (A)} \in ℂ$
24	23	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \in ℂ$
25	24	adantrl	$⊢ ((φ \land x \in ℝ^{+}) \land (n \in (1 \dots ⌊x⌋) \land f \in D)) \to \overline{f (A)} \in ℂ$
26	18	ad4ant14	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to f : {Base}_{Z} ⟶ ℂ$
27	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
28	1 16 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
29		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
30	27 28 29	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
31	30	adantr	$⊢ (φ \land x \in ℝ^{+}) \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 x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to L (n) \in {Base}_{Z}$
35	34	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to L (n) \in {Base}_{Z}$
36	26 35	ffvelrnd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to f (L (n)) \in ℂ$
37	36	anasss	$⊢ ((φ \land x \in ℝ^{+}) \land (n \in (1 \dots ⌊x⌋) \land f \in D)) \to f (L (n)) \in ℂ$
38		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
39	38	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
40		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
41	39 40	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
42	41 39	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
43	42	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
44	43	adantrr	$⊢ ((φ \land x \in ℝ^{+}) \land (n \in (1 \dots ⌊x⌋) \land f \in D)) \to \frac{Λ (n)}{n} \in ℂ$
45	37 44	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land (n \in (1 \dots ⌊x⌋) \land f \in D)) \to f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
46	25 45	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land (n \in (1 \dots ⌊x⌋) \land f \in D)) \to \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
47	46	anass1rs	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land n \in (1 \dots ⌊x⌋)) \to \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
48	15 47	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
49		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
50	49	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
51	50	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
52	51	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \log x \in ℂ$
53		ax-1cn	$⊢ 1 \in ℂ$
54		neg1cn	$⊢ - 1 \in ℂ$
55		0cn	$⊢ 0 \in ℂ$
56	54 55	ifcli	$⊢ if (f \in W, - 1, 0) \in ℂ$
57	53 56	ifcli	$⊢ if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
58		mulcl	$⊢ (\log x \in ℂ \land if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ) \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
59	52 57 58	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
60	14 48 59	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D} (\sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = \sum_{f \in D} \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \sum_{f \in D} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
61	45	anass1rs	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land n \in (1 \dots ⌊x⌋)) \to f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
62	15 61	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
63	24 62 59	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = \overline{f (A)} \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \overline{f (A)} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
64	15 24 61	fsummulc2	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
65	57	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
66	24 52 65	mul12d	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \overline{f (A)} if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
67		ovif2	$⊢ \overline{f (A)} if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = if (f = \underset{˙}{1}, \overline{f (A)} \cdot 1, \overline{f (A)} if (f \in W, - 1, 0))$
68		fveq1	$⊢ f = \underset{˙}{1} \to f (A) = \underset{˙}{1} (A)$
69	3	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to N \in ℕ$
70	9	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to A \in U$
71	4 1 6 8 69 70	dchr1	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \underset{˙}{1} (A) = 1$
72	68 71	sylan9eqr	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f = \underset{˙}{1}) \to f (A) = 1$
73	72	fveq2d	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f = \underset{˙}{1}) \to \overline{f (A)} = \overline{1}$
74		1re	$⊢ 1 \in ℝ$
75		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
76	74 75	ax-mp	$⊢ \overline{1} = 1$
77	73 76	syl6eq	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f = \underset{˙}{1}) \to \overline{f (A)} = 1$
78	77	oveq1d	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f = \underset{˙}{1}) \to \overline{f (A)} \cdot 1 = 1 \cdot 1$
79		1t1e1	$⊢ 1 \cdot 1 = 1$
80	78 79	syl6eq	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f = \underset{˙}{1}) \to \overline{f (A)} \cdot 1 = 1$
81		df-ne	$⊢ f \neq \underset{˙}{1} \leftrightarrow \neg f = \underset{˙}{1}$
82		ovif2	$⊢ \overline{f (A)} if (f \in W, - 1, 0) = if (f \in W, \overline{f (A)} -1, \overline{f (A)} \cdot 0)$
83	11	fveq2d	$⊢ (φ \land f \in W) \to f (A) = f (1_{Z})$
84	83	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to f (A) = f (1_{Z})$
85	4 1 5	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
86		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to f \in D$
87	85 86	sseldi	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to f \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
88		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
89		eqid	$⊢ 1_{Z} = 1_{Z}$
90	88 89	ringidval	$⊢ 1_{Z} = 0_{{mulGrp}_{Z}}$
91		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
92		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
93	91 92	ringidval	$⊢ 1 = 0_{{mulGrp}_{ℂ_{fld}}}$
94	90 93	mhm0	$⊢ f \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \to f (1_{Z}) = 1$
95	87 94	syl	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to f (1_{Z}) = 1$
96	95	ad2antrr	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to f (1_{Z}) = 1$
97	84 96	eqtrd	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to f (A) = 1$
98	97	fveq2d	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to \overline{f (A)} = \overline{1}$
99	98 76	syl6eq	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to \overline{f (A)} = 1$
100	99	oveq1d	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to \overline{f (A)} -1 = 1 -1$
101	54	mulid2i	$⊢ 1 -1 = - 1$
102	100 101	syl6eq	$⊢ ((((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \land f \in W) \to \overline{f (A)} -1 = - 1$
103	102	ifeq1da	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to if (f \in W, \overline{f (A)} -1, \overline{f (A)} \cdot 0) = if (f \in W, - 1, \overline{f (A)} \cdot 0)$
104	24	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to \overline{f (A)} \in ℂ$
105	104	mul01d	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to \overline{f (A)} \cdot 0 = 0$
106	105	ifeq2d	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to if (f \in W, - 1, \overline{f (A)} \cdot 0) = if (f \in W, - 1, 0)$
107	103 106	eqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to if (f \in W, \overline{f (A)} -1, \overline{f (A)} \cdot 0) = if (f \in W, - 1, 0)$
108	82 107	syl5eq	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land f \neq \underset{˙}{1}) \to \overline{f (A)} if (f \in W, - 1, 0) = if (f \in W, - 1, 0)$
109	81 108	sylan2br	$⊢ (((φ \land x \in ℝ^{+}) \land f \in D) \land \neg f = \underset{˙}{1}) \to \overline{f (A)} if (f \in W, - 1, 0) = if (f \in W, - 1, 0)$
110	80 109	ifeq12da	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to if (f = \underset{˙}{1}, \overline{f (A)} \cdot 1, \overline{f (A)} if (f \in W, - 1, 0)) = if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
111	67 110	syl5eq	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
112	111	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \log x \overline{f (A)} if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
113	66 112	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
114	64 113	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \overline{f (A)} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
115	63 114	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
116	115	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D} \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = \sum_{f \in D} (\sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)))$
117		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
118		inss1	$⊢ (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)$
119		ssfi	$⊢ ((1 \dots ⌊x⌋) \in Fin \land (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \cap T \in Fin$
120	117 118 119	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap T \in Fin$
121	12	phicld	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℕ$
122	121	nncnd	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \in ℂ$
123	118	a1i	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋)$
124	123	sselda	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap T)) \to n \in (1 \dots ⌊x⌋)$
125	124 43	syldan	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap T)) \to \frac{Λ (n)}{n} \in ℂ$
126	120 122 125	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) = \sum_{n \in (1 \dots ⌊x⌋) \cap T} ϕ (N) (\frac{Λ (n)}{n})$
127	122	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to ϕ (N) \in ℂ$
128	127 43	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to ϕ (N) (\frac{Λ (n)}{n}) \in ℂ$
129	124 128	syldan	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ((1 \dots ⌊x⌋) \cap T)) \to ϕ (N) (\frac{Λ (n)}{n}) \in ℂ$
130	129	ralrimiva	$⊢ (φ \land x \in ℝ^{+}) \to \forall n \in ((1 \dots ⌊x⌋) \cap T) ϕ (N) (\frac{Λ (n)}{n}) \in ℂ$
131	117	olcd	$⊢ (φ \land x \in ℝ^{+}) \to ((1 \dots ⌊x⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊x⌋) \in Fin)$
132		sumss2	$⊢ (((1 \dots ⌊x⌋) \cap T \subseteq (1 \dots ⌊x⌋) \land \forall n \in ((1 \dots ⌊x⌋) \cap T) ϕ (N) (\frac{Λ (n)}{n}) \in ℂ) \land ((1 \dots ⌊x⌋) \subseteq ℤ_{\geq 1} \lor (1 \dots ⌊x⌋) \in Fin)) \to \sum_{n \in (1 \dots ⌊x⌋) \cap T} ϕ (N) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} if (n \in ((1 \dots ⌊x⌋) \cap T), ϕ (N) (\frac{Λ (n)}{n}), 0)$
133	123 130 131 132	syl21anc	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n \in (1 \dots ⌊x⌋) \cap T} ϕ (N) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} if (n \in ((1 \dots ⌊x⌋) \cap T), ϕ (N) (\frac{Λ (n)}{n}), 0)$
134		elin	$⊢ n \in ((1 \dots ⌊x⌋) \cap T) \leftrightarrow (n \in (1 \dots ⌊x⌋) \land n \in T)$
135	134	baib	$⊢ n \in (1 \dots ⌊x⌋) \to (n \in ((1 \dots ⌊x⌋) \cap T) \leftrightarrow n \in T)$
136	135	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (n \in ((1 \dots ⌊x⌋) \cap T) \leftrightarrow n \in T)$
137	10	eleq2i	$⊢ n \in T \leftrightarrow n \in L^{-1} [\{A\}]$
138	31	ffnd	$⊢ (φ \land x \in ℝ^{+}) \to L Fn ℤ$
139		fniniseg	$⊢ L Fn ℤ \to (n \in L^{-1} [\{A\}] \leftrightarrow (n \in ℤ \land L (n) = A))$
140	139	baibd	$⊢ (L Fn ℤ \land n \in ℤ) \to (n \in L^{-1} [\{A\}] \leftrightarrow L (n) = A)$
141	138 32 140	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (n \in L^{-1} [\{A\}] \leftrightarrow L (n) = A)$
142	137 141	syl5bb	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (n \in T \leftrightarrow L (n) = A)$
143	136 142	bitr2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (L (n) = A \leftrightarrow n \in ((1 \dots ⌊x⌋) \cap T))$
144	43	mul02d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \cdot (\frac{Λ (n)}{n}) = 0$
145	143 144	ifbieq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to if (L (n) = A, ϕ (N) (\frac{Λ (n)}{n}), 0 \cdot (\frac{Λ (n)}{n})) = if (n \in ((1 \dots ⌊x⌋) \cap T), ϕ (N) (\frac{Λ (n)}{n}), 0)$
146		ovif	$⊢ if (L (n) = A, ϕ (N), 0) (\frac{Λ (n)}{n}) = if (L (n) = A, ϕ (N) (\frac{Λ (n)}{n}), 0 \cdot (\frac{Λ (n)}{n}))$
147	3	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to N \in ℕ$
148	147 13	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to D \in Fin$
149	23	ad4ant14	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to \overline{f (A)} \in ℂ$
150	36 149	mulcld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to f (L (n)) \overline{f (A)} \in ℂ$
151	148 43 150	fsummulc1	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{f \in D} f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = \sum_{f \in D} f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n})$
152	9	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to A \in U$
153	4 5 1 16 8 147 34 152	sum2dchr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{f \in D} f (L (n)) \overline{f (A)} = if (L (n) = A, ϕ (N), 0)$
154	153	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{f \in D} f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = if (L (n) = A, ϕ (N), 0) (\frac{Λ (n)}{n})$
155	43	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to \frac{Λ (n)}{n} \in ℂ$
156		mulass	$⊢ (f (L (n)) \in ℂ \land \overline{f (A)} \in ℂ \land \frac{Λ (n)}{n} \in ℂ) \to f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n})$
157		mul12	$⊢ (f (L (n)) \in ℂ \land \overline{f (A)} \in ℂ \land \frac{Λ (n)}{n} \in ℂ) \to f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
158	156 157	eqtrd	$⊢ (f (L (n)) \in ℂ \land \overline{f (A)} \in ℂ \land \frac{Λ (n)}{n} \in ℂ) \to f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
159	36 149 155 158	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land f \in D) \to f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
160	159	sumeq2dv	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{f \in D} f (L (n)) \overline{f (A)} (\frac{Λ (n)}{n}) = \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
161	151 154 160	3eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to if (L (n) = A, ϕ (N), 0) (\frac{Λ (n)}{n}) = \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
162	146 161	syl5eqr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to if (L (n) = A, ϕ (N) (\frac{Λ (n)}{n}), 0 \cdot (\frac{Λ (n)}{n})) = \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
163	145 162	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to if (n \in ((1 \dots ⌊x⌋) \cap T), ϕ (N) (\frac{Λ (n)}{n}), 0) = \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
164	163	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} if (n \in ((1 \dots ⌊x⌋) \cap T), ϕ (N) (\frac{Λ (n)}{n}), 0) = \sum_{n = 1}^{⌊x⌋} \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
165	126 133 164	3eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
166	117 14 46	fsumcom	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} \sum_{f \in D} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) = \sum_{f \in D} \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
167	165 166	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) = \sum_{f \in D} \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n})$
168	4	dchrabl	$⊢ N \in ℕ \to G \in Abel$
169		ablgrp	$⊢ G \in Abel \to G \in Grp$
170	5 6	grpidcl	$⊢ G \in Grp \to \underset{˙}{1} \in D$
171	12 168 169 170	4syl	$⊢ (φ \land x \in ℝ^{+}) \to \underset{˙}{1} \in D$
172	51	mulid1d	$⊢ (φ \land x \in ℝ^{+}) \to \log x \cdot 1 = \log x$
173	172 51	eqeltrd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \cdot 1 \in ℂ$
174		iftrue	$⊢ f = \underset{˙}{1} \to if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = 1$
175	174	oveq2d	$⊢ f = \underset{˙}{1} \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \cdot 1$
176	175	sumsn	$⊢ (\underset{˙}{1} \in D \land \log x \cdot 1 \in ℂ) \to \sum_{f \in \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \cdot 1$
177	171 173 176	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \cdot 1$
178		eldifsn	$⊢ f \in (D ∖ \{\underset{˙}{1}\}) \leftrightarrow (f \in D \land f \neq \underset{˙}{1})$
179		ifnefalse	$⊢ f \neq \underset{˙}{1} \to if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = if (f \in W, - 1, 0)$
180	179	ad2antll	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = if (f \in W, - 1, 0)$
181		negeq	$⊢ if (f \in W, 1, 0) = 1 \to - if (f \in W, 1, 0) = - 1$
182		negeq	$⊢ if (f \in W, 1, 0) = 0 \to - if (f \in W, 1, 0) = - 0$
183		neg0	$⊢ - 0 = 0$
184	182 183	syl6eq	$⊢ if (f \in W, 1, 0) = 0 \to - if (f \in W, 1, 0) = 0$
185	181 184	ifsb	$⊢ - if (f \in W, 1, 0) = if (f \in W, - 1, 0)$
186	180 185	syl6eqr	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = - if (f \in W, 1, 0)$
187	186	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x (- if (f \in W, 1, 0))$
188	51	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to \log x \in ℂ$
189	53 55	ifcli	$⊢ if (f \in W, 1, 0) \in ℂ$
190		mulneg2	$⊢ (\log x \in ℂ \land if (f \in W, 1, 0) \in ℂ) \to \log x (- if (f \in W, 1, 0)) = - \log x if (f \in W, 1, 0)$
191	188 189 190	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to \log x (- if (f \in W, 1, 0)) = - \log x if (f \in W, 1, 0)$
192	187 191	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (f \in D \land f \neq \underset{˙}{1})) \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = - \log x if (f \in W, 1, 0)$
193	178 192	sylan2b	$⊢ ((φ \land x \in ℝ^{+}) \land f \in (D ∖ \{\underset{˙}{1}\})) \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = - \log x if (f \in W, 1, 0)$
194	193	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{f \in D ∖ \{\underset{˙}{1}\}} (- \log x if (f \in W, 1, 0))$
195		diffi	$⊢ D \in Fin \to D ∖ \{\underset{˙}{1}\} \in Fin$
196	14 195	syl	$⊢ (φ \land x \in ℝ^{+}) \to D ∖ \{\underset{˙}{1}\} \in Fin$
197	51	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in (D ∖ \{\underset{˙}{1}\})) \to \log x \in ℂ$
198		mulcl	$⊢ (\log x \in ℂ \land if (f \in W, 1, 0) \in ℂ) \to \log x if (f \in W, 1, 0) \in ℂ$
199	197 189 198	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land f \in (D ∖ \{\underset{˙}{1}\})) \to \log x if (f \in W, 1, 0) \in ℂ$
200	196 199	fsumneg	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D ∖ \{\underset{˙}{1}\}} (- \log x if (f \in W, 1, 0)) = - \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f \in W, 1, 0)$
201	189	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land f \in (D ∖ \{\underset{˙}{1}\})) \to if (f \in W, 1, 0) \in ℂ$
202	196 51 201	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to \log x \sum_{f \in D ∖ \{\underset{˙}{1}\}} if (f \in W, 1, 0) = \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f \in W, 1, 0)$
203	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
204		difss	$⊢ D ∖ \{\underset{˙}{1}\} \subseteq D$
205	203 204	sstri	$⊢ W \subseteq D$
206		ssfi	$⊢ (D \in Fin \land W \subseteq D) \to W \in Fin$
207	14 205 206	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to W \in Fin$
208		fsumconst	$⊢ (W \in Fin \land 1 \in ℂ) \to \sum_{f \in W} 1 = \|W\| \cdot 1$
209	207 53 208	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in W} 1 = \|W\| \cdot 1$
210	203	a1i	$⊢ (φ \land x \in ℝ^{+}) \to W \subseteq D ∖ \{\underset{˙}{1}\}$
211	53	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 1 \in ℂ$
212	211	ralrimivw	$⊢ (φ \land x \in ℝ^{+}) \to \forall f \in W 1 \in ℂ$
213	196	olcd	$⊢ (φ \land x \in ℝ^{+}) \to (D ∖ \{\underset{˙}{1}\} \subseteq ℤ_{\geq 1} \lor D ∖ \{\underset{˙}{1}\} \in Fin)$
214		sumss2	$⊢ ((W \subseteq D ∖ \{\underset{˙}{1}\} \land \forall f \in W 1 \in ℂ) \land (D ∖ \{\underset{˙}{1}\} \subseteq ℤ_{\geq 1} \lor D ∖ \{\underset{˙}{1}\} \in Fin)) \to \sum_{f \in W} 1 = \sum_{f \in D ∖ \{\underset{˙}{1}\}} if (f \in W, 1, 0)$
215	210 212 213 214	syl21anc	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in W} 1 = \sum_{f \in D ∖ \{\underset{˙}{1}\}} if (f \in W, 1, 0)$
216		hashcl	$⊢ W \in Fin \to \|W\| \in ℕ_{0}$
217	207 216	syl	$⊢ (φ \land x \in ℝ^{+}) \to \|W\| \in ℕ_{0}$
218	217	nn0cnd	$⊢ (φ \land x \in ℝ^{+}) \to \|W\| \in ℂ$
219	218	mulid1d	$⊢ (φ \land x \in ℝ^{+}) \to \|W\| \cdot 1 = \|W\|$
220	209 215 219	3eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D ∖ \{\underset{˙}{1}\}} if (f \in W, 1, 0) = \|W\|$
221	220	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \log x \sum_{f \in D ∖ \{\underset{˙}{1}\}} if (f \in W, 1, 0) = \log x \|W\|$
222	202 221	eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f \in W, 1, 0) = \log x \|W\|$
223	222	negeqd	$⊢ (φ \land x \in ℝ^{+}) \to - \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f \in W, 1, 0) = - \log x \|W\|$
224	194 200 223	3eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = - \log x \|W\|$
225	177 224	oveq12d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) + \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \cdot 1 + (- \log x \|W\|)$
226	51 218	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \log x \|W\| \in ℂ$
227	173 226	negsubd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \cdot 1 + (- \log x \|W\|) = \log x \cdot 1 - \log x \|W\|$
228	225 227	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) + \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x \cdot 1 - \log x \|W\|$
229		disjdif	$⊢ \{\underset{˙}{1}\} \cap (D ∖ \{\underset{˙}{1}\}) = \emptyset$
230	229	a1i	$⊢ (φ \land x \in ℝ^{+}) \to \{\underset{˙}{1}\} \cap (D ∖ \{\underset{˙}{1}\}) = \emptyset$
231		undif2	$⊢ \{\underset{˙}{1}\} \cup (D ∖ \{\underset{˙}{1}\}) = \{\underset{˙}{1}\} \cup D$
232	171	snssd	$⊢ (φ \land x \in ℝ^{+}) \to \{\underset{˙}{1}\} \subseteq D$
233		ssequn1	$⊢ \{\underset{˙}{1}\} \subseteq D \leftrightarrow \{\underset{˙}{1}\} \cup D = D$
234	232 233	sylib	$⊢ (φ \land x \in ℝ^{+}) \to \{\underset{˙}{1}\} \cup D = D$
235	231 234	syl5req	$⊢ (φ \land x \in ℝ^{+}) \to D = \{\underset{˙}{1}\} \cup (D ∖ \{\underset{˙}{1}\})$
236	230 235 14 59	fsumsplit	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{f \in \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) + \sum_{f \in D ∖ \{\underset{˙}{1}\}} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
237	51 211 218	subdid	$⊢ (φ \land x \in ℝ^{+}) \to \log x (1 - \|W\|) = \log x \cdot 1 - \log x \|W\|$
238	228 236 237	3eqtr4rd	$⊢ (φ \land x \in ℝ^{+}) \to \log x (1 - \|W\|) = \sum_{f \in D} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
239	167 238	oveq12d	$⊢ (φ \land x \in ℝ^{+}) \to ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|) = \sum_{f \in D} \sum_{n = 1}^{⌊x⌋} \overline{f (A)} f (L (n)) (\frac{Λ (n)}{n}) - \sum_{f \in D} \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))$
240	60 116 239	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{f \in D} \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)$
241	240	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{f \in D} \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)))) = (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|))$
242		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
243	242	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
244	3 13	syl	$⊢ φ \to D \in Fin$
245	22	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to f (A) \in ℂ$
246	245	cjcld	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} \in ℂ$
247	62 59	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
248	246 247	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land f \in D) \to \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) \in ℂ$
249	248	anasss	$⊢ (φ \land (x \in ℝ^{+} \land f \in D)) \to \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) \in ℂ$
250	23	adantr	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \overline{f (A)} \in ℂ$
251	247	an32s	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) \in ℂ$
252		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land \overline{f (A)} \in ℂ) \to (x \in ℝ^{+} ⟼ \overline{f (A)}) \in 𝑂 (1)$
253	242 23 252	sylancr	$⊢ (φ \land f \in D) \to (x \in ℝ^{+} ⟼ \overline{f (A)}) \in 𝑂 (1)$
254		fveq1	$⊢ f = \underset{˙}{1} \to f (L (n)) = \underset{˙}{1} (L (n))$
255	254	oveq1d	$⊢ f = \underset{˙}{1} \to f (L (n)) (\frac{Λ (n)}{n}) = \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
256	255	sumeq2sdv	$⊢ f = \underset{˙}{1} \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n})$
257	256 175	oveq12d	$⊢ f = \underset{˙}{1} \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x \cdot 1$
258	257	adantl	$⊢ ((φ \land f \in D) \land f = \underset{˙}{1}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x \cdot 1$
259	49	recnd	$⊢ x \in ℝ^{+} \to \log x \in ℂ$
260	259	mulid1d	$⊢ x \in ℝ^{+} \to \log x \cdot 1 = \log x$
261	260	oveq2d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x \cdot 1 = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x$
262	258 261	sylan9eq	$⊢ (((φ \land f \in D) \land f = \underset{˙}{1}) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x$
263	262	mpteq2dva	$⊢ ((φ \land f \in D) \land f = \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x)$
264	1 2 3 4 5 6	rpvmasumlem	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
265	264	ad2antrr	$⊢ ((φ \land f \in D) \land f = \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} \underset{˙}{1} (L (n)) (\frac{Λ (n)}{n}) - \log x) \in 𝑂 (1)$
266	263 265	eqeltrd	$⊢ ((φ \land f \in D) \land f = \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) \in 𝑂 (1)$
267	179	oveq2d	$⊢ f \neq \underset{˙}{1} \to \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \log x if (f \in W, - 1, 0)$
268	267	oveq2d	$⊢ f \neq \underset{˙}{1} \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f \in W, - 1, 0)$
269	51	adantlr	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \log x \in ℂ$
270		mulcom	$⊢ (\log x \in ℂ \land - 1 \in ℂ) \to \log x -1 = -1 \log x$
271	269 54 270	sylancl	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \log x -1 = -1 \log x$
272	269	mulm1d	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to -1 \log x = - \log x$
273	271 272	eqtrd	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \log x -1 = - \log x$
274	269	mul01d	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \log x \cdot 0 = 0$
275	273 274	ifeq12d	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to if (f \in W, \log x -1, \log x \cdot 0) = if (f \in W, - \log x, 0)$
276		ovif2	$⊢ \log x if (f \in W, - 1, 0) = if (f \in W, \log x -1, \log x \cdot 0)$
277		negeq	$⊢ if (f \in W, \log x, 0) = \log x \to - if (f \in W, \log x, 0) = - \log x$
278		negeq	$⊢ if (f \in W, \log x, 0) = 0 \to - if (f \in W, \log x, 0) = - 0$
279	278 183	syl6eq	$⊢ if (f \in W, \log x, 0) = 0 \to - if (f \in W, \log x, 0) = 0$
280	277 279	ifsb	$⊢ - if (f \in W, \log x, 0) = if (f \in W, - \log x, 0)$
281	275 276 280	3eqtr4g	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \log x if (f \in W, - 1, 0) = - if (f \in W, \log x, 0)$
282	281	oveq2d	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f \in W, - 1, 0) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - (- if (f \in W, \log x, 0))$
283	62	an32s	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
284		ifcl	$⊢ (\log x \in ℂ \land 0 \in ℂ) \to if (f \in W, \log x, 0) \in ℂ$
285	269 55 284	sylancl	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to if (f \in W, \log x, 0) \in ℂ$
286	283 285	subnegd	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - (- if (f \in W, \log x, 0)) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)$
287	282 286	eqtrd	$⊢ ((φ \land f \in D) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f \in W, - 1, 0) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)$
288	268 287	sylan9eqr	$⊢ (((φ \land f \in D) \land x \in ℝ^{+}) \land f \neq \underset{˙}{1}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)$
289	288	an32s	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)$
290	289	mpteq2dva	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0))$
291	3	ad2antrr	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to N \in ℕ$
292		simplr	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to f \in D$
293		simpr	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to f \neq \underset{˙}{1}$
294		eqid	$⊢ (a \in ℕ ⟼ \frac{f (L (a))}{a}) = (a \in ℕ ⟼ \frac{f (L (a))}{a})$
295	1 2 291 4 5 6 292 293 294	dchrmusumlema	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to \exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y})$
296	3	adantr	$⊢ (φ \land f \in D) \to N \in ℕ$
297	296	ad2antrr	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to N \in ℕ$
298	292	adantr	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to f \in D$
299		simplr	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to f \neq \underset{˙}{1}$
300		simprl	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to c \in [0, +∞)$
301		simprrl	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t$
302		simprrr	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}$
303	1 2 297 4 5 6 298 299 294 300 301 302 7	dchrvmaeq0	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (f \in W \leftrightarrow t = 0)$
304		ifbi	$⊢ (f \in W \leftrightarrow t = 0) \to if (f \in W, \log x, 0) = if (t = 0, \log x, 0)$
305	304	oveq2d	$⊢ (f \in W \leftrightarrow t = 0) \to \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0) = \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (t = 0, \log x, 0)$
306	305	mpteq2dv	$⊢ (f \in W \leftrightarrow t = 0) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (t = 0, \log x, 0))$
307	303 306	syl	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (t = 0, \log x, 0))$
308	1 2 297 4 5 6 298 299 294 300 301 302	dchrvmasumif	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (t = 0, \log x, 0)) \in 𝑂 (1)$
309	307 308	eqeltrd	$⊢ (((φ \land f \in D) \land f \neq \underset{˙}{1}) \land (c \in [0, +∞) \land (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}))) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) \in 𝑂 (1)$
310	309	rexlimdvaa	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to (\exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) \in 𝑂 (1))$
311	310	exlimdv	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to (\exists t \exists c \in [0, +∞) (seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) ⇝ t \land \forall y \in [1, +∞) \|seq 1 (+ (a \in ℕ ⟼ \frac{f (L (a))}{a})) (⌊y⌋) - t\| \leq \frac{c}{y}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) \in 𝑂 (1))$
312	295 311	mpd	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) + if (f \in W, \log x, 0)) \in 𝑂 (1)$
313	290 312	eqeltrd	$⊢ ((φ \land f \in D) \land f \neq \underset{˙}{1}) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) \in 𝑂 (1)$
314	266 313	pm2.61dane	$⊢ (φ \land f \in D) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0))) \in 𝑂 (1)$
315	250 251 253 314	o1mul2	$⊢ (φ \land f \in D) \to (x \in ℝ^{+} ⟼ \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)))) \in 𝑂 (1)$
316	243 244 249 315	fsumo1	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{f \in D} \overline{f (A)} (\sum_{n = 1}^{⌊x⌋} f (L (n)) (\frac{Λ (n)}{n}) - \log x if (f = \underset{˙}{1}, 1, if (f \in W, - 1, 0)))) \in 𝑂 (1)$
317	241 316	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ ϕ (N) \sum_{n \in (1 \dots ⌊x⌋) \cap T} (\frac{Λ (n)}{n}) - \log x (1 - \|W\|)) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem rpvmasum2

Proof