# 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}=\left\{{p}\in ℙ|{p}\parallel {A}\right\}$
Assertion vmaval ${⊢}{A}\in ℕ\to \Lambda \left({A}\right)=if\left(\left|{S}\right|=1,\mathrm{log}\bigcup {S},0\right)$

### Proof

Step Hyp Ref Expression
1 vmaval.1 ${⊢}{S}=\left\{{p}\in ℙ|{p}\parallel {A}\right\}$
2 prmex ${⊢}ℙ\in \mathrm{V}$
3 2 rabex ${⊢}\left\{{p}\in ℙ|{p}\parallel {x}\right\}\in \mathrm{V}$
4 3 a1i ${⊢}{x}={A}\to \left\{{p}\in ℙ|{p}\parallel {x}\right\}\in \mathrm{V}$
5 id ${⊢}{s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\to {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}$
6 breq2 ${⊢}{x}={A}\to \left({p}\parallel {x}↔{p}\parallel {A}\right)$
7 6 rabbidv ${⊢}{x}={A}\to \left\{{p}\in ℙ|{p}\parallel {x}\right\}=\left\{{p}\in ℙ|{p}\parallel {A}\right\}$
8 7 1 eqtr4di ${⊢}{x}={A}\to \left\{{p}\in ℙ|{p}\parallel {x}\right\}={S}$
9 5 8 sylan9eqr ${⊢}\left({x}={A}\wedge {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\right)\to {s}={S}$
10 9 fveqeq2d ${⊢}\left({x}={A}\wedge {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\right)\to \left(\left|{s}\right|=1↔\left|{S}\right|=1\right)$
11 9 unieqd ${⊢}\left({x}={A}\wedge {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\right)\to \bigcup {s}=\bigcup {S}$
12 11 fveq2d ${⊢}\left({x}={A}\wedge {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\right)\to \mathrm{log}\bigcup {s}=\mathrm{log}\bigcup {S}$
13 10 12 ifbieq1d ${⊢}\left({x}={A}\wedge {s}=\left\{{p}\in ℙ|{p}\parallel {x}\right\}\right)\to if\left(\left|{s}\right|=1,\mathrm{log}\bigcup {s},0\right)=if\left(\left|{S}\right|=1,\mathrm{log}\bigcup {S},0\right)$
14 4 13 csbied
15 df-vma
16 fvex ${⊢}\mathrm{log}\bigcup {S}\in \mathrm{V}$
17 c0ex ${⊢}0\in \mathrm{V}$
18 16 17 ifex ${⊢}if\left(\left|{S}\right|=1,\mathrm{log}\bigcup {S},0\right)\in \mathrm{V}$
19 14 15 18 fvmpt ${⊢}{A}\in ℕ\to \Lambda \left({A}\right)=if\left(\left|{S}\right|=1,\mathrm{log}\bigcup {S},0\right)$