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 = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cprmo | |- #p |
|
| 1 | vn | |- n |
|
| 2 | cn0 | |- NN0 |
|
| 3 | vk | |- k |
|
| 4 | c1 | |- 1 |
|
| 5 | cfz | |- ... |
|
| 6 | 1 | cv | |- n |
| 7 | 4 6 5 | co | |- ( 1 ... n ) |
| 8 | 3 | cv | |- k |
| 9 | cprime | |- Prime |
|
| 10 | 8 9 | wcel | |- k e. Prime |
| 11 | 10 8 4 | cif | |- if ( k e. Prime , k , 1 ) |
| 12 | 7 11 3 | cprod | |- prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) |
| 13 | 1 2 12 | cmpt | |- ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) ) |
| 14 | 0 13 | wceq | |- #p = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) ) |