This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )