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

Metamath Proof Explorer

Theorem efvmacl

Description: The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion efvmacl ( 𝐴 ∈ ℕ → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( ( Λ ‘ 𝐴 ) = 0 → ( exp ‘ ( Λ ‘ 𝐴 ) ) = ( exp ‘ 0 ) )
2 ef0 ⊢ ( exp ‘ 0 ) = 1
3 1 2 eqtrdi ⊢ ( ( Λ ‘ 𝐴 ) = 0 → ( exp ‘ ( Λ ‘ 𝐴 ) ) = 1 )
4 3 eleq1d ⊢ ( ( Λ ‘ 𝐴 ) = 0 → ( ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ ↔ 1 ∈ ℕ ) )
5 isppw2 ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
6 vmappw ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
7 6 fveq2d ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( exp ‘ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ) = ( exp ‘ ( log ‘ 𝑝 ) ) )
8 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
9 8 nnrpd ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
10 9 reeflogd ⊢ ( 𝑝 ∈ ℙ → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
11 10 8 eqeltrd ⊢ ( 𝑝 ∈ ℙ → ( exp ‘ ( log ‘ 𝑝 ) ) ∈ ℕ )
12 11 adantr ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( exp ‘ ( log ‘ 𝑝 ) ) ∈ ℕ )
13 7 12 eqeltrd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( exp ‘ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℕ )
14 fveq2 ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝐴 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
15 14 fveq2d ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( exp ‘ ( Λ ‘ 𝐴 ) ) = ( exp ‘ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
16 15 eleq1d ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ ↔ ( exp ‘ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℕ ) )
17 13 16 syl5ibrcom ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ ) )
18 17 rexlimivv ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )
19 5 18 biimtrdi ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ ) )
20 19 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ ( Λ ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )
21 1nn ⊢ 1 ∈ ℕ
22 21 a1i ⊢ ( 𝐴 ∈ ℕ → 1 ∈ ℕ )
23 4 20 22 pm2.61ne ⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )