This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ 𝑃 = 2 ) )

Proof

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