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 p 3 ¬ 8 p mod p = 8 mod p p

Proof

Step Hyp Ref Expression
1 9nn 9
2 1 elexi 9 V
3 eleq1 p = 9 p 3 9 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 9
10 8 9 imbi12d p = 9 8 p mod p = 8 mod p p 8 9 mod 9 = 8 mod 9 9
11 10 notbid p = 9 ¬ 8 p mod p = 8 mod p p ¬ 8 9 mod 9 = 8 mod 9 9
12 3 11 anbi12d p = 9 p 3 ¬ 8 p mod p = 8 mod p p 9 3 ¬ 8 9 mod 9 = 8 mod 9 9
13 3z 3
14 1 nnzi 9
15 3re 3
16 9re 9
17 3lt9 3 < 9
18 15 16 17 ltleii 3 9
19 eluz2 9 3 3 9 3 9
20 13 14 18 19 mpbir3an 9 3
21 8nn 8
22 8nn0 8 0
23 0z 0
24 1nn0 1 0
25 8exp8mod9 8 8 mod 9 = 1
26 1re 1
27 nnrp 9 9 +
28 1 27 ax-mp 9 +
29 0le1 0 1
30 1lt9 1 < 9
31 modid 1 9 + 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
36 35 addid2i 0 + 8 = 8
37 9cn 9
38 37 mul02i 0 9 = 0
39 38 oveq1i 0 9 + 8 = 0 + 8
40 35 mulid2i 1 8 = 8
41 36 39 40 3eqtr4i 0 9 + 8 = 1 8
42 1 21 22 23 24 22 33 34 41 modxp1i 8 9 mod 9 = 8 mod 9
43 9nprm ¬ 9
44 42 43 pm3.2i 8 9 mod 9 = 8 mod 9 ¬ 9
45 annim 8 9 mod 9 = 8 mod 9 ¬ 9 ¬ 8 9 mod 9 = 8 mod 9 9
46 44 45 mpbi ¬ 8 9 mod 9 = 8 mod 9 9
47 20 46 pm3.2i 9 3 ¬ 8 9 mod 9 = 8 mod 9 9
48 2 12 47 ceqsexv2d p p 3 ¬ 8 p mod p = 8 mod p p
49 df-rex p 3 ¬ 8 p mod p = 8 mod p p p p 3 ¬ 8 p mod p = 8 mod p p
50 48 49 mpbir p 3 ¬ 8 p mod p = 8 mod p p