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	⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )

Proof

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

Metamath Proof Explorer

Theorem oddprm

Proof