pntsval2

Description: The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016)

		Ref	Expression
	Hypothesis	pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
	Assertion	pntsval2	$⊢ A \in ℝ \to S (A) = \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
2	1	pntsval	$⊢ A \in ℝ \to S (A) = \sum_{n = 1}^{⌊A⌋} Λ (n) (\log n + ψ (\frac{A}{n}))$
3		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
4	3	adantl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
5		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
6	4 5	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℝ$
7	6	recnd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℂ$
8	4	nnrpd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to n \in ℝ^{+}$
9	8	relogcld	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \log n \in ℝ$
10	9	recnd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \log n \in ℂ$
11		simpl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to A \in ℝ$
12	11 4	nndivred	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \frac{A}{n} \in ℝ$
13		chpcl	$⊢ \frac{A}{n} \in ℝ \to ψ (\frac{A}{n}) \in ℝ$
14	12 13	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to ψ (\frac{A}{n}) \in ℝ$
15	14	recnd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to ψ (\frac{A}{n}) \in ℂ$
16	7 10 15	adddid	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) (\log n + ψ (\frac{A}{n})) = Λ (n) \log n + Λ (n) ψ (\frac{A}{n})$
17	16	sumeq2dv	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} Λ (n) (\log n + ψ (\frac{A}{n})) = \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + Λ (n) ψ (\frac{A}{n}))$
18		fveq2	$⊢ n = m \to Λ (n) = Λ (m)$
19		oveq2	$⊢ n = m \to \frac{A}{n} = \frac{A}{m}$
20	19	fveq2d	$⊢ n = m \to ψ (\frac{A}{n}) = ψ (\frac{A}{m})$
21	18 20	oveq12d	$⊢ n = m \to Λ (n) ψ (\frac{A}{n}) = Λ (m) ψ (\frac{A}{m})$
22	21	cbvsumv	$⊢ \sum_{n = 1}^{⌊A⌋} Λ (n) ψ (\frac{A}{n}) = \sum_{m = 1}^{⌊A⌋} Λ (m) ψ (\frac{A}{m})$
23		fzfid	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{m}⌋) \in Fin$
24		elfznn	$⊢ m \in (1 \dots ⌊A⌋) \to m \in ℕ$
25	24	adantl	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to m \in ℕ$
26		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
27	25 26	syl	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to Λ (m) \in ℝ$
28	27	recnd	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to Λ (m) \in ℂ$
29		elfznn	$⊢ k \in (1 \dots ⌊\frac{A}{m}⌋) \to k \in ℕ$
30	29	adantl	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to k \in ℕ$
31		vmacl	$⊢ k \in ℕ \to Λ (k) \in ℝ$
32	30 31	syl	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to Λ (k) \in ℝ$
33	32	recnd	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to Λ (k) \in ℂ$
34	23 28 33	fsummulc2	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to Λ (m) \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (k) = \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (k)$
35		simpl	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to A \in ℝ$
36	35 25	nndivred	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to \frac{A}{m} \in ℝ$
37		chpval	$⊢ \frac{A}{m} \in ℝ \to ψ (\frac{A}{m}) = \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (k)$
38	36 37	syl	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to ψ (\frac{A}{m}) = \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (k)$
39	38	oveq2d	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to Λ (m) ψ (\frac{A}{m}) = Λ (m) \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (k)$
40	30	nncnd	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to k \in ℂ$
41	24	ad2antlr	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to m \in ℕ$
42	41	nncnd	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to m \in ℂ$
43	41	nnne0d	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to m \neq 0$
44	40 42 43	divcan3d	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to \frac{m k}{m} = k$
45	44	fveq2d	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to Λ (\frac{m k}{m}) = Λ (k)$
46	45	oveq2d	$⊢ ((A \in ℝ \land m \in (1 \dots ⌊A⌋)) \land k \in (1 \dots ⌊\frac{A}{m}⌋)) \to Λ (m) Λ (\frac{m k}{m}) = Λ (m) Λ (k)$
47	46	sumeq2dv	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (\frac{m k}{m}) = \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (k)$
48	34 39 47	3eqtr4d	$⊢ (A \in ℝ \land m \in (1 \dots ⌊A⌋)) \to Λ (m) ψ (\frac{A}{m}) = \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (\frac{m k}{m})$
49	48	sumeq2dv	$⊢ A \in ℝ \to \sum_{m = 1}^{⌊A⌋} Λ (m) ψ (\frac{A}{m}) = \sum_{m = 1}^{⌊A⌋} \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (\frac{m k}{m})$
50		fvoveq1	$⊢ n = m k \to Λ (\frac{n}{m}) = Λ (\frac{m k}{m})$
51	50	oveq2d	$⊢ n = m k \to Λ (m) Λ (\frac{n}{m}) = Λ (m) Λ (\frac{m k}{m})$
52		id	$⊢ A \in ℝ \to A \in ℝ$
53		ssrab2	$⊢ \{y \in ℕ \| y ∥ n\} \subseteq ℕ$
54		simpr	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to m \in \{y \in ℕ \| y ∥ n\}$
55	53 54	sseldi	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to m \in ℕ$
56	55 26	syl	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) \in ℝ$
57		dvdsdivcl	$⊢ (n \in ℕ \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in \{y \in ℕ \| y ∥ n\}$
58	4 57	sylan	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in \{y \in ℕ \| y ∥ n\}$
59	53 58	sseldi	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{m} \in ℕ$
60		vmacl	$⊢ \frac{n}{m} \in ℕ \to Λ (\frac{n}{m}) \in ℝ$
61	59 60	syl	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (\frac{n}{m}) \in ℝ$
62	56 61	remulcld	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{n}{m}) \in ℝ$
63	62	recnd	$⊢ ((A \in ℝ \land n \in (1 \dots ⌊A⌋)) \land m \in \{y \in ℕ \| y ∥ n\}) \to Λ (m) Λ (\frac{n}{m}) \in ℂ$
64	63	anasss	$⊢ (A \in ℝ \land (n \in (1 \dots ⌊A⌋) \land m \in \{y \in ℕ \| y ∥ n\})) \to Λ (m) Λ (\frac{n}{m}) \in ℂ$
65	51 52 64	dvdsflsumcom	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) = \sum_{m = 1}^{⌊A⌋} \sum_{k = 1}^{⌊\frac{A}{m}⌋} Λ (m) Λ (\frac{m k}{m})$
66	49 65	eqtr4d	$⊢ A \in ℝ \to \sum_{m = 1}^{⌊A⌋} Λ (m) ψ (\frac{A}{m}) = \sum_{n = 1}^{⌊A⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
67	22 66	syl5eq	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} Λ (n) ψ (\frac{A}{n}) = \sum_{n = 1}^{⌊A⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
68	67	oveq2d	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} Λ (n) \log n + \sum_{n = 1}^{⌊A⌋} Λ (n) ψ (\frac{A}{n}) = \sum_{n = 1}^{⌊A⌋} Λ (n) \log n + \sum_{n = 1}^{⌊A⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
69		fzfid	$⊢ A \in ℝ \to (1 \dots ⌊A⌋) \in Fin$
70	7 10	mulcld	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \log n \in ℂ$
71	7 15	mulcld	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) ψ (\frac{A}{n}) \in ℂ$
72	69 70 71	fsumadd	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + Λ (n) ψ (\frac{A}{n})) = \sum_{n = 1}^{⌊A⌋} Λ (n) \log n + \sum_{n = 1}^{⌊A⌋} Λ (n) ψ (\frac{A}{n})$
73		fzfid	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to (1 \dots n) \in Fin$
74		dvdsssfz1	$⊢ n \in ℕ \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
75	4 74	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
76	73 75	ssfid	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \{y \in ℕ \| y ∥ n\} \in Fin$
77	76 62	fsumrecl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℝ$
78	77	recnd	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}) \in ℂ$
79	69 70 78	fsumadd	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})) = \sum_{n = 1}^{⌊A⌋} Λ (n) \log n + \sum_{n = 1}^{⌊A⌋} \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m})$
80	68 72 79	3eqtr4d	$⊢ A \in ℝ \to \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + Λ (n) ψ (\frac{A}{n})) = \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$
81	2 17 80	3eqtrd	$⊢ A \in ℝ \to S (A) = \sum_{n = 1}^{⌊A⌋} (Λ (n) \log n + \sum_{m \in \{y \in ℕ \| y ∥ n\}} Λ (m) Λ (\frac{n}{m}))$

Metamath Proof Explorer

Theorem pntsval2

Proof