prmo6

		Ref	Expression
	Assertion	prmo6	$⊢ #_{p} (6) = 30$

Step	Hyp	Ref	Expression
1		6nn	$⊢ 6 \in ℕ$
2		prmonn2	$⊢ 6 \in ℕ \to #_{p} (6) = if (6 \in ℙ, #_{p} (6 - 1) \cdot 6, #_{p} (6 - 1))$
3	1 2	ax-mp	$⊢ #_{p} (6) = if (6 \in ℙ, #_{p} (6 - 1) \cdot 6, #_{p} (6 - 1))$
4		6nprm	$⊢ \neg 6 \in ℙ$
5	4	iffalsei	$⊢ if (6 \in ℙ, #_{p} (6 - 1) \cdot 6, #_{p} (6 - 1)) = #_{p} (6 - 1)$
6	3 5	eqtri	$⊢ #_{p} (6) = #_{p} (6 - 1)$
7		6m1e5	$⊢ 6 - 1 = 5$
8	7	fveq2i	$⊢ #_{p} (6 - 1) = #_{p} (5)$
9		prmo5	$⊢ #_{p} (5) = 30$
10	8 9	eqtri	$⊢ #_{p} (6 - 1) = 30$
11	6 10	eqtri	$⊢ #_{p} (6) = 30$

Metamath Proof Explorer