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 𝑝 ) → 𝑝 ∈ ℙ )