dchrvmasumlem1

Description: An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of Shapiro, p. 377. (Contributed by Mario Carneiro, 3-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}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrvmasum.a	$⊢ φ \to A \in ℝ^{+}$
Assertion	dchrvmasumlem1	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$

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		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrvmasum.a	$⊢ φ \to A \in ℝ^{+}$
10		2fveq3	$⊢ n = d m \to X (L (n)) = X (L (d m))$
11		oveq2	$⊢ n = d m \to \frac{μ (d)}{n} = \frac{μ (d)}{d m}$
12		fvoveq1	$⊢ n = d m \to \log (\frac{n}{d}) = \log (\frac{d m}{d})$
13	11 12	oveq12d	$⊢ n = d m \to (\frac{μ (d)}{n}) \log (\frac{n}{d}) = (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
14	10 13	oveq12d	$⊢ n = d m \to X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d}) = X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
15	9	rpred	$⊢ φ \to A \in ℝ$
16	7	adantr	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X \in D$
17		elfzelz	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℤ$
18	17	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℤ$
19	4 1 5 2 16 18	dchrzrhcl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) \in ℂ$
20	19	adantrr	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to X (L (n)) \in ℂ$
21		elrabi	$⊢ d \in \{x \in ℕ \| x ∥ n\} \to d \in ℕ$
22	21	ad2antll	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to d \in ℕ$
23		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
24	22 23	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) \in ℤ$
25	24	zred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) \in ℝ$
26		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
27	26	ad2antrl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to n \in ℕ$
28	25 27	nndivred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to \frac{μ (d)}{n} \in ℝ$
29	28	recnd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to \frac{μ (d)}{n} \in ℂ$
30	27	nnrpd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to n \in ℝ^{+}$
31	22	nnrpd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to d \in ℝ^{+}$
32	30 31	rpdivcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to \frac{n}{d} \in ℝ^{+}$
33	32	relogcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to \log (\frac{n}{d}) \in ℝ$
34	33	recnd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to \log (\frac{n}{d}) \in ℂ$
35	29 34	mulcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to (\frac{μ (d)}{n}) \log (\frac{n}{d}) \in ℂ$
36	20 35	mulcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d}) \in ℂ$
37	14 15 36	dvdsflsumcom	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d}) = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
38		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
39	38	a1i	$⊢ φ \to Λ : ℕ ⟶ ℝ$
40		ax-resscn	$⊢ ℝ \subseteq ℂ$
41		fss	$⊢ (Λ : ℕ ⟶ ℝ \land ℝ \subseteq ℂ) \to Λ : ℕ ⟶ ℂ$
42	39 40 41	sylancl	$⊢ φ \to Λ : ℕ ⟶ ℂ$
43		vmasum	$⊢ m \in ℕ \to \sum_{i \in \{x \in ℕ \| x ∥ m\}} Λ (i) = \log m$
44	43	adantl	$⊢ (φ \land m \in ℕ) \to \sum_{i \in \{x \in ℕ \| x ∥ m\}} Λ (i) = \log m$
45	44	eqcomd	$⊢ (φ \land m \in ℕ) \to \log m = \sum_{i \in \{x \in ℕ \| x ∥ m\}} Λ (i)$
46	45	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ \log m) = (m \in ℕ ⟼ \sum_{i \in \{x \in ℕ \| x ∥ m\}} Λ (i))$
47	42 46	muinv	$⊢ φ \to Λ = (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}))$
48	47	fveq1d	$⊢ φ \to Λ (n) = (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})) (n)$
49		sumex	$⊢ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}) \in V$
50		eqid	$⊢ (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})) = (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}))$
51	50	fvmpt2	$⊢ (n \in ℕ \land \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}) \in V) \to (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})) (n) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})$
52	26 49 51	sylancl	$⊢ n \in (1 \dots ⌊A⌋) \to (n \in ℕ ⟼ \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})) (n) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})$
53	48 52	sylan9eq	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d})$
54		breq1	$⊢ x = d \to (x ∥ n \leftrightarrow d ∥ n)$
55	54	elrab	$⊢ d \in \{x \in ℕ \| x ∥ n\} \leftrightarrow (d \in ℕ \land d ∥ n)$
56	55	simprbi	$⊢ d \in \{x \in ℕ \| x ∥ n\} \to d ∥ n$
57	56	adantl	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to d ∥ n$
58	26	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
59		nndivdvds	$⊢ (n \in ℕ \land d \in ℕ) \to (d ∥ n \leftrightarrow \frac{n}{d} \in ℕ)$
60	58 21 59	syl2an	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to (d ∥ n \leftrightarrow \frac{n}{d} \in ℕ)$
61	57 60	mpbid	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to \frac{n}{d} \in ℕ$
62		fveq2	$⊢ m = \frac{n}{d} \to \log m = \log (\frac{n}{d})$
63		eqid	$⊢ (m \in ℕ ⟼ \log m) = (m \in ℕ ⟼ \log m)$
64		fvex	$⊢ \log (\frac{n}{d}) \in V$
65	62 63 64	fvmpt	$⊢ \frac{n}{d} \in ℕ \to (m \in ℕ ⟼ \log m) (\frac{n}{d}) = \log (\frac{n}{d})$
66	61 65	syl	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to (m \in ℕ ⟼ \log m) (\frac{n}{d}) = \log (\frac{n}{d})$
67	66	oveq2d	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}) = μ (d) \log (\frac{n}{d})$
68	67	sumeq2dv	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (m \in ℕ ⟼ \log m) (\frac{n}{d}) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) \log (\frac{n}{d})$
69	53 68	eqtrd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) \log (\frac{n}{d})$
70	69	oveq1d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{Λ (n)}{n} = \frac{\sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) \log (\frac{n}{d})}{n}$
71		fzfid	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to (1 \dots n) \in Fin$
72		dvdsssfz1	$⊢ n \in ℕ \to \{x \in ℕ \| x ∥ n\} \subseteq (1 \dots n)$
73	58 72	syl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \{x \in ℕ \| x ∥ n\} \subseteq (1 \dots n)$
74	71 73	ssfid	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \{x \in ℕ \| x ∥ n\} \in Fin$
75	58	nncnd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℂ$
76	24	zcnd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) \in ℂ$
77	76	anassrs	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to μ (d) \in ℂ$
78	34	anassrs	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to \log (\frac{n}{d}) \in ℂ$
79	77 78	mulcld	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to μ (d) \log (\frac{n}{d}) \in ℂ$
80	58	nnne0d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \neq 0$
81	74 75 79 80	fsumdivc	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{\sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) \log (\frac{n}{d})}{n} = \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d) \log (\frac{n}{d})}{n})$
82	21	adantl	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to d \in ℕ$
83	82 23	syl	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to μ (d) \in ℤ$
84	83	zcnd	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to μ (d) \in ℂ$
85	75	adantr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to n \in ℂ$
86	80	adantr	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to n \neq 0$
87	84 78 85 86	div23d	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to \frac{μ (d) \log (\frac{n}{d})}{n} = (\frac{μ (d)}{n}) \log (\frac{n}{d})$
88	87	sumeq2dv	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d) \log (\frac{n}{d})}{n}) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d)}{n}) \log (\frac{n}{d})$
89	70 81 88	3eqtrd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{Λ (n)}{n} = \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d)}{n}) \log (\frac{n}{d})$
90	89	oveq2d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) (\frac{Λ (n)}{n}) = X (L (n)) \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d)}{n}) \log (\frac{n}{d})$
91	35	anassrs	$⊢ ((φ \land n \in (1 \dots ⌊A⌋)) \land d \in \{x \in ℕ \| x ∥ n\}) \to (\frac{μ (d)}{n}) \log (\frac{n}{d}) \in ℂ$
92	74 19 91	fsummulc2	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) \sum_{d \in \{x \in ℕ \| x ∥ n\}} (\frac{μ (d)}{n}) \log (\frac{n}{d}) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d})$
93	90 92	eqtrd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) (\frac{Λ (n)}{n}) = \sum_{d \in \{x \in ℕ \| x ∥ n\}} X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d})$
94	93	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) = \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} X (L (n)) (\frac{μ (d)}{n}) \log (\frac{n}{d})$
95		fzfid	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{d}⌋) \in Fin$
96	7	adantr	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X \in D$
97		elfzelz	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℤ$
98	97	adantl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℤ$
99	4 1 5 2 96 98	dchrzrhcl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) \in ℂ$
100		fznnfl	$⊢ A \in ℝ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
101	15 100	syl	$⊢ φ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
102	101	simprbda	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℕ$
103	102 23	syl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to μ (d) \in ℤ$
104	103	zred	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to μ (d) \in ℝ$
105	104 102	nndivred	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℝ$
106	105	recnd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℂ$
107	99 106	mulcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
108	7	ad2antrr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X \in D$
109		elfzelz	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℤ$
110	109	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℤ$
111	4 1 5 2 108 110	dchrzrhcl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) \in ℂ$
112		elfznn	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℕ$
113	112	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℕ$
114	113	nnrpd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℝ^{+}$
115	114	relogcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m \in ℝ$
116	115 113	nndivred	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log m}{m} \in ℝ$
117	116	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log m}{m} \in ℂ$
118	111 117	mulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log m}{m}) \in ℂ$
119	95 107 118	fsummulc2	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d)) (\frac{μ (d)}{d}) X (L (m)) (\frac{\log m}{m})$
120	99	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d)) \in ℂ$
121	106	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{μ (d)}{d} \in ℂ$
122	120 121 111 117	mul4d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d)) (\frac{μ (d)}{d}) X (L (m)) (\frac{\log m}{m}) = X (L (d)) X (L (m)) (\frac{μ (d)}{d}) (\frac{\log m}{m})$
123	97	ad2antlr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℤ$
124	4 1 5 2 108 123 110	dchrzrhmul	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d m)) = X (L (d)) X (L (m))$
125	104	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) \in ℝ$
126	125	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) \in ℂ$
127	115	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log m \in ℂ$
128	102	nnrpd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℝ^{+}$
129	128	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℝ^{+}$
130	129 114	rpmulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d m \in ℝ^{+}$
131	130	rpcnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (d m \in ℂ \land d m \neq 0)$
132		div23	$⊢ (μ (d) \in ℂ \land \log m \in ℂ \land (d m \in ℂ \land d m \neq 0)) \to \frac{μ (d) \log m}{d m} = (\frac{μ (d)}{d m}) \log m$
133	126 127 131 132	syl3anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{μ (d) \log m}{d m} = (\frac{μ (d)}{d m}) \log m$
134	129	rpcnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (d \in ℂ \land d \neq 0)$
135	114	rpcnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (m \in ℂ \land m \neq 0)$
136		divmuldiv	$⊢ ((μ (d) \in ℂ \land \log m \in ℂ) \land ((d \in ℂ \land d \neq 0) \land (m \in ℂ \land m \neq 0))) \to (\frac{μ (d)}{d}) (\frac{\log m}{m}) = \frac{μ (d) \log m}{d m}$
137	126 127 134 135 136	syl22anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{μ (d)}{d}) (\frac{\log m}{m}) = \frac{μ (d) \log m}{d m}$
138	113	nncnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℂ$
139	129	rpcnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℂ$
140	129	rpne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \neq 0$
141	138 139 140	divcan3d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{d m}{d} = m$
142	141	fveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{d m}{d}) = \log m$
143	142	oveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{μ (d)}{d m}) \log (\frac{d m}{d}) = (\frac{μ (d)}{d m}) \log m$
144	133 137 143	3eqtr4rd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{μ (d)}{d m}) \log (\frac{d m}{d}) = (\frac{μ (d)}{d}) (\frac{\log m}{m})$
145	124 144	oveq12d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d}) = X (L (d)) X (L (m)) (\frac{μ (d)}{d}) (\frac{\log m}{m})$
146	122 145	eqtr4d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d)) (\frac{μ (d)}{d}) X (L (m)) (\frac{\log m}{m}) = X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
147	146	sumeq2dv	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d)) (\frac{μ (d)}{d}) X (L (m)) (\frac{\log m}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
148	119 147	eqtrd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
149	148	sumeq2dv	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m}) = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d m)) (\frac{μ (d)}{d m}) \log (\frac{d m}{d})$
150	37 94 149	3eqtr4d	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} X (L (n)) (\frac{Λ (n)}{n}) = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log m}{m})$

Metamath Proof Explorer

Theorem dchrvmasumlem1

Proof