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 
|- ( P e. Prime -> ( P e. Even <-> P = 2 ) )

Proof

Step Hyp Ref Expression
1 2a1 
 |-  ( P = 2 -> ( P e. Prime -> ( P e. Even -> P = 2 ) ) )
2 df-ne 
 |-  ( P =/= 2 <-> -. P = 2 )
3 2 biimpri 
 |-  ( -. P = 2 -> P =/= 2 )
4 3 anim2i 
 |-  ( ( P e. Prime /\ -. P = 2 ) -> ( P e. Prime /\ P =/= 2 ) )
5 4 ancoms 
 |-  ( ( -. P = 2 /\ P e. Prime ) -> ( P e. Prime /\ P =/= 2 ) )
6 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
7 5 6 sylibr 
 |-  ( ( -. P = 2 /\ P e. Prime ) -> P e. ( Prime \ { 2 } ) )
8 oddprmALTV 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Odd )
9 oddneven 
 |-  ( P e. Odd -> -. P e. Even )
10 9 pm2.21d 
 |-  ( P e. Odd -> ( P e. Even -> P = 2 ) )
11 7 8 10 3syl 
 |-  ( ( -. P = 2 /\ P e. Prime ) -> ( P e. Even -> P = 2 ) )
12 11 ex 
 |-  ( -. P = 2 -> ( P e. Prime -> ( P e. Even -> P = 2 ) ) )
13 1 12 pm2.61i 
 |-  ( P e. Prime -> ( P e. Even -> P = 2 ) )
14 2evenALTV 
 |-  2 e. Even
15 eleq1 
 |-  ( P = 2 -> ( P e. Even <-> 2 e. Even ) )
16 14 15 mpbiri 
 |-  ( P = 2 -> P e. Even )
17 13 16 impbid1 
 |-  ( P e. Prime -> ( P e. Even <-> P = 2 ) )