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 ) )