prmo4

		Ref	Expression
	Assertion	prmo4	$⊢ #_{p} (4) = 6$

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

Metamath Proof Explorer