Theorem prmocl

Description: Closure of the primorial function. (Contributed by AV, 28-Aug-2020)

	Ref	Expression
Assertion	prmocl	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		prmoval	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)=\prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)$$
2		fzfid	$$⊢N\in {\mathbb{N}}_0\to \left(1\dots N\right)\in \mathrm{Fin}$$
3		elfznn	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{N}$$
4	3	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to k\in \mathbb{N}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6	5	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to 1\in \mathbb{N}$$
7	4 6	ifcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge k\in \left(1\dots N\right)\right)\to if\left(k\in \mathbb{P},k,1\right)\in \mathbb{N}$$
8	2 7	fprodnncl	$$⊢N\in {\mathbb{N}}_0\to \prod _{k=1}^{N}if\left(k\in \mathbb{P},k,1\right)\in \mathbb{N}$$
9	1 8	eqeltrd	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\in \mathbb{N}$$