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−12∈ℕ
5 nnz ⊢N−12∈ℕ→N−12∈ℤ
6 nnz ⊢N∈ℕ→N∈ℤ
7 oddm1d2 ⊢N∈ℤ→¬2∥N↔N−12∈ℤ
8 6 7 syl ⊢N∈ℕ→¬2∥N↔N−12∈ℤ
9 5 8 syl5ibrcom ⊢N−12∈ℕ→N∈ℕ→¬2∥N
10 4 9 syl ⊢N∈ℙ∖2→N∈ℕ→¬2∥N
11 3 10 jcai ⊢N∈ℙ∖2→N∈ℕ∧¬2∥N