Metamath Proof Explorer


Theorem oddprmALTV

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion oddprmALTV ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → 𝑁 ∈ Odd )

Proof

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 )