Theorem 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	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℝ )
2		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
3	2	adantr	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
4		eluz2b2	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
5	3 4	sylib	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
6	5	simpld	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
7	6	nnred	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℝ )
8		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
9	8	adantl	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
10	7 9	reexpcld	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ )
11	5	simprd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 < 𝑝 )
12	6	nncnd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℂ )
13	12	exp1d	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 1 ) = 𝑝 )
14	6	nnge1d	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑝 )
15		simpr	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
16		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
17	15 16	eleqtrdi	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
18	7 14 17	leexp2ad	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝑝 ↑ 1 ) ≤ ( 𝑝 ↑ 𝑘 ) )
19	13 18	eqbrtrrd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) )
20	1 7 10 11 19	ltletrd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 < ( 𝑝 ↑ 𝑘 ) )
21	1 20	ltned	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → 1 ≠ ( 𝑝 ↑ 𝑘 ) )
22	21	neneqd	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ¬ 1 = ( 𝑝 ↑ 𝑘 ) )
23	22	nrexdv	⊢ ( 𝑝 ∈ ℙ → ¬ ∃ 𝑘 ∈ ℕ 1 = ( 𝑝 ↑ 𝑘 ) )
24	23	nrex	⊢ ¬ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 1 = ( 𝑝 ↑ 𝑘 )
25		1nn	⊢ 1 ∈ ℕ
26		isppw2	⊢ ( 1 ∈ ℕ → ( ( Λ ‘ 1 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 1 = ( 𝑝 ↑ 𝑘 ) ) )
27	25 26	ax-mp	⊢ ( ( Λ ‘ 1 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 1 = ( 𝑝 ↑ 𝑘 ) )
28	27	necon1bbii	⊢ ( ¬ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 1 = ( 𝑝 ↑ 𝑘 ) ↔ ( Λ ‘ 1 ) = 0 )
29	24 28	mpbi	⊢ ( Λ ‘ 1 ) = 0