Theorem prmo0

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

	Ref	Expression
Assertion	prmo0	|- ( #p ` 0 ) = 1

Proof

Step	Hyp	Ref	Expression
1		0nn0	|- 0 e. NN0
2		prmoval	|- ( 0 e. NN0 -> ( #p ` 0 ) = prod_ k e. ( 1 ... 0 ) if ( k e. Prime , k , 1 ) )
3	1 2	ax-mp	|- ( #p ` 0 ) = prod_ k e. ( 1 ... 0 ) if ( k e. Prime , k , 1 )
4		fz10	|- ( 1 ... 0 ) = (/)
5	4	prodeq1i	|- prod_ k e. ( 1 ... 0 ) if ( k e. Prime , k , 1 ) = prod_ k e. (/) if ( k e. Prime , k , 1 )
6		prod0	|- prod_ k e. (/) if ( k e. Prime , k , 1 ) = 1
7	3 5 6	3eqtri	|- ( #p ` 0 ) = 1