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 = ( 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmo	⊢ #p
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		c1	⊢ 1
5		cfz	⊢ ...
6	1	cv	⊢ 𝑛
7	4 6 5	co	⊢ ( 1 ... 𝑛 )
8	3	cv	⊢ 𝑘
9		cprime	⊢ ℙ
10	8 9	wcel	⊢ 𝑘 ∈ ℙ
11	10 8 4	cif	⊢ if ( 𝑘 ∈ ℙ , 𝑘 , 1 )
12	7 11 3	cprod	⊢ ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 )
13	1 2 12	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
14	0 13	wceq	⊢ #p = ( 𝑛 ∈ ℕ0 ↦ ∏ 𝑘 ∈ ( 1 ... 𝑛 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )