Metamath Proof Explorer


Syntax definition cprmo

Description: Extend class notation to include the primorial of nonnegative integers.

Ref Expression
Assertion cprmo class #p