prmo3

		Ref	Expression
	Assertion	prmo3	$⊢ #_{p} (3) = 6$

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

Metamath Proof Explorer