Theorem logsqvma2

Description: The Möbius inverse of logsqvma . Equation 10.4.8 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

	Ref	Expression
Assertion	logsqvma2	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)+\Lambda \left(N\right)\log N$$

Proof

Step	Hyp	Ref	Expression
1		dvdsfi	$$⊢k\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel k\right\}\in \mathrm{Fin}$$
2		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel k\right\}\subseteq \mathbb{N}$$
3		simpr	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to d\in \left\{x\in \mathbb{N}|x\parallel k\right\}$$
4	2 3	sselid	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to d\in \mathbb{N}$$
5		vmacl	$$⊢d\in \mathbb{N}\to \Lambda \left(d\right)\in ℝ$$
6	4 5	syl	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \Lambda \left(d\right)\in ℝ$$
7		dvdsdivcl	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \frac{k}{d}\in \left\{x\in \mathbb{N}|x\parallel k\right\}$$
8	2 7	sselid	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \frac{k}{d}\in \mathbb{N}$$
9		vmacl	$$⊢\frac{k}{d}\in \mathbb{N}\to \Lambda \left(\frac{k}{d}\right)\in ℝ$$
10	8 9	syl	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \Lambda \left(\frac{k}{d}\right)\in ℝ$$
11	6 10	remulcld	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)\in ℝ$$
12	1 11	fsumrecl	$$⊢k\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)\in ℝ$$
13		vmacl	$$⊢k\in \mathbb{N}\to \Lambda \left(k\right)\in ℝ$$
14		nnrp	$$⊢k\in \mathbb{N}\to k\in {ℝ}^{+}$$
15	14	relogcld	$$⊢k\in \mathbb{N}\to \log k\in ℝ$$
16	13 15	remulcld	$$⊢k\in \mathbb{N}\to \Lambda \left(k\right)\log k\in ℝ$$
17	12 16	readdcld	$$⊢k\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\in ℝ$$
18	17	recnd	$$⊢k\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\in ℂ$$
19	18	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \mathbb{N}\right)\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\in ℂ$$
20	19	fmpttd	$$⊢N\in \mathbb{N}\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right):\mathbb{N}⟶ℂ$$
21		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel n\right\}\subseteq \mathbb{N}$$
22		simpr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel n\right\}\right)\to m\in \left\{x\in \mathbb{N}|x\parallel n\right\}$$
23	21 22	sselid	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel n\right\}\right)\to m\in \mathbb{N}$$
24		breq2	$$⊢k=m\to \left(x\parallel k\leftrightarrow x\parallel m\right)$$
25	24	rabbidv	$$⊢k=m\to \left\{x\in \mathbb{N}|x\parallel k\right\}=\left\{x\in \mathbb{N}|x\parallel m\right\}$$
26		fvoveq1	$$⊢k=m\to \Lambda \left(\frac{k}{d}\right)=\Lambda \left(\frac{m}{d}\right)$$
27	26	oveq2d	$$⊢k=m\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)$$
28	27	adantr	$$⊢\left(k=m\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)$$
29	25 28	sumeq12dv	$$⊢k=m\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)$$
30		fveq2	$$⊢k=m\to \Lambda \left(k\right)=\Lambda \left(m\right)$$
31		fveq2	$$⊢k=m\to \log k=\log m$$
32	30 31	oveq12d	$$⊢k=m\to \Lambda \left(k\right)\log k=\Lambda \left(m\right)\log m$$
33	29 32	oveq12d	$$⊢k=m\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m$$
34		eqid	$$⊢\left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)=\left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)$$
35		ovex	$$⊢\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\in \mathrm{V}$$
36	33 34 35	fvmpt3i	$$⊢m\in \mathbb{N}\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(m\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m$$
37	23 36	syl	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel n\right\}\right)\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(m\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m$$
38	37	sumeq2dv	$$⊢\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\to \sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(m\right)=\sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m\right)$$
39		logsqvma	$$⊢n\in \mathbb{N}\to \sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m\right)={\log n}^2$$
40	39	adantl	$$⊢\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\to \sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(\sum _{d\in \left\{x\in \mathbb{N}|x\parallel m\right\}}\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)+\Lambda \left(m\right)\log m\right)={\log n}^2$$
41	38 40	eqtr2d	$$⊢\left(N\in \mathbb{N}\wedge n\in \mathbb{N}\right)\to {\log n}^2=\sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(m\right)$$
42	41	mpteq2dva	$$⊢N\in \mathbb{N}\to \left(n\in \mathbb{N}⟼{\log n}^2\right)=\left(n\in \mathbb{N}⟼\sum _{m\in \left\{x\in \mathbb{N}|x\parallel n\right\}}\left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(m\right)\right)$$
43	20 42	muinv	$$⊢N\in \mathbb{N}\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)=\left(i\in \mathbb{N}⟼\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)\right)$$
44	43	fveq1d	$$⊢N\in \mathbb{N}\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(N\right)=\left(i\in \mathbb{N}⟼\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)\right)\left(N\right)$$
45		breq2	$$⊢k=N\to \left(x\parallel k\leftrightarrow x\parallel N\right)$$
46	45	rabbidv	$$⊢k=N\to \left\{x\in \mathbb{N}|x\parallel k\right\}=\left\{x\in \mathbb{N}|x\parallel N\right\}$$
47		fvoveq1	$$⊢k=N\to \Lambda \left(\frac{k}{d}\right)=\Lambda \left(\frac{N}{d}\right)$$
48	47	oveq2d	$$⊢k=N\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)$$
49	48	adantr	$$⊢\left(k=N\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)$$
50	46 49	sumeq12dv	$$⊢k=N\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)$$
51		fveq2	$$⊢k=N\to \Lambda \left(k\right)=\Lambda \left(N\right)$$
52		fveq2	$$⊢k=N\to \log k=\log N$$
53	51 52	oveq12d	$$⊢k=N\to \Lambda \left(k\right)\log k=\Lambda \left(N\right)\log N$$
54	50 53	oveq12d	$$⊢k=N\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)+\Lambda \left(N\right)\log N$$
55	54 34 35	fvmpt3i	$$⊢N\in \mathbb{N}\to \left(k\in \mathbb{N}⟼\sum _{d\in \left\{x\in \mathbb{N}|x\parallel k\right\}}\Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)+\Lambda \left(k\right)\log k\right)\left(N\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)+\Lambda \left(N\right)\log N$$
56		fveq2	$$⊢j=d\to \mu \left(j\right)=\mu \left(d\right)$$
57		oveq2	$$⊢j=d\to \frac{i}{j}=\frac{i}{d}$$
58	57	fveq2d	$$⊢j=d\to \log \left(\frac{i}{j}\right)=\log \left(\frac{i}{d}\right)$$
59	58	oveq1d	$$⊢j=d\to {\log \left(\frac{i}{j}\right)}^2={\log \left(\frac{i}{d}\right)}^2$$
60	56 59	oveq12d	$$⊢j=d\to \mu \left(j\right){\log \left(\frac{i}{j}\right)}^2=\mu \left(d\right){\log \left(\frac{i}{d}\right)}^2$$
61	60	cbvsumv	$$⊢\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(d\right){\log \left(\frac{i}{d}\right)}^2$$
62		breq2	$$⊢i=N\to \left(x\parallel i\leftrightarrow x\parallel N\right)$$
63	62	rabbidv	$$⊢i=N\to \left\{x\in \mathbb{N}|x\parallel i\right\}=\left\{x\in \mathbb{N}|x\parallel N\right\}$$
64		fvoveq1	$$⊢i=N\to \log \left(\frac{i}{d}\right)=\log \left(\frac{N}{d}\right)$$
65	64	oveq1d	$$⊢i=N\to {\log \left(\frac{i}{d}\right)}^2={\log \left(\frac{N}{d}\right)}^2$$
66	65	oveq2d	$$⊢i=N\to \mu \left(d\right){\log \left(\frac{i}{d}\right)}^2=\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2$$
67	66	adantr	$$⊢\left(i=N\wedge d\in \left\{x\in \mathbb{N}|x\parallel i\right\}\right)\to \mu \left(d\right){\log \left(\frac{i}{d}\right)}^2=\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2$$
68	63 67	sumeq12dv	$$⊢i=N\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(d\right){\log \left(\frac{i}{d}\right)}^2=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2$$
69	61 68	eqtrid	$$⊢i=N\to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2$$
70		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel i\right\}\subseteq \mathbb{N}$$
71		dvdsdivcl	$$⊢\left(i\in \mathbb{N}\wedge j\in \left\{x\in \mathbb{N}|x\parallel i\right\}\right)\to \frac{i}{j}\in \left\{x\in \mathbb{N}|x\parallel i\right\}$$
72	70 71	sselid	$$⊢\left(i\in \mathbb{N}\wedge j\in \left\{x\in \mathbb{N}|x\parallel i\right\}\right)\to \frac{i}{j}\in \mathbb{N}$$
73		fveq2	$$⊢n=\frac{i}{j}\to \log n=\log \left(\frac{i}{j}\right)$$
74	73	oveq1d	$$⊢n=\frac{i}{j}\to {\log n}^2={\log \left(\frac{i}{j}\right)}^2$$
75		eqid	$$⊢\left(n\in \mathbb{N}⟼{\log n}^2\right)=\left(n\in \mathbb{N}⟼{\log n}^2\right)$$
76		ovex	$$⊢{\log n}^2\in \mathrm{V}$$
77	74 75 76	fvmpt3i	$$⊢\frac{i}{j}\in \mathbb{N}\to \left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)={\log \left(\frac{i}{j}\right)}^2$$
78	72 77	syl	$$⊢\left(i\in \mathbb{N}\wedge j\in \left\{x\in \mathbb{N}|x\parallel i\right\}\right)\to \left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)={\log \left(\frac{i}{j}\right)}^2$$
79	78	oveq2d	$$⊢\left(i\in \mathbb{N}\wedge j\in \left\{x\in \mathbb{N}|x\parallel i\right\}\right)\to \mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)=\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2$$
80	79	sumeq2dv	$$⊢i\in \mathbb{N}\to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)=\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2$$
81	80	mpteq2ia	$$⊢\left(i\in \mathbb{N}⟼\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)\right)=\left(i\in \mathbb{N}⟼\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2\right)$$
82		sumex	$$⊢\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right){\log \left(\frac{i}{j}\right)}^2\in \mathrm{V}$$
83	69 81 82	fvmpt3i	$$⊢N\in \mathbb{N}\to \left(i\in \mathbb{N}⟼\sum _{j\in \left\{x\in \mathbb{N}|x\parallel i\right\}}\mu \left(j\right)\left(n\in \mathbb{N}⟼{\log n}^2\right)\left(\frac{i}{j}\right)\right)\left(N\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2$$
84	44 55 83	3eqtr3rd	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\mu \left(d\right){\log \left(\frac{N}{d}\right)}^2=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)+\Lambda \left(N\right)\log N$$