Theorem 9fppr8

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

	Ref	Expression
Assertion	9fppr8	⊢ 9 ∈ ( FPPr ‘ 8 )

Proof

Step	Hyp	Ref	Expression
1		8nn	⊢ 8 ∈ ℕ
2		4z	⊢ 4 ∈ ℤ
3		9nn	⊢ 9 ∈ ℕ
4	3	nnzi	⊢ 9 ∈ ℤ
5		4re	⊢ 4 ∈ ℝ
6		9re	⊢ 9 ∈ ℝ
7		4lt9	⊢ 4 < 9
8	5 6 7	ltleii	⊢ 4 ≤ 9
9		eluz2	⊢ ( 9 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 9 ∈ ℤ ∧ 4 ≤ 9 ) )
10	2 4 8 9	mpbir3an	⊢ 9 ∈ ( ℤ≥ ‘ 4 )
11		2z	⊢ 2 ∈ ℤ
12		3z	⊢ 3 ∈ ℤ
13		2re	⊢ 2 ∈ ℝ
14		3re	⊢ 3 ∈ ℝ
15		2lt3	⊢ 2 < 3
16	13 14 15	ltleii	⊢ 2 ≤ 3
17		eluz2	⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3 ) )
18	11 12 16 17	mpbir3an	⊢ 3 ∈ ( ℤ≥ ‘ 2 )
19		nprm	⊢ ( ( 3 ∈ ( ℤ≥ ‘ 2 ) ∧ 3 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 3 · 3 ) ∈ ℙ )
20	18 18 19	mp2an	⊢ ¬ ( 3 · 3 ) ∈ ℙ
21		df-nel	⊢ ( 9 ∉ ℙ ↔ ¬ 9 ∈ ℙ )
22		3t3e9	⊢ ( 3 · 3 ) = 9
23	22	eqcomi	⊢ 9 = ( 3 · 3 )
24	23	eleq1i	⊢ ( 9 ∈ ℙ ↔ ( 3 · 3 ) ∈ ℙ )
25	21 24	xchbinx	⊢ ( 9 ∉ ℙ ↔ ¬ ( 3 · 3 ) ∈ ℙ )
26	20 25	mpbir	⊢ 9 ∉ ℙ
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 ∈ ( ℤ≥ ‘ 4 ) ∧ 9 ∉ ℙ ∧ ( ( 8 ↑ ( 9 − 1 ) ) mod 9 ) = 1 )
33		fpprel	⊢ ( 8 ∈ ℕ → ( 9 ∈ ( FPPr ‘ 8 ) ↔ ( 9 ∈ ( ℤ≥ ‘ 4 ) ∧ 9 ∉ ℙ ∧ ( ( 8 ↑ ( 9 − 1 ) ) mod 9 ) = 1 ) ) )
34	32 33	mpbiri	⊢ ( 8 ∈ ℕ → 9 ∈ ( FPPr ‘ 8 ) )
35	1 34	ax-mp	⊢ 9 ∈ ( FPPr ‘ 8 )