This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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