Theorem prmoval

Description: Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020)

	Ref	Expression
Assertion	prmoval	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)=\prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
2	1	prodeq1d	$$⊢n=N\to \prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)=\prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)$$
3		df-prmo	$$⊢{\#}_p=\left(n\in {\mathbb{N}}_0⟼\prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)\right)$$
4		prodex	$$⊢\prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)=\prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)$$