Step |
Hyp |
Ref |
Expression |
1 |
|
eldifsn |
⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) ) |
2 |
|
prmz |
⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℤ ) |
3 |
2
|
adantr |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → 𝑁 ∈ ℤ ) |
4 |
|
necom |
⊢ ( 𝑁 ≠ 2 ↔ 2 ≠ 𝑁 ) |
5 |
|
df-ne |
⊢ ( 2 ≠ 𝑁 ↔ ¬ 2 = 𝑁 ) |
6 |
4 5
|
sylbb |
⊢ ( 𝑁 ≠ 2 → ¬ 2 = 𝑁 ) |
7 |
6
|
adantl |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 = 𝑁 ) |
8 |
|
1ne2 |
⊢ 1 ≠ 2 |
9 |
8
|
nesymi |
⊢ ¬ 2 = 1 |
10 |
9
|
a1i |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 = 1 ) |
11 |
|
ioran |
⊢ ( ¬ ( 2 = 𝑁 ∨ 2 = 1 ) ↔ ( ¬ 2 = 𝑁 ∧ ¬ 2 = 1 ) ) |
12 |
7 10 11
|
sylanbrc |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ ( 2 = 𝑁 ∨ 2 = 1 ) ) |
13 |
|
2nn |
⊢ 2 ∈ ℕ |
14 |
13
|
a1i |
⊢ ( 𝑁 ≠ 2 → 2 ∈ ℕ ) |
15 |
|
dvdsprime |
⊢ ( ( 𝑁 ∈ ℙ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑁 ↔ ( 2 = 𝑁 ∨ 2 = 1 ) ) ) |
16 |
14 15
|
sylan2 |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ( 2 ∥ 𝑁 ↔ ( 2 = 𝑁 ∨ 2 = 1 ) ) ) |
17 |
12 16
|
mtbird |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 ∥ 𝑁 ) |
18 |
|
isodd3 |
⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ) |
19 |
3 17 18
|
sylanbrc |
⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → 𝑁 ∈ Odd ) |
20 |
1 19
|
sylbi |
⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → 𝑁 ∈ Odd ) |