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