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 𝑝 ∈ ( ℤ ‘ 3 ) ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ )

Proof

Step Hyp Ref Expression
1 decex 3 4 1 ∈ V
2 eleq1 ( 𝑝 = 3 4 1 → ( 𝑝 ∈ ( ℤ ‘ 3 ) ↔ 3 4 1 ∈ ( ℤ ‘ 3 ) ) )
3 oveq2 ( 𝑝 = 3 4 1 → ( 2 ↑ 𝑝 ) = ( 2 ↑ 3 4 1 ) )
4 id ( 𝑝 = 3 4 1 → 𝑝 = 3 4 1 )
5 3 4 oveq12d ( 𝑝 = 3 4 1 → ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) )
6 oveq2 ( 𝑝 = 3 4 1 → ( 2 mod 𝑝 ) = ( 2 mod 3 4 1 ) )
7 5 6 eqeq12d ( 𝑝 = 3 4 1 → ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) ↔ ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) ) )
8 eleq1 ( 𝑝 = 3 4 1 → ( 𝑝 ∈ ℙ ↔ 3 4 1 ∈ ℙ ) )
9 7 8 imbi12d ( 𝑝 = 3 4 1 → ( ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ ) ) )
10 9 notbid ( 𝑝 = 3 4 1 → ( ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ¬ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ ) ) )
11 2 10 anbi12d ( 𝑝 = 3 4 1 → ( ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) ↔ ( 3 4 1 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ ) ) ) )
12 3z 3 ∈ ℤ
13 3nn0 3 ∈ ℕ0
14 4nn0 4 ∈ ℕ0
15 13 14 deccl 3 4 ∈ ℕ0
16 1nn0 1 ∈ ℕ0
17 15 16 deccl 3 4 1 ∈ ℕ0
18 17 nn0zi 3 4 1 ∈ ℤ
19 13 dec0h 3 = 0 3
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 < 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 ∈ ( ℤ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 3 4 1 ∈ ℤ ∧ 3 ≤ 3 4 1 ) )
33 12 18 31 32 mpbir3an 3 4 1 ∈ ( ℤ ‘ 3 )
34 341fppr2 3 4 1 ∈ ( FPPr ‘ 2 )
35 fpprwppr ( 3 4 1 ∈ ( 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 · 3 1 ) = 3 4 1
38 37 eqcomi 3 4 1 = ( 1 1 · 3 1 )
39 2z 2 ∈ ℤ
40 16 16 deccl 1 1 ∈ ℕ0
41 40 nn0zi 1 1 ∈ ℤ
42 2nn0 2 ∈ ℕ0
43 42 dec0h 2 = 0 2
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 0 2 ≤ 1 1
49 43 48 eqbrtri 2 ≤ 1 1
50 eluz2 ( 1 1 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 1 1 ∈ ℤ ∧ 2 ≤ 1 1 ) )
51 39 41 49 50 mpbir3an 1 1 ∈ ( ℤ ‘ 2 )
52 13 16 deccl 3 1 ∈ ℕ0
53 52 nn0zi 3 1 ∈ ℤ
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 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 3 1 ∈ ℤ ∧ 2 ≤ 3 1 ) )
58 39 53 56 57 mpbir3an 3 1 ∈ ( ℤ ‘ 2 )
59 nprm ( ( 1 1 ∈ ( ℤ ‘ 2 ) ∧ 3 1 ∈ ( ℤ ‘ 2 ) ) → ¬ ( 1 1 · 3 1 ) ∈ ℙ )
60 51 58 59 mp2an ¬ ( 1 1 · 3 1 ) ∈ ℙ
61 38 60 eqneltri ¬ 3 4 1 ∈ ℙ
62 36 61 pm3.2i ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) ∧ ¬ 3 4 1 ∈ ℙ )
63 annim ( ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) ∧ ¬ 3 4 1 ∈ ℙ ) ↔ ¬ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ ) )
64 62 63 mpbi ¬ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ )
65 33 64 pm3.2i ( 3 4 1 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 2 ↑ 3 4 1 ) mod 3 4 1 ) = ( 2 mod 3 4 1 ) → 3 4 1 ∈ ℙ ) )
66 1 11 65 ceqsexv2d 𝑝 ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) )
67 df-rex ( ∃ 𝑝 ∈ ( ℤ ‘ 3 ) ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ∃ 𝑝 ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
68 66 67 mpbir 𝑝 ∈ ( ℤ ‘ 3 ) ¬ ( ( ( 2 ↑ 𝑝 ) mod 𝑝 ) = ( 2 mod 𝑝 ) → 𝑝 ∈ ℙ )