prmo5

		Ref	Expression
	Assertion	prmo5	$⊢ #_{p} (5) = 30$

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

Metamath Proof Explorer