dchrvmasum2lem

Description: Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n ) Lam ( n ) / n ) given in dchrvmasumlem1 . Part of Lemma 9.4.3 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-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 ℝ^{+}$
	dchrvmasum2.2	$⊢ φ \to 1 \leq A$
Assertion	dchrvmasum2lem	$⊢ φ \to \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{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		dchrvmasum2.2	$⊢ φ \to 1 \leq A$
11		2fveq3	$⊢ n = d m \to X (L (n)) = X (L (d m))$
12		id	$⊢ n = d m \to n = d m$
13	11 12	oveq12d	$⊢ n = d m \to \frac{X (L (n))}{n} = \frac{X (L (d m))}{d m}$
14		oveq2	$⊢ n = d m \to \frac{A}{n} = \frac{A}{d m}$
15	14	fveq2d	$⊢ n = d m \to \log (\frac{A}{n}) = \log (\frac{A}{d m})$
16	13 15	oveq12d	$⊢ n = d m \to (\frac{X (L (n))}{n}) \log (\frac{A}{n}) = (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
17	16	oveq2d	$⊢ n = d m \to μ (d) (\frac{X (L (n))}{n}) \log (\frac{A}{n}) = μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
18	9	rpred	$⊢ φ \to A \in ℝ$
19		elrabi	$⊢ d \in \{x \in ℕ \| x ∥ n\} \to d \in ℕ$
20	19	ad2antll	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to d \in ℕ$
21		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
22	20 21	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) \in ℤ$
23	22	zcnd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) \in ℂ$
24	7	adantr	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X \in D$
25		elfzelz	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℤ$
26	25	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℤ$
27	4 1 5 2 24 26	dchrzrhcl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to X (L (n)) \in ℂ$
28		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
29	28	adantl	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
30	29	nncnd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \in ℂ$
31	29	nnne0d	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to n \neq 0$
32	27 30 31	divcld	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{X (L (n))}{n} \in ℂ$
33	28	nnrpd	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℝ^{+}$
34		rpdivcl	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{A}{n} \in ℝ^{+}$
35	9 33 34	syl2an	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \frac{A}{n} \in ℝ^{+}$
36	35	relogcld	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \log (\frac{A}{n}) \in ℝ$
37	36	recnd	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to \log (\frac{A}{n}) \in ℂ$
38	32 37	mulcld	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to (\frac{X (L (n))}{n}) \log (\frac{A}{n}) \in ℂ$
39	38	adantrr	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to (\frac{X (L (n))}{n}) \log (\frac{A}{n}) \in ℂ$
40	23 39	mulcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land d \in \{x \in ℕ \| x ∥ n\})) \to μ (d) (\frac{X (L (n))}{n}) \log (\frac{A}{n}) \in ℂ$
41	17 18 40	dvdsflsumcom	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (\frac{X (L (n))}{n}) \log (\frac{A}{n}) = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
42		2fveq3	$⊢ n = 1 \to X (L (n)) = X (L (1))$
43		id	$⊢ n = 1 \to n = 1$
44	42 43	oveq12d	$⊢ n = 1 \to \frac{X (L (n))}{n} = \frac{X (L (1))}{1}$
45		oveq2	$⊢ n = 1 \to \frac{A}{n} = \frac{A}{1}$
46	45	fveq2d	$⊢ n = 1 \to \log (\frac{A}{n}) = \log (\frac{A}{1})$
47	44 46	oveq12d	$⊢ n = 1 \to (\frac{X (L (n))}{n}) \log (\frac{A}{n}) = (\frac{X (L (1))}{1}) \log (\frac{A}{1})$
48		fzfid	$⊢ φ \to (1 \dots ⌊A⌋) \in Fin$
49		fz1ssnn	$⊢ (1 \dots ⌊A⌋) \subseteq ℕ$
50	49	a1i	$⊢ φ \to (1 \dots ⌊A⌋) \subseteq ℕ$
51		flge1nn	$⊢ (A \in ℝ \land 1 \leq A) \to ⌊A⌋ \in ℕ$
52	18 10 51	syl2anc	$⊢ φ \to ⌊A⌋ \in ℕ$
53		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
54	52 53	eleqtrdi	$⊢ φ \to ⌊A⌋ \in ℤ_{\geq 1}$
55		eluzfz1	$⊢ ⌊A⌋ \in ℤ_{\geq 1} \to 1 \in (1 \dots ⌊A⌋)$
56	54 55	syl	$⊢ φ \to 1 \in (1 \dots ⌊A⌋)$
57	47 48 50 56 38	musumsum	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (\frac{X (L (n))}{n}) \log (\frac{A}{n}) = (\frac{X (L (1))}{1}) \log (\frac{A}{1})$
58	4 1 5 2 7	dchrzrh1	$⊢ φ \to X (L (1)) = 1$
59	58	oveq1d	$⊢ φ \to \frac{X (L (1))}{1} = \frac{1}{1}$
60		1div1e1	$⊢ \frac{1}{1} = 1$
61	59 60	eqtrdi	$⊢ φ \to \frac{X (L (1))}{1} = 1$
62	9	rpcnd	$⊢ φ \to A \in ℂ$
63	62	div1d	$⊢ φ \to \frac{A}{1} = A$
64	63	fveq2d	$⊢ φ \to \log (\frac{A}{1}) = \log A$
65	61 64	oveq12d	$⊢ φ \to (\frac{X (L (1))}{1}) \log (\frac{A}{1}) = 1 \log A$
66	9	relogcld	$⊢ φ \to \log A \in ℝ$
67	66	recnd	$⊢ φ \to \log A \in ℂ$
68	67	mulid2d	$⊢ φ \to 1 \log A = \log A$
69	57 65 68	3eqtrrd	$⊢ φ \to \log A = \sum_{n = 1}^{⌊A⌋} \sum_{d \in \{x \in ℕ \| x ∥ n\}} μ (d) (\frac{X (L (n))}{n}) \log (\frac{A}{n})$
70		fzfid	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{d}⌋) \in Fin$
71	7	adantr	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X \in D$
72		elfzelz	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℤ$
73	72	adantl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℤ$
74	4 1 5 2 71 73	dchrzrhcl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) \in ℂ$
75		fznnfl	$⊢ A \in ℝ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
76	18 75	syl	$⊢ φ \to (d \in (1 \dots ⌊A⌋) \leftrightarrow (d \in ℕ \land d \leq A))$
77	76	simprbda	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℕ$
78	77 21	syl	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to μ (d) \in ℤ$
79	78	zred	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to μ (d) \in ℝ$
80	79 77	nndivred	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℝ$
81	80	recnd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{μ (d)}{d} \in ℂ$
82	74 81	mulcld	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
83	7	ad2antrr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X \in D$
84		elfzelz	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℤ$
85	84	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℤ$
86	4 1 5 2 83 85	dchrzrhcl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) \in ℂ$
87		elfznn	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℕ$
88	87	nnrpd	$⊢ d \in (1 \dots ⌊A⌋) \to d \in ℝ^{+}$
89		rpdivcl	$⊢ (A \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{A}{d} \in ℝ^{+}$
90	9 88 89	syl2an	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to \frac{A}{d} \in ℝ^{+}$
91		elfznn	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℕ$
92	91	nnrpd	$⊢ m \in (1 \dots ⌊\frac{A}{d}⌋) \to m \in ℝ^{+}$
93		rpdivcl	$⊢ (\frac{A}{d} \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{\frac{A}{d}}{m} \in ℝ^{+}$
94	90 92 93	syl2an	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\frac{A}{d}}{m} \in ℝ^{+}$
95	94	relogcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{\frac{A}{d}}{m}) \in ℝ$
96	91	adantl	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℕ$
97	95 96	nndivred	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{\frac{A}{d}}{m})}{m} \in ℝ$
98	97	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\log (\frac{\frac{A}{d}}{m})}{m} \in ℂ$
99	86 98	mulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) \in ℂ$
100	70 82 99	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 (\frac{\frac{A}{d}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (d)) (\frac{μ (d)}{d}) X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$
101	74	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d)) \in ℂ$
102	79	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) \in ℝ$
103	102	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) \in ℂ$
104	77	nnrpd	$⊢ (φ \land d \in (1 \dots ⌊A⌋)) \to d \in ℝ^{+}$
105	104	adantr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℝ^{+}$
106	105	rpcnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (d \in ℂ \land d \neq 0)$
107		div12	$⊢ (X (L (d)) \in ℂ \land μ (d) \in ℂ \land (d \in ℂ \land d \neq 0)) \to X (L (d)) (\frac{μ (d)}{d}) = μ (d) (\frac{X (L (d))}{d})$
108	101 103 106 107	syl3anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (d)) (\frac{μ (d)}{d}) = μ (d) (\frac{X (L (d))}{d})$
109	95	recnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{\frac{A}{d}}{m}) \in ℂ$
110	96	nnrpd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℝ^{+}$
111	110	rpcnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (m \in ℂ \land m \neq 0)$
112		div12	$⊢ (X (L (m)) \in ℂ \land \log (\frac{\frac{A}{d}}{m}) \in ℂ \land (m \in ℂ \land m \neq 0)) \to X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) = \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (m))}{m})$
113	86 109 111 112	syl3anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) = \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (m))}{m})$
114	108 113	oveq12d	$⊢ ((φ \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 (\frac{\frac{A}{d}}{m})}{m}) = μ (d) (\frac{X (L (d))}{d}) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (m))}{m})$
115	105	rpcnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℂ$
116	105	rpne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \neq 0$
117	101 115 116	divcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{X (L (d))}{d} \in ℂ$
118	96	nncnd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \in ℂ$
119	96	nnne0d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to m \neq 0$
120	86 118 119	divcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{X (L (m))}{m} \in ℂ$
121	117 120	mulcld	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) \in ℂ$
122	103 109 121	mulassd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = μ (d) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
123	103 117 109 120	mul4d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) (\frac{X (L (d))}{d}) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (m))}{m}) = μ (d) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
124	72	ad2antlr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to d \in ℤ$
125	4 1 5 2 83 124 85	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))$
126	125	oveq1d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{X (L (d m))}{d m} = \frac{X (L (d)) X (L (m))}{d m}$
127		divmuldiv	$⊢ ((X (L (d)) \in ℂ \land X (L (m)) \in ℂ) \land ((d \in ℂ \land d \neq 0) \land (m \in ℂ \land m \neq 0))) \to (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = \frac{X (L (d)) X (L (m))}{d m}$
128	101 86 106 111 127	syl22anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = \frac{X (L (d)) X (L (m))}{d m}$
129	126 128	eqtr4d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{X (L (d m))}{d m} = (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
130	62	ad2antrr	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to A \in ℂ$
131		divdiv1	$⊢ (A \in ℂ \land (d \in ℂ \land d \neq 0) \land (m \in ℂ \land m \neq 0)) \to \frac{\frac{A}{d}}{m} = \frac{A}{d m}$
132	130 106 111 131	syl3anc	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{\frac{A}{d}}{m} = \frac{A}{d m}$
133	132	eqcomd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \frac{A}{d m} = \frac{\frac{A}{d}}{m}$
134	133	fveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to \log (\frac{A}{d m}) = \log (\frac{\frac{A}{d}}{m})$
135	129 134	oveq12d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m}) = (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) \log (\frac{\frac{A}{d}}{m})$
136	121 109	mulcomd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) \log (\frac{\frac{A}{d}}{m}) = \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
137	135 136	eqtrd	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m}) = \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
138	137	oveq2d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m}) = μ (d) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
139	122 123 138	3eqtr4d	$⊢ ((φ \land d \in (1 \dots ⌊A⌋)) \land m \in (1 \dots ⌊\frac{A}{d}⌋)) \to μ (d) (\frac{X (L (d))}{d}) \log (\frac{\frac{A}{d}}{m}) (\frac{X (L (m))}{m}) = μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
140	114 139	eqtrd	$⊢ ((φ \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 (\frac{\frac{A}{d}}{m})}{m}) = μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
141	140	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 (\frac{\frac{A}{d}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
142	100 141	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 (\frac{\frac{A}{d}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{A}{d}⌋} μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
143	142	sumeq2dv	$⊢ φ \to \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m}) = \sum_{d = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{d}⌋} μ (d) (\frac{X (L (d m))}{d m}) \log (\frac{A}{d m})$
144	41 69 143	3eqtr4d	$⊢ φ \to \log A = \sum_{d = 1}^{⌊A⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{A}{d}⌋} X (L (m)) (\frac{\log (\frac{\frac{A}{d}}{m})}{m})$

Metamath Proof Explorer

Theorem dchrvmasum2lem

Proof