Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-prmo | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-prmo | โข #p = (๐ โ โ0 โฆ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cprmo 16829 | . 2 class #p | |
2 | vn | . . 3 setvar ๐ | |
3 | cn0 12334 | . . 3 class โ0 | |
4 | c1 10973 | . . . . 5 class 1 | |
5 | 2 | cv 1539 | . . . . 5 class ๐ |
6 | cfz 13340 | . . . . 5 class ... | |
7 | 4, 5, 6 | co 7337 | . . . 4 class (1...๐) |
8 | vk | . . . . . . 7 setvar ๐ | |
9 | 8 | cv 1539 | . . . . . 6 class ๐ |
10 | cprime 16473 | . . . . . 6 class โ | |
11 | 9, 10 | wcel 2105 | . . . . 5 wff ๐ โ โ |
12 | 11, 9, 4 | cif 4473 | . . . 4 class if(๐ โ โ, ๐, 1) |
13 | 7, 12, 8 | cprod 15714 | . . 3 class โ๐ โ (1...๐)if(๐ โ โ, ๐, 1) |
14 | 2, 3, 13 | cmpt 5175 | . 2 class (๐ โ โ0 โฆ โ๐ โ (1...๐)if(๐ โ โ, ๐, 1)) |
15 | 1, 14 | wceq 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 |