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 addlidi ⊢ ( 0 + 8 ) = 8
37 9cn ⊢ 9 ∈ ℂ
38 37 mul02i ⊢ ( 0 · 9 ) = 0
39 38 oveq1i ⊢ ( ( 0 · 9 ) + 8 ) = ( 0 + 8 )
40 35 mullidi ⊢ ( 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 𝑝 ) → 𝑝 ∈ ℙ )