| Step |
Hyp |
Ref |
Expression |
| 1 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
| 2 |
|
0red |
⊢ ( 𝐴 ∈ ℤ → 0 ∈ ℝ ) |
| 3 |
1 2
|
leloed |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 0 ↔ ( 𝐴 < 0 ∨ 𝐴 = 0 ) ) ) |
| 4 |
|
prmnn |
⊢ ( ( 2 · 𝐴 ) ∈ ℙ → ( 2 · 𝐴 ) ∈ ℕ ) |
| 5 |
|
nnnn0 |
⊢ ( ( 2 · 𝐴 ) ∈ ℕ → ( 2 · 𝐴 ) ∈ ℕ0 ) |
| 6 |
|
nn0ge0 |
⊢ ( ( 2 · 𝐴 ) ∈ ℕ0 → 0 ≤ ( 2 · 𝐴 ) ) |
| 7 |
|
2pos |
⊢ 0 < 2 |
| 8 |
7
|
a1i |
⊢ ( 𝐴 ∈ ℤ → 0 < 2 ) |
| 9 |
8
|
anim1i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( 0 < 2 ∧ 𝐴 < 0 ) ) |
| 10 |
9
|
olcd |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( ( 2 < 0 ∧ 0 < 𝐴 ) ∨ ( 0 < 2 ∧ 𝐴 < 0 ) ) ) |
| 11 |
|
2re |
⊢ 2 ∈ ℝ |
| 12 |
11
|
a1i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → 2 ∈ ℝ ) |
| 13 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ ) |
| 14 |
12 13
|
mul2lt0bi |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( ( 2 · 𝐴 ) < 0 ↔ ( ( 2 < 0 ∧ 0 < 𝐴 ) ∨ ( 0 < 2 ∧ 𝐴 < 0 ) ) ) ) |
| 15 |
10 14
|
mpbird |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( 2 · 𝐴 ) < 0 ) |
| 16 |
12 13
|
remulcld |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( 2 · 𝐴 ) ∈ ℝ ) |
| 17 |
|
0red |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → 0 ∈ ℝ ) |
| 18 |
16 17
|
ltnled |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ( ( 2 · 𝐴 ) < 0 ↔ ¬ 0 ≤ ( 2 · 𝐴 ) ) ) |
| 19 |
15 18
|
mpbid |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 < 0 ) → ¬ 0 ≤ ( 2 · 𝐴 ) ) |
| 20 |
19
|
ex |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 < 0 → ¬ 0 ≤ ( 2 · 𝐴 ) ) ) |
| 21 |
20
|
con2d |
⊢ ( 𝐴 ∈ ℤ → ( 0 ≤ ( 2 · 𝐴 ) → ¬ 𝐴 < 0 ) ) |
| 22 |
21
|
com12 |
⊢ ( 0 ≤ ( 2 · 𝐴 ) → ( 𝐴 ∈ ℤ → ¬ 𝐴 < 0 ) ) |
| 23 |
4 5 6 22
|
4syl |
⊢ ( ( 2 · 𝐴 ) ∈ ℙ → ( 𝐴 ∈ ℤ → ¬ 𝐴 < 0 ) ) |
| 24 |
23
|
com12 |
⊢ ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ → ¬ 𝐴 < 0 ) ) |
| 25 |
24
|
con2d |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 < 0 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) |
| 26 |
25
|
a1dd |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 < 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) ) |
| 27 |
|
oveq2 |
⊢ ( 𝐴 = 0 → ( 2 · 𝐴 ) = ( 2 · 0 ) ) |
| 28 |
|
2t0e0 |
⊢ ( 2 · 0 ) = 0 |
| 29 |
27 28
|
eqtrdi |
⊢ ( 𝐴 = 0 → ( 2 · 𝐴 ) = 0 ) |
| 30 |
|
0nprm |
⊢ ¬ 0 ∈ ℙ |
| 31 |
30
|
a1i |
⊢ ( 𝐴 = 0 → ¬ 0 ∈ ℙ ) |
| 32 |
29 31
|
eqneltrd |
⊢ ( 𝐴 = 0 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) |
| 33 |
32
|
a1i13 |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 = 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) ) |
| 34 |
26 33
|
jaod |
⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 < 0 ∨ 𝐴 = 0 ) → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) ) |
| 35 |
3 34
|
sylbid |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 0 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) ) |
| 36 |
|
2z |
⊢ 2 ∈ ℤ |
| 37 |
|
uzid |
⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) ) |
| 38 |
36 37
|
ax-mp |
⊢ 2 ∈ ( ℤ≥ ‘ 2 ) |
| 39 |
36
|
a1i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 2 ∈ ℤ ) |
| 40 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 𝐴 ∈ ℤ ) |
| 41 |
|
df-ne |
⊢ ( 𝐴 ≠ 1 ↔ ¬ 𝐴 = 1 ) |
| 42 |
|
1red |
⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℝ ) |
| 43 |
42 1
|
ltlend |
⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 ↔ ( 1 ≤ 𝐴 ∧ 𝐴 ≠ 1 ) ) ) |
| 44 |
|
1zzd |
⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℤ ) |
| 45 |
|
zltp1le |
⊢ ( ( 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) ) |
| 46 |
44 45
|
mpancom |
⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) ) |
| 47 |
46
|
biimpd |
⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → ( 1 + 1 ) ≤ 𝐴 ) ) |
| 48 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 49 |
48
|
breq1i |
⊢ ( 2 ≤ 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) |
| 50 |
47 49
|
imbitrrdi |
⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → 2 ≤ 𝐴 ) ) |
| 51 |
43 50
|
sylbird |
⊢ ( 𝐴 ∈ ℤ → ( ( 1 ≤ 𝐴 ∧ 𝐴 ≠ 1 ) → 2 ≤ 𝐴 ) ) |
| 52 |
51
|
expdimp |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ) → ( 𝐴 ≠ 1 → 2 ≤ 𝐴 ) ) |
| 53 |
41 52
|
biimtrrid |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ) → ( ¬ 𝐴 = 1 → 2 ≤ 𝐴 ) ) |
| 54 |
53
|
3impia |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 2 ≤ 𝐴 ) |
| 55 |
|
eluz2 |
⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) ) |
| 56 |
39 40 54 55
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) |
| 57 |
|
nprm |
⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 2 · 𝐴 ) ∈ ℙ ) |
| 58 |
38 56 57
|
sylancr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ ¬ 𝐴 = 1 ) → ¬ ( 2 · 𝐴 ) ∈ ℙ ) |
| 59 |
58
|
3exp |
⊢ ( 𝐴 ∈ ℤ → ( 1 ≤ 𝐴 → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) ) |
| 60 |
|
zle0orge1 |
⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ≤ 0 ∨ 1 ≤ 𝐴 ) ) |
| 61 |
35 59 60
|
mpjaod |
⊢ ( 𝐴 ∈ ℤ → ( ¬ 𝐴 = 1 → ¬ ( 2 · 𝐴 ) ∈ ℙ ) ) |
| 62 |
61
|
con4d |
⊢ ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ → 𝐴 = 1 ) ) |
| 63 |
|
oveq2 |
⊢ ( 𝐴 = 1 → ( 2 · 𝐴 ) = ( 2 · 1 ) ) |
| 64 |
|
2t1e2 |
⊢ ( 2 · 1 ) = 2 |
| 65 |
63 64
|
eqtrdi |
⊢ ( 𝐴 = 1 → ( 2 · 𝐴 ) = 2 ) |
| 66 |
|
2prm |
⊢ 2 ∈ ℙ |
| 67 |
65 66
|
eqeltrdi |
⊢ ( 𝐴 = 1 → ( 2 · 𝐴 ) ∈ ℙ ) |
| 68 |
62 67
|
impbid1 |
⊢ ( 𝐴 ∈ ℤ → ( ( 2 · 𝐴 ) ∈ ℙ ↔ 𝐴 = 1 ) ) |