Metamath Proof Explorer

Theorem oddprm

Description: A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion oddprm ⊢ N ∈ ℙ ∖ 2 → N − 1 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 eldifi ⊢ N ∈ ℙ ∖ 2 → N ∈ ℙ
2 prmz ⊢ N ∈ ℙ → N ∈ ℤ
3 1 2 syl ⊢ N ∈ ℙ ∖ 2 → N ∈ ℤ
4 eldifsni ⊢ N ∈ ℙ ∖ 2 → N ≠ 2
5 4 necomd ⊢ N ∈ ℙ ∖ 2 → 2 ≠ N
6 5 neneqd ⊢ N ∈ ℙ ∖ 2 → ¬ 2 = N
7 2z ⊢ 2 ∈ ℤ
8 uzid ⊢ 2 ∈ ℤ → 2 ∈ ℤ ≥ 2
9 7 8 ax-mp ⊢ 2 ∈ ℤ ≥ 2
10 dvdsprm ⊢ 2 ∈ ℤ ≥ 2 ∧ N ∈ ℙ → 2 ∥ N ↔ 2 = N
11 9 1 10 sylancr ⊢ N ∈ ℙ ∖ 2 → 2 ∥ N ↔ 2 = N
12 6 11 mtbird ⊢ N ∈ ℙ ∖ 2 → ¬ 2 ∥ N
13 1z ⊢ 1 ∈ ℤ
14 n2dvds1 ⊢ ¬ 2 ∥ 1
15 omoe ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N ∧ 1 ∈ ℤ ∧ ¬ 2 ∥ 1 → 2 ∥ N − 1
16 13 14 15 mpanr12 ⊢ N ∈ ℤ ∧ ¬ 2 ∥ N → 2 ∥ N − 1
17 3 12 16 syl2anc ⊢ N ∈ ℙ ∖ 2 → 2 ∥ N − 1
18 prmnn ⊢ N ∈ ℙ → N ∈ ℕ
19 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
20 1 18 19 3syl ⊢ N ∈ ℙ ∖ 2 → N − 1 ∈ ℕ 0
21 nn0z ⊢ N − 1 ∈ ℕ 0 → N − 1 ∈ ℤ
22 evend2 ⊢ N − 1 ∈ ℤ → 2 ∥ N − 1 ↔ N − 1 2 ∈ ℤ
23 20 21 22 3syl ⊢ N ∈ ℙ ∖ 2 → 2 ∥ N − 1 ↔ N − 1 2 ∈ ℤ
24 17 23 mpbid ⊢ N ∈ ℙ ∖ 2 → N − 1 2 ∈ ℤ
25 prmuz2 ⊢ N ∈ ℙ → N ∈ ℤ ≥ 2
26 uz2m1nn ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ
27 nngt0 ⊢ N − 1 ∈ ℕ → 0 < N − 1
28 nnre ⊢ N − 1 ∈ ℕ → N − 1 ∈ ℝ
29 2rp ⊢ 2 ∈ ℝ +
30 29 a1i ⊢ N − 1 ∈ ℕ → 2 ∈ ℝ +
31 28 30 gt0divd ⊢ N − 1 ∈ ℕ → 0 < N − 1 ↔ 0 < N − 1 2
32 27 31 mpbid ⊢ N − 1 ∈ ℕ → 0 < N − 1 2
33 1 25 26 32 4syl ⊢ N ∈ ℙ ∖ 2 → 0 < N − 1 2
34 elnnz ⊢ N − 1 2 ∈ ℕ ↔ N − 1 2 ∈ ℤ ∧ 0 < N − 1 2
35 24 33 34 sylanbrc ⊢ N ∈ ℙ ∖ 2 → N − 1 2 ∈ ℕ