Metamath Proof Explorer

Theorem evenprm2

Description: A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020)

Ref Expression
Assertion evenprm2 ⊢ P ∈ ℙ → P ∈ Even ↔ P = 2

Proof

Step Hyp Ref Expression
1 2a1 ⊢ P = 2 → P ∈ ℙ → P ∈ Even → P = 2
2 df-ne ⊢ P ≠ 2 ↔ ¬ P = 2
3 2 biimpri ⊢ ¬ P = 2 → P ≠ 2
4 3 anim2i ⊢ P ∈ ℙ ∧ ¬ P = 2 → P ∈ ℙ ∧ P ≠ 2
5 4 ancoms ⊢ ¬ P = 2 ∧ P ∈ ℙ → P ∈ ℙ ∧ P ≠ 2
6 eldifsn ⊢ P ∈ ℙ ∖ 2 ↔ P ∈ ℙ ∧ P ≠ 2
7 5 6 sylibr ⊢ ¬ P = 2 ∧ P ∈ ℙ → P ∈ ℙ ∖ 2
8 oddprmALTV ⊢ P ∈ ℙ ∖ 2 → P ∈ Odd
9 oddneven ⊢ P ∈ Odd → ¬ P ∈ Even
10 9 pm2.21d ⊢ P ∈ Odd → P ∈ Even → P = 2
11 7 8 10 3syl ⊢ ¬ P = 2 ∧ P ∈ ℙ → P ∈ Even → P = 2
12 11 ex ⊢ ¬ P = 2 → P ∈ ℙ → P ∈ Even → P = 2
13 1 12 pm2.61i ⊢ P ∈ ℙ → P ∈ Even → P = 2
14 2evenALTV ⊢ 2 ∈ Even
15 eleq1 ⊢ P = 2 → P ∈ Even ↔ 2 ∈ Even
16 14 15 mpbiri ⊢ P = 2 → P ∈ Even
17 13 16 impbid1 ⊢ P ∈ ℙ → P ∈ Even ↔ P = 2