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 Λ P K = log P

Proof

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