Metamath Proof Explorer

Theorem prmo1

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

Ref Expression
Assertion prmo1 ⊢ # p ⁡ 1 = 1

Proof

Step Hyp Ref Expression
1 1nn0 ⊢ 1 ∈ ℕ 0
2 prmoval ⊢ 1 ∈ ℕ 0 → # p ⁡ 1 = ∏ k = 1 1 if k ∈ ℙ k 1
3 1 2 ax-mp ⊢ # p ⁡ 1 = ∏ k = 1 1 if k ∈ ℙ k 1
4 1z ⊢ 1 ∈ ℤ
5 ax-1cn ⊢ 1 ∈ ℂ
6 1nprm ⊢ ¬ 1 ∈ ℙ
7 eleq1 ⊢ k = 1 → k ∈ ℙ ↔ 1 ∈ ℙ
8 6 7 mtbiri ⊢ k = 1 → ¬ k ∈ ℙ
9 8 iffalsed ⊢ k = 1 → if k ∈ ℙ k 1 = 1
10 9 fprod1 ⊢ 1 ∈ ℤ ∧ 1 ∈ ℂ → ∏ k = 1 1 if k ∈ ℙ k 1 = 1
11 4 5 10 mp2an ⊢ ∏ k = 1 1 if k ∈ ℙ k 1 = 1
12 3 11 eqtri ⊢ # p ⁡ 1 = 1