prmo1

		Ref	Expression
	Assertion	prmo1	$⊢ #_{p} (1) = 1$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		prmoval	$⊢ 1 \in ℕ_{0} \to #_{p} (1) = \prod_{k = 1}^{1} if (k \in ℙ, k, 1)$
3	1 2	ax-mp	$⊢ #_{p} (1) = \prod_{k = 1}^{1} if (k \in ℙ, k, 1)$
4		1z	$⊢ 1 \in ℤ$
5		ax-1cn	$⊢ 1 \in ℂ$
6		1nprm	$⊢ \neg 1 \in ℙ$
7		eleq1	$⊢ k = 1 \to (k \in ℙ \leftrightarrow 1 \in ℙ)$
8	6 7	mtbiri	$⊢ k = 1 \to \neg k \in ℙ$
9	8	iffalsed	$⊢ k = 1 \to if (k \in ℙ, k, 1) = 1$
10	9	fprod1	$⊢ (1 \in ℤ \land 1 \in ℂ) \to \prod_{k = 1}^{1} if (k \in ℙ, k, 1) = 1$
11	4 5 10	mp2an	$⊢ \prod_{k = 1}^{1} if (k \in ℙ, k, 1) = 1$
12	3 11	eqtri	$⊢ #_{p} (1) = 1$

Metamath Proof Explorer