Theorem oddprmALTV

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Revised by AV, 21-Jun-2020)

	Ref	Expression
Assertion	oddprmALTV	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → 𝑁 ∈ Odd )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) )
2		prmz	⊢ ( 𝑁 ∈ ℙ → 𝑁 ∈ ℤ )
3	2	adantr	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → 𝑁 ∈ ℤ )
4		necom	⊢ ( 𝑁 ≠ 2 ↔ 2 ≠ 𝑁 )
5		df-ne	⊢ ( 2 ≠ 𝑁 ↔ ¬ 2 = 𝑁 )
6	4 5	sylbb	⊢ ( 𝑁 ≠ 2 → ¬ 2 = 𝑁 )
7	6	adantl	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 = 𝑁 )
8		1ne2	⊢ 1 ≠ 2
9	8	nesymi	⊢ ¬ 2 = 1
10	9	a1i	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 = 1 )
11		ioran	⊢ ( ¬ ( 2 = 𝑁 ∨ 2 = 1 ) ↔ ( ¬ 2 = 𝑁 ∧ ¬ 2 = 1 ) )
12	7 10 11	sylanbrc	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ ( 2 = 𝑁 ∨ 2 = 1 ) )
13		2nn	⊢ 2 ∈ ℕ
14	13	a1i	⊢ ( 𝑁 ≠ 2 → 2 ∈ ℕ )
15		dvdsprime	⊢ ( ( 𝑁 ∈ ℙ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑁 ↔ ( 2 = 𝑁 ∨ 2 = 1 ) ) )
16	14 15	sylan2	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ( 2 ∥ 𝑁 ↔ ( 2 = 𝑁 ∨ 2 = 1 ) ) )
17	12 16	mtbird	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → ¬ 2 ∥ 𝑁 )
18		isodd3	⊢ ( 𝑁 ∈ Odd ↔ ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) )
19	3 17 18	sylanbrc	⊢ ( ( 𝑁 ∈ ℙ ∧ 𝑁 ≠ 2 ) → 𝑁 ∈ Odd )
20	1 19	sylbi	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → 𝑁 ∈ Odd )