This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) = ∏ 𝑘 ∈ ( 1 ... 1 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
3 1 2 ax-mp ⊢ ( #p ‘ 1 ) = ∏ 𝑘 ∈ ( 1 ... 1 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 )
4 1z ⊢ 1 ∈ ℤ
5 ax-1cn ⊢ 1 ∈ ℂ
6 1nprm ⊢ ¬ 1 ∈ ℙ
7 eleq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ∈ ℙ ↔ 1 ∈ ℙ ) )
8 6 7 mtbiri ⊢ ( 𝑘 = 1 → ¬ 𝑘 ∈ ℙ )
9 8 iffalsed ⊢ ( 𝑘 = 1 → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 )
10 9 fprod1 ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℂ ) → ∏ 𝑘 ∈ ( 1 ... 1 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 )
11 4 5 10 mp2an ⊢ ∏ 𝑘 ∈ ( 1 ... 1 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1
12 3 11 eqtri ⊢ ( #p ‘ 1 ) = 1