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−12∈ℕ

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−12∈ℤ
23 20 21 22 3syl ⊢N∈ℙ∖2→2∥N−1↔N−12∈ℤ
24 17 23 mpbid ⊢N∈ℙ∖2→N−12∈ℤ
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−12
32 27 31 mpbid ⊢N−1∈ℕ→0<N−12
33 1 25 26 32 4syl ⊢N∈ℙ∖2→0<N−12
34 elnnz ⊢N−12∈ℕ↔N−12∈ℤ∧0<N−12
35 24 33 34 sylanbrc ⊢N∈ℙ∖2→N−12∈ℕ