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

Proof

Step Hyp Ref Expression
1 9nn 9 ∈ ℕ
2 1 elexi 9 ∈ V
3 eleq1 ( 𝑝 = 9 → ( 𝑝 ∈ ( ℤ ‘ 3 ) ↔ 9 ∈ ( ℤ ‘ 3 ) ) )
4 oveq2 ( 𝑝 = 9 → ( 8 ↑ 𝑝 ) = ( 8 ↑ 9 ) )
5 id ( 𝑝 = 9 → 𝑝 = 9 )
6 4 5 oveq12d ( 𝑝 = 9 → ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( ( 8 ↑ 9 ) mod 9 ) )
7 oveq2 ( 𝑝 = 9 → ( 8 mod 𝑝 ) = ( 8 mod 9 ) )
8 6 7 eqeq12d ( 𝑝 = 9 → ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) ↔ ( ( 8 ↑ 9 ) mod 9 ) = ( 8 mod 9 ) ) )
9 eleq1 ( 𝑝 = 9 → ( 𝑝 ∈ ℙ ↔ 9 ∈ ℙ ) )
10 8 9 imbi12d ( 𝑝 = 9 → ( ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ( ( ( 8 ↑ 9 ) mod 9 ) = ( 8 mod 9 ) → 9 ∈ ℙ ) ) )
11 10 notbid ( 𝑝 = 9 → ( ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ¬ ( ( ( 8 ↑ 9 ) mod 9 ) = ( 8 mod 9 ) → 9 ∈ ℙ ) ) )
12 3 11 anbi12d ( 𝑝 = 9 → ( ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) ↔ ( 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 𝑝 ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) )
49 df-rex ( ∃ 𝑝 ∈ ( ℤ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ↔ ∃ 𝑝 ( 𝑝 ∈ ( ℤ ‘ 3 ) ∧ ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ ) ) )
50 48 49 mpbir 𝑝 ∈ ( ℤ ‘ 3 ) ¬ ( ( ( 8 ↑ 𝑝 ) mod 𝑝 ) = ( 8 mod 𝑝 ) → 𝑝 ∈ ℙ )