Metamath Proof Explorer

Theorem nfermltl8rev

Description: Fermat's little theorem with base 8 reversed is not generally true: There is an integer p (for example 9, see 9fppr8 ) so that " p is prime" does not follow from 8 ^ p == 8 (mod p ). (Contributed by AV, 3-Jun-2023)

Ref Expression
Assertion nfermltl8rev 
|- E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime )

Proof

Step Hyp Ref Expression
1 9nn 
 |-  9 e. NN
2 1 elexi 
 |-  9 e. _V
3 eleq1 
 |-  ( p = 9 -> ( p e. ( ZZ>= ` 3 ) <-> 9 e. ( ZZ>= ` 3 ) ) )
4 oveq2 
 |-  ( p = 9 -> ( 8 ^ p ) = ( 8 ^ 9 ) )
5 id 
 |-  ( p = 9 -> p = 9 )
6 4 5 oveq12d 
 |-  ( p = 9 -> ( ( 8 ^ p ) mod p ) = ( ( 8 ^ 9 ) mod 9 ) )
7 oveq2 
 |-  ( p = 9 -> ( 8 mod p ) = ( 8 mod 9 ) )
8 6 7 eqeq12d 
 |-  ( p = 9 -> ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) <-> ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) ) )
9 eleq1 
 |-  ( p = 9 -> ( p e. Prime <-> 9 e. Prime ) )
10 8 9 imbi12d 
 |-  ( p = 9 -> ( ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) <-> ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime ) ) )
11 10 notbid 
 |-  ( p = 9 -> ( -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) <-> -. ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime ) ) )
12 3 11 anbi12d 
 |-  ( p = 9 -> ( ( p e. ( ZZ>= ` 3 ) /\ -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) <-> ( 9 e. ( ZZ>= ` 3 ) /\ -. ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime ) ) ) )
13 3z 
 |-  3 e. ZZ
14 1 nnzi 
 |-  9 e. ZZ
15 3re 
 |-  3 e. RR
16 9re 
 |-  9 e. RR
17 3lt9 
 |-  3 < 9
18 15 16 17 ltleii 
 |-  3 <_ 9
19 eluz2 
 |-  ( 9 e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ 9 e. ZZ /\ 3 <_ 9 ) )
20 13 14 18 19 mpbir3an 
 |-  9 e. ( ZZ>= ` 3 )
21 8nn 
 |-  8 e. NN
22 8nn0 
 |-  8 e. NN0
23 0z 
 |-  0 e. ZZ
24 1nn0 
 |-  1 e. NN0
25 8exp8mod9 
 |-  ( ( 8 ^ 8 ) mod 9 ) = 1
26 1re 
 |-  1 e. RR
27 nnrp 
 |-  ( 9 e. NN -> 9 e. RR+ )
28 1 27 ax-mp 
 |-  9 e. RR+
29 0le1 
 |-  0 <_ 1
30 1lt9 
 |-  1 < 9
31 modid 
 |-  ( ( ( 1 e. RR /\ 9 e. RR+ ) /\ ( 0 <_ 1 /\ 1 < 9 ) ) -> ( 1 mod 9 ) = 1 )
32 26 28 29 30 31 mp4an 
 |-  ( 1 mod 9 ) = 1
33 25 32 eqtr4i 
 |-  ( ( 8 ^ 8 ) mod 9 ) = ( 1 mod 9 )
34 8p1e9 
 |-  ( 8 + 1 ) = 9
35 8cn 
 |-  8 e. CC
36 35 addid2i 
 |-  ( 0 + 8 ) = 8
37 9cn 
 |-  9 e. CC
38 37 mul02i 
 |-  ( 0 x. 9 ) = 0
39 38 oveq1i 
 |-  ( ( 0 x. 9 ) + 8 ) = ( 0 + 8 )
40 35 mulid2i 
 |-  ( 1 x. 8 ) = 8
41 36 39 40 3eqtr4i 
 |-  ( ( 0 x. 9 ) + 8 ) = ( 1 x. 8 )
42 1 21 22 23 24 22 33 34 41 modxp1i 
 |-  ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 )
43 9nprm 
 |-  -. 9 e. Prime
44 42 43 pm3.2i 
 |-  ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) /\ -. 9 e. Prime )
45 annim 
 |-  ( ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) /\ -. 9 e. Prime ) <-> -. ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime ) )
46 44 45 mpbi 
 |-  -. ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime )
47 20 46 pm3.2i 
 |-  ( 9 e. ( ZZ>= ` 3 ) /\ -. ( ( ( 8 ^ 9 ) mod 9 ) = ( 8 mod 9 ) -> 9 e. Prime ) )
48 2 12 47 ceqsexv2d 
 |-  E. p ( p e. ( ZZ>= ` 3 ) /\ -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) )
49 df-rex 
 |-  ( E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) <-> E. p ( p e. ( ZZ>= ` 3 ) /\ -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime ) ) )
50 48 49 mpbir 
 |-  E. p e. ( ZZ>= ` 3 ) -. ( ( ( 8 ^ p ) mod p ) = ( 8 mod p ) -> p e. Prime )