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