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

Proof

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