Definition df-prmo 16714

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‘10) = 2 · 3 · 5 · 7 = 210 (see ex-prmo 28802).

In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 26308, where the primorial function is defined by using the sequence builder (𝑃 = seq1( · , 𝐹)), 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 = (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1))

Distinct variable group:   𝑘,𝑛

Detailed syntax breakdown of Definition df-prmo

Step	Hyp	Ref	Expression
1		cprmo 16713	. 2 class #p
2		vn	. . 3 setvar 𝑛
3		cn0 12216	. . 3 class ℕ0
4		c1 10856	. . . . 5 class 1
5	2	cv 1540	. . . . 5 class 𝑛
6		cfz 13221	. . . . 5 class ...
7	4, 5, 6	co 7268	. . . 4 class (1...𝑛)
8		vk	. . . . . . 7 setvar 𝑘
9	8	cv 1540	. . . . . 6 class 𝑘
10		cprime 16357	. . . . . 6 class ℙ
11	9, 10	wcel 2109	. . . . 5 wff 𝑘 ∈ ℙ
12	11, 9, 4	cif 4464	. . . 4 class if(𝑘 ∈ ℙ, 𝑘, 1)
13	7, 12, 8	cprod 15596	. . 3 class ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)
14	2, 3, 13	cmpt 5161	. 2 class (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1))
15	1, 14	wceq 1541	1 wff #p = (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1))

This definition is referenced by:  prmoval  16715