Metamath Proof Explorer

Theorem nnoddn2prm

Description: A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion nnoddn2prm ⊢ N ∈ ℙ ∖ 2 → N ∈ ℕ ∧ ¬ 2 ∥ N

Proof

Step Hyp Ref Expression
1 eldifi ⊢ N ∈ ℙ ∖ 2 → N ∈ ℙ
2 prmnn ⊢ N ∈ ℙ → N ∈ ℕ
3 1 2 syl ⊢ N ∈ ℙ ∖ 2 → N ∈ ℕ
4 oddprm ⊢ N ∈ ℙ ∖ 2 → N − 1 2 ∈ ℕ
5 nnz ⊢ N − 1 2 ∈ ℕ → N − 1 2 ∈ ℤ
6 nnz ⊢ N ∈ ℕ → N ∈ ℤ
7 oddm1d2 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℤ
8 6 7 syl ⊢ N ∈ ℕ → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℤ
9 5 8 syl5ibrcom ⊢ N − 1 2 ∈ ℕ → N ∈ ℕ → ¬ 2 ∥ N
10 4 9 syl ⊢ N ∈ ℙ ∖ 2 → N ∈ ℕ → ¬ 2 ∥ N
11 3 10 jcai ⊢ N ∈ ℙ ∖ 2 → N ∈ ℕ ∧ ¬ 2 ∥ N