9fppr8

Description: 9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023)

		Ref	Expression
	Assertion	9fppr8	$⊢ 9 \in FPPr (8)$

Step	Hyp	Ref	Expression
1		8nn	$⊢ 8 \in ℕ$
2		4z	$⊢ 4 \in ℤ$
3		9nn	$⊢ 9 \in ℕ$
4	3	nnzi	$⊢ 9 \in ℤ$
5		4re	$⊢ 4 \in ℝ$
6		9re	$⊢ 9 \in ℝ$
7		4lt9	$⊢ 4 < 9$
8	5 6 7	ltleii	$⊢ 4 \leq 9$
9		eluz2	$⊢ 9 \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land 9 \in ℤ \land 4 \leq 9)$
10	2 4 8 9	mpbir3an	$⊢ 9 \in ℤ_{\geq 4}$
11		2z	$⊢ 2 \in ℤ$
12		3z	$⊢ 3 \in ℤ$
13		2re	$⊢ 2 \in ℝ$
14		3re	$⊢ 3 \in ℝ$
15		2lt3	$⊢ 2 < 3$
16	13 14 15	ltleii	$⊢ 2 \leq 3$
17		eluz2	$⊢ 3 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 3 \in ℤ \land 2 \leq 3)$
18	11 12 16 17	mpbir3an	$⊢ 3 \in ℤ_{\geq 2}$
19		nprm	$⊢ (3 \in ℤ_{\geq 2} \land 3 \in ℤ_{\geq 2}) \to \neg 3 \cdot 3 \in ℙ$
20	18 18 19	mp2an	$⊢ \neg 3 \cdot 3 \in ℙ$
21		df-nel	$⊢ 9 \notin ℙ \leftrightarrow \neg 9 \in ℙ$
22		3t3e9	$⊢ 3 \cdot 3 = 9$
23	22	eqcomi	$⊢ 9 = 3 \cdot 3$
24	23	eleq1i	$⊢ 9 \in ℙ \leftrightarrow 3 \cdot 3 \in ℙ$
25	21 24	xchbinx	$⊢ 9 \notin ℙ \leftrightarrow \neg 3 \cdot 3 \in ℙ$
26	20 25	mpbir	$⊢ 9 \notin ℙ$
27		9m1e8	$⊢ 9 - 1 = 8$
28	27	oveq2i	$⊢ 8^{9 - 1} = 8^{8}$
29	28	oveq1i	$⊢ 8^{9 - 1} \mod 9 = 8^{8} \mod 9$
30		8exp8mod9	$⊢ 8^{8} \mod 9 = 1$
31	29 30	eqtri	$⊢ 8^{9 - 1} \mod 9 = 1$
32	10 26 31	3pm3.2i	$⊢ (9 \in ℤ_{\geq 4} \land 9 \notin ℙ \land 8^{9 - 1} \mod 9 = 1)$
33		fpprel	$⊢ 8 \in ℕ \to (9 \in FPPr (8) \leftrightarrow (9 \in ℤ_{\geq 4} \land 9 \notin ℙ \land 8^{9 - 1} \mod 9 = 1))$
34	32 33	mpbiri	$⊢ 8 \in ℕ \to 9 \in FPPr (8)$
35	1 34	ax-mp	$⊢ 9 \in FPPr (8)$

Metamath Proof Explorer