prmocl

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

		Ref	Expression
	Assertion	prmocl	$⊢ N \in ℕ_{0} \to #_{p} (N) \in ℕ$

Step	Hyp	Ref	Expression
1		prmoval	$⊢ N \in ℕ_{0} \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
2		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
3		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
4	3	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in ℕ$
5		1nn	$⊢ 1 \in ℕ$
6	5	a1i	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 \in ℕ$
7	4 6	ifcld	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) \in ℕ$
8	2 7	fprodnncl	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \in ℕ$
9	1 8	eqeltrd	$⊢ N \in ℕ_{0} \to #_{p} (N) \in ℕ$

Metamath Proof Explorer