Metamath Proof Explorer

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 = ∏ k = 1 0 if k ∈ ℙ k 1
3 1 2 ax-mp ⊢ # p ⁡ 0 = ∏ k = 1 0 if k ∈ ℙ k 1
4 fz10 ⊢ 1 … 0 = ∅
5 4 prodeq1i ⊢ ∏ k = 1 0 if k ∈ ℙ k 1 = ∏ k ∈ ∅ if k ∈ ℙ k 1
6 prod0 ⊢ ∏ k ∈ ∅ if k ∈ ℙ k 1 = 1
7 3 5 6 3eqtri ⊢ # p ⁡ 0 = 1