Metamath Proof Explorer

Theorem vmappw

Description: Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmappw ⊢P∈ℙ∧K∈ℕ→Λ⁡PK=log⁡P

Proof

Step Hyp Ref Expression
1 prmnn ⊢P∈ℙ→P∈ℕ
2 nnnn0 ⊢K∈ℕ→K∈ℕ0
3 nnexpcl ⊢P∈ℕ∧K∈ℕ0→PK∈ℕ
4 1 2 3 syl2an ⊢P∈ℙ∧K∈ℕ→PK∈ℕ
5 eqid ⊢p∈ℙ|p∥PK=p∈ℙ|p∥PK
6 5 vmaval ⊢PK∈ℕ→Λ⁡PK=ifp∈ℙ|p∥PK=1log⁡⋃p∈ℙ|p∥PK0
7 4 6 syl ⊢P∈ℙ∧K∈ℕ→Λ⁡PK=ifp∈ℙ|p∥PK=1log⁡⋃p∈ℙ|p∥PK0
8 df-rab ⊢p∈ℙ|p∥PK=p|p∈ℙ∧p∥PK
9 prmdvdsexpb ⊢p∈ℙ∧P∈ℙ∧K∈ℕ→p∥PK↔p=P
10 9 biimpd ⊢p∈ℙ∧P∈ℙ∧K∈ℕ→p∥PK→p=P
11 10 3coml ⊢P∈ℙ∧K∈ℕ∧p∈ℙ→p∥PK→p=P
12 11 3expa ⊢P∈ℙ∧K∈ℕ∧p∈ℙ→p∥PK→p=P
13 12 expimpd ⊢P∈ℙ∧K∈ℕ→p∈ℙ∧p∥PK→p=P
14 simpl ⊢P∈ℙ∧K∈ℕ→P∈ℙ
15 prmz ⊢P∈ℙ→P∈ℤ
16 iddvdsexp ⊢P∈ℤ∧K∈ℕ→P∥PK
17 15 16 sylan ⊢P∈ℙ∧K∈ℕ→P∥PK
18 14 17 jca ⊢P∈ℙ∧K∈ℕ→P∈ℙ∧P∥PK
19 eleq1 ⊢p=P→p∈ℙ↔P∈ℙ
20 breq1 ⊢p=P→p∥PK↔P∥PK
21 19 20 anbi12d ⊢p=P→p∈ℙ∧p∥PK↔P∈ℙ∧P∥PK
22 18 21 syl5ibrcom ⊢P∈ℙ∧K∈ℕ→p=P→p∈ℙ∧p∥PK
23 13 22 impbid ⊢P∈ℙ∧K∈ℕ→p∈ℙ∧p∥PK↔p=P
24 velsn ⊢p∈P↔p=P
25 23 24 bitr4di ⊢P∈ℙ∧K∈ℕ→p∈ℙ∧p∥PK↔p∈P
26 25 eqabcdv ⊢P∈ℙ∧K∈ℕ→p|p∈ℙ∧p∥PK=P
27 8 26 eqtrid ⊢P∈ℙ∧K∈ℕ→p∈ℙ|p∥PK=P
28 27 fveq2d ⊢P∈ℙ∧K∈ℕ→p∈ℙ|p∥PK=P
29 hashsng ⊢P∈ℙ→P=1
30 29 adantr ⊢P∈ℙ∧K∈ℕ→P=1
31 28 30 eqtrd ⊢P∈ℙ∧K∈ℕ→p∈ℙ|p∥PK=1
32 31 iftrued ⊢P∈ℙ∧K∈ℕ→ifp∈ℙ|p∥PK=1log⁡⋃p∈ℙ|p∥PK0=log⁡⋃p∈ℙ|p∥PK
33 27 unieqd ⊢P∈ℙ∧K∈ℕ→⋃p∈ℙ|p∥PK=⋃P
34 unisng ⊢P∈ℙ→⋃P=P
35 34 adantr ⊢P∈ℙ∧K∈ℕ→⋃P=P
36 33 35 eqtrd ⊢P∈ℙ∧K∈ℕ→⋃p∈ℙ|p∥PK=P
37 36 fveq2d ⊢P∈ℙ∧K∈ℕ→log⁡⋃p∈ℙ|p∥PK=log⁡P
38 7 32 37 3eqtrd ⊢P∈ℙ∧K∈ℕ→Λ⁡PK=log⁡P