Metamath Proof Explorer


Theorem prmo0

Description: The primorial of 0. (Contributed by AV, 28-Aug-2020)

Ref Expression
Assertion prmo0 #p0=1

Proof

Step Hyp Ref Expression
1 0nn0 00
2 prmoval 00#p0=k=10ifkk1
3 1 2 ax-mp #p0=k=10ifkk1
4 fz10 10=
5 4 prodeq1i k=10ifkk1=kifkk1
6 prod0 kifkk1=1
7 3 5 6 3eqtri #p0=1