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 ∥ 𝑁 ) )