Metamath Proof Explorer


Theorem nfermltl2rev

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

Ref Expression
Assertion nfermltl2rev p 3 ¬ 2 p mod p = 2 mod p p

Proof

Step Hyp Ref Expression
1 decex 341 V
2 eleq1 p = 341 p 3 341 3
3 oveq2 p = 341 2 p = 2 341
4 id p = 341 p = 341
5 3 4 oveq12d p = 341 2 p mod p = 2 341 mod 341
6 oveq2 p = 341 2 mod p = 2 mod 341
7 5 6 eqeq12d p = 341 2 p mod p = 2 mod p 2 341 mod 341 = 2 mod 341
8 eleq1 p = 341 p 341
9 7 8 imbi12d p = 341 2 p mod p = 2 mod p p 2 341 mod 341 = 2 mod 341 341
10 9 notbid p = 341 ¬ 2 p mod p = 2 mod p p ¬ 2 341 mod 341 = 2 mod 341 341
11 2 10 anbi12d p = 341 p 3 ¬ 2 p mod p = 2 mod p p 341 3 ¬ 2 341 mod 341 = 2 mod 341 341
12 3z 3
13 3nn0 3 0
14 4nn0 4 0
15 13 14 deccl 34 0
16 1nn0 1 0
17 15 16 deccl 341 0
18 17 nn0zi 341
19 13 dec0h 3 = 03
20 0nn0 0 0
21 3re 3
22 9re 9
23 3lt9 3 < 9
24 21 22 23 ltleii 3 9
25 3nn 3
26 0re 0
27 9pos 0 < 9
28 26 22 27 ltleii 0 9
29 25 14 20 28 decltdi 0 < 34
30 20 15 13 16 24 29 decleh 03 341
31 19 30 eqbrtri 3 341
32 eluz2 341 3 3 341 3 341
33 12 18 31 32 mpbir3an 341 3
34 341fppr2 341 FPPr 2
35 fpprwppr 341 FPPr 2 2 341 mod 341 = 2 mod 341
36 34 35 ax-mp 2 341 mod 341 = 2 mod 341
37 11t31e341 11 31 = 341
38 37 eqcomi 341 = 11 31
39 2z 2
40 16 16 deccl 11 0
41 40 nn0zi 11
42 2nn0 2 0
43 42 dec0h 2 = 02
44 2re 2
45 2lt9 2 < 9
46 44 22 45 ltleii 2 9
47 0lt1 0 < 1
48 20 16 42 16 46 47 decleh 02 11
49 43 48 eqbrtri 2 11
50 eluz2 11 2 2 11 2 11
51 39 41 49 50 mpbir3an 11 2
52 13 16 deccl 31 0
53 52 nn0zi 31
54 3pos 0 < 3
55 20 13 42 16 46 54 decleh 02 31
56 43 55 eqbrtri 2 31
57 eluz2 31 2 2 31 2 31
58 39 53 56 57 mpbir3an 31 2
59 nprm 11 2 31 2 ¬ 11 31
60 51 58 59 mp2an ¬ 11 31
61 38 60 eqneltri ¬ 341
62 36 61 pm3.2i 2 341 mod 341 = 2 mod 341 ¬ 341
63 annim 2 341 mod 341 = 2 mod 341 ¬ 341 ¬ 2 341 mod 341 = 2 mod 341 341
64 62 63 mpbi ¬ 2 341 mod 341 = 2 mod 341 341
65 33 64 pm3.2i 341 3 ¬ 2 341 mod 341 = 2 mod 341 341
66 1 11 65 ceqsexv2d p p 3 ¬ 2 p mod p = 2 mod p p
67 df-rex p 3 ¬ 2 p mod p = 2 mod p p p p 3 ¬ 2 p mod p = 2 mod p p
68 66 67 mpbir p 3 ¬ 2 p mod p = 2 mod p p