Definition df-prmo

Description: Define the primorial function on nonnegative integers as the product of all prime numbers less than or equal to the integer. For example, ( #p1 0 ) = 2 x. 3 x. 5 x. 7 = 2 1 0 (see ex-prmo ).

In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht , where the primorial function is defined by using the sequence builder ( P = seq 1 ( x. , F ) ), the more specialized definition of a product of a series is used here. (Contributed by AV, 28-Aug-2020)

	Ref	Expression
Assertion	df-prmo	$$⊢{\#}_p=\left(n\in {\mathbb{N}}_0⟼\prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmo	$$class{\#}_p$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vk	$$setvark$$
4		c1	$$class1$$
5		cfz	$$class\dots$$
6	1	cv	$$setvarn$$
7	4 6 5	co	$$class\left(1\dots n\right)$$
8	3	cv	$$setvark$$
9		cprime	$$class\mathbb{P}$$
10	8 9	wcel	$$wffk\in \mathbb{P}$$
11	10 8 4	cif	$$classif\left(k\in \mathbb{P},k,1\right)$$
12	7 11 3	cprod	$$class\prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)$$
13	1 2 12	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼\prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)\right)$$
14	0 13	wceq	$$wff{\#}_p=\left(n\in {\mathbb{N}}_0⟼\prod _{k=1}^{n}if\left(k\in \mathbb{P},k,1\right)\right)$$