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		fzfid	$$⊢k\in \mathbb{N}\to \left(1\dots k\right)\in \mathrm{Fin}$$
2		dvdsssfz1	$$⊢k\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel k\right\}\subseteq \left(1\dots k\right)$$
3	1 2	ssfid	$$⊢k\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel k\right\}\in \mathrm{Fin}$$
4		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel k\right\}\subseteq \mathbb{N}$$
5		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\}$$
6	4 5	sselid	$$⊢\left(k\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel k\right\}\right)\to d\in \mathbb{N}$$
7		vmacl	$$⊢d\in \mathbb{N}\to \Lambda \left(d\right)\in ℝ$$
8	6 7	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 ℝ$$
9		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\}$$
10	4 9	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}$$
11		vmacl	$$⊢\frac{k}{d}\in \mathbb{N}\to \Lambda \left(\frac{k}{d}\right)\in ℝ$$
12	10 11	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 ℝ$$
13	8 12	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 ℝ$$
14	3 13	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 ℝ$$
15		vmacl	$$⊢k\in \mathbb{N}\to \Lambda \left(k\right)\in ℝ$$
16		nnrp	$$⊢k\in \mathbb{N}\to k\in {ℝ}^{+}$$
17	16	relogcld	$$⊢k\in \mathbb{N}\to \log k\in ℝ$$
18	15 17	remulcld	$$⊢k\in \mathbb{N}\to \Lambda \left(k\right)\log k\in ℝ$$
19	14 18	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 ℝ$$
20	19	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 ℂ$$
21	20	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 ℂ$$
22	21	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}⟶ℂ$$
23		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel n\right\}\subseteq \mathbb{N}$$
24		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\}$$
25	23 24	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}$$
26		breq2	$$⊢k=m\to \left(x\parallel k\leftrightarrow x\parallel m\right)$$
27	26	rabbidv	$$⊢k=m\to \left\{x\in \mathbb{N}|x\parallel k\right\}=\left\{x\in \mathbb{N}|x\parallel m\right\}$$
28		fvoveq1	$$⊢k=m\to \Lambda \left(\frac{k}{d}\right)=\Lambda \left(\frac{m}{d}\right)$$
29	28	oveq2d	$$⊢k=m\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{m}{d}\right)$$
30	29	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)$$
31	27 30	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)$$
32		fveq2	$$⊢k=m\to \Lambda \left(k\right)=\Lambda \left(m\right)$$
33		fveq2	$$⊢k=m\to \log k=\log m$$
34	32 33	oveq12d	$$⊢k=m\to \Lambda \left(k\right)\log k=\Lambda \left(m\right)\log m$$
35	31 34	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$$
36		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)$$
37		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}$$
38	35 36 37	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$$
39	25 38	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$$
40	39	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)$$
41		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$$
42	41	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$$
43	40 42	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)$$
44	43	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)$$
45	22 44	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)$$
46	45	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)$$
47		breq2	$$⊢k=N\to \left(x\parallel k\leftrightarrow x\parallel N\right)$$
48	47	rabbidv	$$⊢k=N\to \left\{x\in \mathbb{N}|x\parallel k\right\}=\left\{x\in \mathbb{N}|x\parallel N\right\}$$
49		fvoveq1	$$⊢k=N\to \Lambda \left(\frac{k}{d}\right)=\Lambda \left(\frac{N}{d}\right)$$
50	49	oveq2d	$$⊢k=N\to \Lambda \left(d\right)\Lambda \left(\frac{k}{d}\right)=\Lambda \left(d\right)\Lambda \left(\frac{N}{d}\right)$$
51	50	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)$$
52	48 51	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)$$
53		fveq2	$$⊢k=N\to \Lambda \left(k\right)=\Lambda \left(N\right)$$
54		fveq2	$$⊢k=N\to \log k=\log N$$
55	53 54	oveq12d	$$⊢k=N\to \Lambda \left(k\right)\log k=\Lambda \left(N\right)\log N$$
56	52 55	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$$
57	56 36 37	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$$
58		fveq2	$$⊢j=d\to \mu \left(j\right)=\mu \left(d\right)$$
59		oveq2	$$⊢j=d\to \frac{i}{j}=\frac{i}{d}$$
60	59	fveq2d	$$⊢j=d\to \log \left(\frac{i}{j}\right)=\log \left(\frac{i}{d}\right)$$
61	60	oveq1d	$$⊢j=d\to {\log \left(\frac{i}{j}\right)}^2={\log \left(\frac{i}{d}\right)}^2$$
62	58 61	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$$
63	62	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$$
64		breq2	$$⊢i=N\to \left(x\parallel i\leftrightarrow x\parallel N\right)$$
65	64	rabbidv	$$⊢i=N\to \left\{x\in \mathbb{N}|x\parallel i\right\}=\left\{x\in \mathbb{N}|x\parallel N\right\}$$
66		fvoveq1	$$⊢i=N\to \log \left(\frac{i}{d}\right)=\log \left(\frac{N}{d}\right)$$
67	66	oveq1d	$$⊢i=N\to {\log \left(\frac{i}{d}\right)}^2={\log \left(\frac{N}{d}\right)}^2$$
68	67	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$$
69	68	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$$
70	65 69	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$$
71	63 70	syl5eq	$$⊢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$$
72		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel i\right\}\subseteq \mathbb{N}$$
73		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\}$$
74	72 73	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}$$
75		fveq2	$$⊢n=\frac{i}{j}\to \log n=\log \left(\frac{i}{j}\right)$$
76	75	oveq1d	$$⊢n=\frac{i}{j}\to {\log n}^2={\log \left(\frac{i}{j}\right)}^2$$
77		eqid	$$⊢\left(n\in \mathbb{N}⟼{\log n}^2\right)=\left(n\in \mathbb{N}⟼{\log n}^2\right)$$
78		ovex	$$⊢{\log n}^2\in \mathrm{V}$$
79	76 77 78	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$$
80	74 79	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$$
81	80	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$$
82	81	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$$
83	82	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)$$
84		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}$$
85	71 83 84	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$$
86	46 57 85	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$$