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 ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )