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 16830
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 29111).

In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 26433, 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 16829 . 2 class #p
2 vn . . 3 setvar ๐‘›
3 cn0 12334 . . 3 class โ„•0
4 c1 10973 . . . . 5 class 1
52cv 1539 . . . . 5 class ๐‘›
6 cfz 13340 . . . . 5 class ...
74, 5, 6co 7337 . . . 4 class (1...๐‘›)
8 vk . . . . . . 7 setvar ๐‘˜
98cv 1539 . . . . . 6 class ๐‘˜
10 cprime 16473 . . . . . 6 class โ„™
119, 10wcel 2105 . . . . 5 wff ๐‘˜ โˆˆ โ„™
1211, 9, 4cif 4473 . . . 4 class if(๐‘˜ โˆˆ โ„™, ๐‘˜, 1)
137, 12, 8cprod 15714 . . 3 class โˆ๐‘˜ โˆˆ (1...๐‘›)if(๐‘˜ โˆˆ โ„™, ๐‘˜, 1)
142, 3, 13cmpt 5175 . 2 class (๐‘› โˆˆ โ„•0 โ†ฆ โˆ๐‘˜ โˆˆ (1...๐‘›)if(๐‘˜ โˆˆ โ„™, ๐‘˜, 1))
151, 14wceq 1540 1 wff #p = (๐‘› โˆˆ โ„•0 โ†ฆ โˆ๐‘˜ โˆˆ (1...๐‘›)if(๐‘˜ โˆˆ โ„™, ๐‘˜, 1))
Colors of variables: wff setvar class
This definition is referenced by:  prmoval  16831
  Copyright terms: Public domain W3C validator