MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-prmo Structured version   Visualization version   GIF version

Definition df-prmo 15943
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 27658).

In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 25125, 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
StepHypRef Expression
1 cprmo 15942 . 2 class #p
2 vn . . 3 setvar 𝑛
3 cn0 11494 . . 3 class 0
4 c1 10139 . . . . 5 class 1
52cv 1630 . . . . 5 class 𝑛
6 cfz 12533 . . . . 5 class ...
74, 5, 6co 6793 . . . 4 class (1...𝑛)
8 vk . . . . . . 7 setvar 𝑘
98cv 1630 . . . . . 6 class 𝑘
10 cprime 15592 . . . . . 6 class
119, 10wcel 2145 . . . . 5 wff 𝑘 ∈ ℙ
1211, 9, 4cif 4225 . . . 4 class if(𝑘 ∈ ℙ, 𝑘, 1)
137, 12, 8cprod 14842 . . 3 class 𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)
142, 3, 13cmpt 4863 . 2 class (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1))
151, 14wceq 1631 1 wff #p = (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1))
Colors of variables: wff setvar class
This definition is referenced by:  prmoval  15944
  Copyright terms: Public domain W3C validator