Theorem oddn2prm

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

	Ref	Expression
Assertion	oddn2prm	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ¬ 2 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		nnoddn2prm	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) )
2	1	simprd	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ¬ 2 ∥ 𝑁 )