Theorem prm2orodd

Description: A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021)

	Ref	Expression
Assertion	prm2orodd	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ ¬ 2 ∥ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		dvdsprime	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑃 ↔ ( 2 = 𝑃 ∨ 2 = 1 ) ) )
3	1 2	mpan2	⊢ ( 𝑃 ∈ ℙ → ( 2 ∥ 𝑃 ↔ ( 2 = 𝑃 ∨ 2 = 1 ) ) )
4		eqcom	⊢ ( 2 = 𝑃 ↔ 𝑃 = 2 )
5	4	biimpi	⊢ ( 2 = 𝑃 → 𝑃 = 2 )
6		1ne2	⊢ 1 ≠ 2
7		necom	⊢ ( 1 ≠ 2 ↔ 2 ≠ 1 )
8		eqneqall	⊢ ( 2 = 1 → ( 2 ≠ 1 → 𝑃 = 2 ) )
9	8	com12	⊢ ( 2 ≠ 1 → ( 2 = 1 → 𝑃 = 2 ) )
10	7 9	sylbi	⊢ ( 1 ≠ 2 → ( 2 = 1 → 𝑃 = 2 ) )
11	6 10	ax-mp	⊢ ( 2 = 1 → 𝑃 = 2 )
12	5 11	jaoi	⊢ ( ( 2 = 𝑃 ∨ 2 = 1 ) → 𝑃 = 2 )
13	3 12	syl6bi	⊢ ( 𝑃 ∈ ℙ → ( 2 ∥ 𝑃 → 𝑃 = 2 ) )
14	13	con3d	⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 = 2 → ¬ 2 ∥ 𝑃 ) )
15	14	orrd	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ ¬ 2 ∥ 𝑃 ) )