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 
|- E. p e. ( ZZ>= ` 3 ) -. ( ( ( 2 ^ p ) mod p ) = ( 2 mod p ) -> p e. Prime )

Proof

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