Metamath Proof Explorer


Theorem vmaval

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

Ref Expression
Hypothesis vmaval.1 S = p | p A
Assertion vmaval A Λ A = if S = 1 log S 0

Proof

Step Hyp Ref Expression
1 vmaval.1 S = p | p A
2 prmex V
3 2 rabex p | p x V
4 3 a1i x = A p | p x V
5 id s = p | p x s = p | p x
6 breq2 x = A p x p A
7 6 rabbidv x = A p | p x = p | p A
8 7 1 eqtr4di x = A p | p x = S
9 5 8 sylan9eqr x = A s = p | p x s = S
10 9 fveqeq2d x = A s = p | p x s = 1 S = 1
11 9 unieqd x = A s = p | p x s = S
12 11 fveq2d x = A s = p | p x log s = log S
13 10 12 ifbieq1d x = A s = p | p x if s = 1 log s 0 = if S = 1 log S 0
14 4 13 csbied x = A p | p x / s if s = 1 log s 0 = if S = 1 log S 0
15 df-vma Λ = x p | p x / s if s = 1 log s 0
16 fvex log S V
17 c0ex 0 V
18 16 17 ifex if S = 1 log S 0 V
19 14 15 18 fvmpt A Λ A = if S = 1 log S 0