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