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 ∈ ℕ0
2		prmoval	⊢ ( 0 ∈ ℕ0 → ( #p ‘ 0 ) = ∏ 𝑘 ∈ ( 1 ... 0 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
3	1 2	ax-mp	⊢ ( #p ‘ 0 ) = ∏ 𝑘 ∈ ( 1 ... 0 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 )
4		fz10	⊢ ( 1 ... 0 ) = ∅
5	4	prodeq1i	⊢ ∏ 𝑘 ∈ ( 1 ... 0 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ∏ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , 𝑘 , 1 )
6		prod0	⊢ ∏ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1
7	3 5 6	3eqtri	⊢ ( #p ‘ 0 ) = 1