prmo2

		Ref	Expression
	Assertion	prmo2	$⊢ #_{p} (2) = 2$

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2		prmonn2	$⊢ 2 \in ℕ \to #_{p} (2) = if (2 \in ℙ, #_{p} (2 - 1) \cdot 2, #_{p} (2 - 1))$
3	1 2	ax-mp	$⊢ #_{p} (2) = if (2 \in ℙ, #_{p} (2 - 1) \cdot 2, #_{p} (2 - 1))$
4		2prm	$⊢ 2 \in ℙ$
5	4	iftruei	$⊢ if (2 \in ℙ, #_{p} (2 - 1) \cdot 2, #_{p} (2 - 1)) = #_{p} (2 - 1) \cdot 2$
6		2m1e1	$⊢ 2 - 1 = 1$
7	6	fveq2i	$⊢ #_{p} (2 - 1) = #_{p} (1)$
8		prmo1	$⊢ #_{p} (1) = 1$
9	7 8	eqtri	$⊢ #_{p} (2 - 1) = 1$
10	9	oveq1i	$⊢ #_{p} (2 - 1) \cdot 2 = 1 \cdot 2$
11		2cn	$⊢ 2 \in ℂ$
12	11	mullidi	$⊢ 1 \cdot 2 = 2$
13	10 12	eqtri	$⊢ #_{p} (2 - 1) \cdot 2 = 2$
14	5 13	eqtri	$⊢ if (2 \in ℙ, #_{p} (2 - 1) \cdot 2, #_{p} (2 - 1)) = 2$
15	3 14	eqtri	$⊢ #_{p} (2) = 2$

Metamath Proof Explorer