Theorem vmaf

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

	Ref	Expression
Assertion	vmaf	$$⊢\Lambda :\mathbb{N}⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢\log \bigcup s\in \mathrm{V}$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3	1 2	ifex	$$⊢if\left(\left|s\right|=1,\log \bigcup s,0\right)\in \mathrm{V}$$
4	3	csbex	$$⊢⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)\in \mathrm{V}$$
5	4	a1i	$$⊢\left(\top \wedge x\in \mathbb{N}\right)\to ⦋\left\{p\in \mathbb{P}|p\parallel x\right\}/s⦌if\left(\left|s\right|=1,\log \bigcup s,0\right)\in \mathrm{V}$$
6		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)$$
7	6	a1i	$$⊢\top \to \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)$$
8		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
9	8	adantl	$$⊢\left(\top \wedge n\in \mathbb{N}\right)\to \Lambda \left(n\right)\in ℝ$$
10	5 7 9	fmpt2d	$$⊢\top \to \Lambda :\mathbb{N}⟶ℝ$$
11	10	mptru	$$⊢\Lambda :\mathbb{N}⟶ℝ$$