Metamath Proof Explorer

Theorem 9fppr8

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

Ref Expression
Assertion 9fppr8 
|- 9 e. ( FPPr ` 8 )

Proof

Step Hyp Ref Expression
1 8nn 
 |-  8 e. NN
2 4z 
 |-  4 e. ZZ
3 9nn 
 |-  9 e. NN
4 3 nnzi 
 |-  9 e. ZZ
5 4re 
 |-  4 e. RR
6 9re 
 |-  9 e. RR
7 4lt9 
 |-  4 < 9
8 5 6 7 ltleii 
 |-  4 <_ 9
9 eluz2 
 |-  ( 9 e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ 9 e. ZZ /\ 4 <_ 9 ) )
10 2 4 8 9 mpbir3an 
 |-  9 e. ( ZZ>= ` 4 )
11 2z 
 |-  2 e. ZZ
12 3z 
 |-  3 e. ZZ
13 2re 
 |-  2 e. RR
14 3re 
 |-  3 e. RR
15 2lt3 
 |-  2 < 3
16 13 14 15 ltleii 
 |-  2 <_ 3
17 eluz2 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 3 e. ZZ /\ 2 <_ 3 ) )
18 11 12 16 17 mpbir3an 
 |-  3 e. ( ZZ>= ` 2 )
19 nprm 
 |-  ( ( 3 e. ( ZZ>= ` 2 ) /\ 3 e. ( ZZ>= ` 2 ) ) -> -. ( 3 x. 3 ) e. Prime )
20 18 18 19 mp2an 
 |-  -. ( 3 x. 3 ) e. Prime
21 df-nel 
 |-  ( 9 e/ Prime <-> -. 9 e. Prime )
22 3t3e9 
 |-  ( 3 x. 3 ) = 9
23 22 eqcomi 
 |-  9 = ( 3 x. 3 )
24 23 eleq1i 
 |-  ( 9 e. Prime <-> ( 3 x. 3 ) e. Prime )
25 21 24 xchbinx 
 |-  ( 9 e/ Prime <-> -. ( 3 x. 3 ) e. Prime )
26 20 25 mpbir 
 |-  9 e/ Prime
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 e. ( ZZ>= ` 4 ) /\ 9 e/ Prime /\ ( ( 8 ^ ( 9 - 1 ) ) mod 9 ) = 1 )
33 fpprel 
 |-  ( 8 e. NN -> ( 9 e. ( FPPr ` 8 ) <-> ( 9 e. ( ZZ>= ` 4 ) /\ 9 e/ Prime /\ ( ( 8 ^ ( 9 - 1 ) ) mod 9 ) = 1 ) ) )
34 32 33 mpbiri 
 |-  ( 8 e. NN -> 9 e. ( FPPr ` 8 ) )
35 1 34 ax-mp 
 |-  9 e. ( FPPr ` 8 )