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

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 ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )

Proof

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