Theorem logsqvma

Description: A formula for log ^ 2 ( N ) in terms of the primes. Equation 10.4.6 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢N\in \mathbb{N}\to \left(1\dots N\right)\in \mathrm{Fin}$$
2		dvdsssfz1	$$⊢N\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \left(1\dots N\right)$$
3	1 2	ssfid	$$⊢N\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel N\right\}\in \mathrm{Fin}$$
4		fzfid	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(1\dots d\right)\in \mathrm{Fin}$$
5		elrabi	$$⊢d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\to d\in \mathbb{N}$$
6	5	adantl	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to d\in \mathbb{N}$$
7		dvdsssfz1	$$⊢d\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel d\right\}\subseteq \left(1\dots d\right)$$
8	6 7	syl	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel d\right\}\subseteq \left(1\dots d\right)$$
9	4 8	ssfid	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel d\right\}\in \mathrm{Fin}$$
10		elrabi	$$⊢u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\to u\in \mathbb{N}$$
11	10	ad2antll	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to u\in \mathbb{N}$$
12		vmacl	$$⊢u\in \mathbb{N}\to \Lambda \left(u\right)\in ℝ$$
13	11 12	syl	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \Lambda \left(u\right)\in ℝ$$
14		breq1	$$⊢x=u\to \left(x\parallel d\leftrightarrow u\parallel d\right)$$
15	14	elrab	$$⊢u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\leftrightarrow \left(u\in \mathbb{N}\wedge u\parallel d\right)$$
16	15	simprbi	$$⊢u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\to u\parallel d$$
17	16	ad2antll	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to u\parallel d$$
18	5	ad2antrl	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to d\in \mathbb{N}$$
19		nndivdvds	$$⊢\left(d\in \mathbb{N}\wedge u\in \mathbb{N}\right)\to \left(u\parallel d\leftrightarrow \frac{d}{u}\in \mathbb{N}\right)$$
20	18 11 19	syl2anc	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \left(u\parallel d\leftrightarrow \frac{d}{u}\in \mathbb{N}\right)$$
21	17 20	mpbid	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \frac{d}{u}\in \mathbb{N}$$
22		vmacl	$$⊢\frac{d}{u}\in \mathbb{N}\to \Lambda \left(\frac{d}{u}\right)\in ℝ$$
23	21 22	syl	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \Lambda \left(\frac{d}{u}\right)\in ℝ$$
24	13 23	remulcld	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)\in ℝ$$
25	24	recnd	$$⊢\left(N\in \mathbb{N}\wedge \left(d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\right)\to \Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)\in ℂ$$
26	25	anassrs	$$⊢\left(\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge u\in \left\{x\in \mathbb{N}|x\parallel d\right\}\right)\to \Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)\in ℂ$$
27	9 26	fsumcl	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)\in ℂ$$
28		vmacl	$$⊢d\in \mathbb{N}\to \Lambda \left(d\right)\in ℝ$$
29	6 28	syl	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(d\right)\in ℝ$$
30	6	nnrpd	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to d\in {ℝ}^{+}$$
31	30	relogcld	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \log d\in ℝ$$
32	29 31	remulcld	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(d\right)\log d\in ℝ$$
33	32	recnd	$$⊢\left(N\in \mathbb{N}\wedge d\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(d\right)\log d\in ℂ$$
34	3 27 33	fsumadd	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\left(\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)+\Lambda \left(d\right)\log d\right)=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)+\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
35		id	$$⊢N\in \mathbb{N}\to N\in \mathbb{N}$$
36		fvoveq1	$$⊢d=uk\to \Lambda \left(\frac{d}{u}\right)=\Lambda \left(\frac{uk}{u}\right)$$
37	36	oveq2d	$$⊢d=uk\to \Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)=\Lambda \left(u\right)\Lambda \left(\frac{uk}{u}\right)$$
38	35 37 25	fsumdvdscom	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)=\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(u\right)\Lambda \left(\frac{uk}{u}\right)$$
39		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\subseteq \mathbb{N}$$
40		simpr	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}$$
41	39 40	sselid	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to k\in \mathbb{N}$$
42	41	nncnd	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to k\in ℂ$$
43		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \mathbb{N}$$
44		simpr	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
45	43 44	sselid	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in \mathbb{N}$$
46	45	nncnd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in ℂ$$
47	46	adantr	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to u\in ℂ$$
48	45	nnne0d	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\ne 0$$
49	48	adantr	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to u\ne 0$$
50	42 47 49	divcan3d	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to \frac{uk}{u}=k$$
51	50	fveq2d	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to \Lambda \left(\frac{uk}{u}\right)=\Lambda \left(k\right)$$
52	51	sumeq2dv	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(\frac{uk}{u}\right)=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(k\right)$$
53		dvdsdivcl	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{u}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
54	43 53	sselid	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{u}\in \mathbb{N}$$
55		vmasum	$$⊢\frac{N}{u}\in \mathbb{N}\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(k\right)=\log \left(\frac{N}{u}\right)$$
56	54 55	syl	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(k\right)=\log \left(\frac{N}{u}\right)$$
57		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
58	57	adantr	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to N\in {ℝ}^{+}$$
59	45	nnrpd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in {ℝ}^{+}$$
60	58 59	relogdivd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \log \left(\frac{N}{u}\right)=\log N-\log u$$
61	52 56 60	3eqtrd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(\frac{uk}{u}\right)=\log N-\log u$$
62	61	oveq2d	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(\frac{uk}{u}\right)=\Lambda \left(u\right)\left(\log N-\log u\right)$$
63		fzfid	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(1\dots \frac{N}{u}\right)\in \mathrm{Fin}$$
64		dvdsssfz1	$$⊢\frac{N}{u}\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\subseteq \left(1\dots \frac{N}{u}\right)$$
65	54 64	syl	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\subseteq \left(1\dots \frac{N}{u}\right)$$
66	63 65	ssfid	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\in \mathrm{Fin}$$
67	45 12	syl	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\in ℝ$$
68	67	recnd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\in ℂ$$
69		vmacl	$$⊢k\in \mathbb{N}\to \Lambda \left(k\right)\in ℝ$$
70	41 69	syl	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to \Lambda \left(k\right)\in ℝ$$
71	70	recnd	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to \Lambda \left(k\right)\in ℂ$$
72	51 71	eqeltrd	$$⊢\left(\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}\right)\to \Lambda \left(\frac{uk}{u}\right)\in ℂ$$
73	66 68 72	fsummulc2	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(\frac{uk}{u}\right)=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(u\right)\Lambda \left(\frac{uk}{u}\right)$$
74		relogcl	$$⊢N\in {ℝ}^{+}\to \log N\in ℝ$$
75	74	recnd	$$⊢N\in {ℝ}^{+}\to \log N\in ℂ$$
76	58 75	syl	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \log N\in ℂ$$
77	59	relogcld	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \log u\in ℝ$$
78	77	recnd	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \log u\in ℂ$$
79	68 76 78	subdid	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\left(\log N-\log u\right)=\Lambda \left(u\right)\log N-\Lambda \left(u\right)\log u$$
80	62 73 79	3eqtr3d	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(u\right)\Lambda \left(\frac{uk}{u}\right)=\Lambda \left(u\right)\log N-\Lambda \left(u\right)\log u$$
81	80	sumeq2dv	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{u}\right)\right\}}\Lambda \left(u\right)\Lambda \left(\frac{uk}{u}\right)=\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\left(\Lambda \left(u\right)\log N-\Lambda \left(u\right)\log u\right)$$
82	68 76	mulcld	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\log N\in ℂ$$
83	68 78	mulcld	$$⊢\left(N\in \mathbb{N}\wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \Lambda \left(u\right)\log u\in ℂ$$
84	3 82 83	fsumsub	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\left(\Lambda \left(u\right)\log N-\Lambda \left(u\right)\log u\right)=\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N-\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log u$$
85	57 75	syl	$$⊢N\in \mathbb{N}\to \log N\in ℂ$$
86	85	sqvald	$$⊢N\in \mathbb{N}\to {\log N}^2=\log N\log N$$
87		vmasum	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)=\log N$$
88	87	oveq1d	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N=\log N\log N$$
89	3 85 68	fsummulc1	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N=\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N$$
90	86 88 89	3eqtr2rd	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N={\log N}^2$$
91		fveq2	$$⊢u=d\to \Lambda \left(u\right)=\Lambda \left(d\right)$$
92		fveq2	$$⊢u=d\to \log u=\log d$$
93	91 92	oveq12d	$$⊢u=d\to \Lambda \left(u\right)\log u=\Lambda \left(d\right)\log d$$
94	93	cbvsumv	$$⊢\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log u=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
95	94	a1i	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log u=\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
96	90 95	oveq12d	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log N-\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(u\right)\log u={\log N}^2-\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
97	84 96	eqtrd	$$⊢N\in \mathbb{N}\to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\left(\Lambda \left(u\right)\log N-\Lambda \left(u\right)\log u\right)={\log N}^2-\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
98	38 81 97	3eqtrd	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)={\log N}^2-\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
99	98	oveq1d	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)+\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d={\log N}^2-\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d+\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d$$
100	85	sqcld	$$⊢N\in \mathbb{N}\to {\log N}^2\in ℂ$$
101	3 33	fsumcl	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d\in ℂ$$
102	100 101	npcand	$$⊢N\in \mathbb{N}\to {\log N}^2-\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d+\sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\Lambda \left(d\right)\log d={\log N}^2$$
103	34 99 102	3eqtrd	$$⊢N\in \mathbb{N}\to \sum _{d\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\left(\sum _{u\in \left\{x\in \mathbb{N}|x\parallel d\right\}}\Lambda \left(u\right)\Lambda \left(\frac{d}{u}\right)+\Lambda \left(d\right)\log d\right)={\log N}^2$$