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 ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} (\sum_{u \in \{x \in ℕ \| x ∥ d\}} Λ (u) Λ (\frac{d}{u}) + Λ (d) \log d) = {\log N}^{2}$

Proof

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

Metamath Proof Explorer

Theorem logsqvma

Proof