Definition df-prmo 15736

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

In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 24904, 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.)

Assertion

Ref	Expression
df-prmo	|- #p = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )

Distinct variable group:   k, n

Detailed syntax breakdown of Definition df-prmo

Step	Hyp	Ref	Expression
1		cprmo 15735	. 2 class #p
2		vn	. . 3 setvar n
3		cn0 11292	. . 3 class NN0
4		c1 9937	. . . . 5 class 1
5	2	cv 1482	. . . . 5 class n
6		cfz 12326	. . . . 5 class ...
7	4, 5, 6	co 6650	. . . 4 class ( 1 ... n )
8		vk	. . . . . . 7 setvar k
9	8	cv 1482	. . . . . 6 class k
10		cprime 15385	. . . . . 6 class Prime
11	9, 10	wcel 1990	. . . . 5 wff k e. Prime
12	11, 9, 4	cif 4086	. . . 4 class if ( k e. Prime , k , 1 )
13	7, 12, 8	cprod 14635	. . 3 class prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 )
14	2, 3, 13	cmpt 4729	. 2 class ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
15	1, 14	wceq 1483	1 wff #p = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )

This definition is referenced by:  prmoval  15737