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