vma1

Description: The von Mangoldt function at 1 . (Contributed by Mario Carneiro, 9-Apr-2016)

		Ref	Expression
	Assertion	vma1	$⊢ Λ (1) = 0$

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ (p \in ℙ \land k \in ℕ) \to 1 \in ℝ$
2		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
3	2	adantr	$⊢ (p \in ℙ \land k \in ℕ) \to p \in ℤ_{\geq 2}$
4		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
5	3 4	sylib	$⊢ (p \in ℙ \land k \in ℕ) \to (p \in ℕ \land 1 < p)$
6	5	simpld	$⊢ (p \in ℙ \land k \in ℕ) \to p \in ℕ$
7	6	nnred	$⊢ (p \in ℙ \land k \in ℕ) \to p \in ℝ$
8		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
9	8	adantl	$⊢ (p \in ℙ \land k \in ℕ) \to k \in ℕ_{0}$
10	7 9	reexpcld	$⊢ (p \in ℙ \land k \in ℕ) \to p^{k} \in ℝ$
11	5	simprd	$⊢ (p \in ℙ \land k \in ℕ) \to 1 < p$
12	6	nncnd	$⊢ (p \in ℙ \land k \in ℕ) \to p \in ℂ$
13	12	exp1d	$⊢ (p \in ℙ \land k \in ℕ) \to p^{1} = p$
14	6	nnge1d	$⊢ (p \in ℙ \land k \in ℕ) \to 1 \leq p$
15		simpr	$⊢ (p \in ℙ \land k \in ℕ) \to k \in ℕ$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17	15 16	eleqtrdi	$⊢ (p \in ℙ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
18	7 14 17	leexp2ad	$⊢ (p \in ℙ \land k \in ℕ) \to p^{1} \leq p^{k}$
19	13 18	eqbrtrrd	$⊢ (p \in ℙ \land k \in ℕ) \to p \leq p^{k}$
20	1 7 10 11 19	ltletrd	$⊢ (p \in ℙ \land k \in ℕ) \to 1 < p^{k}$
21	1 20	ltned	$⊢ (p \in ℙ \land k \in ℕ) \to 1 \neq p^{k}$
22	21	neneqd	$⊢ (p \in ℙ \land k \in ℕ) \to \neg 1 = p^{k}$
23	22	nrexdv	$⊢ p \in ℙ \to \neg \exists k \in ℕ 1 = p^{k}$
24	23	nrex	$⊢ \neg \exists p \in ℙ \exists k \in ℕ 1 = p^{k}$
25		1nn	$⊢ 1 \in ℕ$
26		isppw2	$⊢ 1 \in ℕ \to (Λ (1) \neq 0 \leftrightarrow \exists p \in ℙ \exists k \in ℕ 1 = p^{k})$
27	25 26	ax-mp	$⊢ Λ (1) \neq 0 \leftrightarrow \exists p \in ℙ \exists k \in ℕ 1 = p^{k}$
28	27	necon1bbii	$⊢ \neg \exists p \in ℙ \exists k \in ℕ 1 = p^{k} \leftrightarrow Λ (1) = 0$
29	24 28	mpbi	$⊢ Λ (1) = 0$

Metamath Proof Explorer

Theorem vma1

Proof