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 A e Λ A

Proof

Step Hyp Ref Expression
1 fveq2 Λ A = 0 e Λ A = e 0
2 ef0 e 0 = 1
3 1 2 eqtrdi Λ A = 0 e Λ A = 1
4 3 eleq1d Λ A = 0 e Λ A 1
5 isppw2 A Λ A 0 p k A = p k
6 vmappw p k Λ p k = log p
7 6 fveq2d p k e Λ p k = e log p
8 prmnn p p
9 8 nnrpd p p +
10 9 reeflogd p e log p = p
11 10 8 eqeltrd p e log p
12 11 adantr p k e log p
13 7 12 eqeltrd p k e Λ p k
14 fveq2 A = p k Λ A = Λ p k
15 14 fveq2d A = p k e Λ A = e Λ p k
16 15 eleq1d A = p k e Λ A e Λ p k
17 13 16 syl5ibrcom p k A = p k e Λ A
18 17 rexlimivv p k A = p k e Λ A
19 5 18 syl6bi A Λ A 0 e Λ A
20 19 imp A Λ A 0 e Λ A
21 1nn 1
22 21 a1i A 1
23 4 20 22 pm2.61ne A e Λ A