Metamath Proof Explorer

Theorem prm2orodd

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

Ref Expression
Assertion prm2orodd 
|- ( P e. Prime -> ( P = 2 \/ -. 2 || P ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 dvdsprime 
 |-  ( ( P e. Prime /\ 2 e. NN ) -> ( 2 || P <-> ( 2 = P \/ 2 = 1 ) ) )
3 1 2 mpan2 
 |-  ( P e. Prime -> ( 2 || P <-> ( 2 = P \/ 2 = 1 ) ) )
4 eqcom 
 |-  ( 2 = P <-> P = 2 )
5 4 biimpi 
 |-  ( 2 = P -> P = 2 )
6 1ne2 
 |-  1 =/= 2
7 necom 
 |-  ( 1 =/= 2 <-> 2 =/= 1 )
8 eqneqall 
 |-  ( 2 = 1 -> ( 2 =/= 1 -> P = 2 ) )
9 8 com12 
 |-  ( 2 =/= 1 -> ( 2 = 1 -> P = 2 ) )
10 7 9 sylbi 
 |-  ( 1 =/= 2 -> ( 2 = 1 -> P = 2 ) )
11 6 10 ax-mp 
 |-  ( 2 = 1 -> P = 2 )
12 5 11 jaoi 
 |-  ( ( 2 = P \/ 2 = 1 ) -> P = 2 )
13 3 12 biimtrdi 
 |-  ( P e. Prime -> ( 2 || P -> P = 2 ) )
14 13 con3d 
 |-  ( P e. Prime -> ( -. P = 2 -> -. 2 || P ) )
15 14 orrd 
 |-  ( P e. Prime -> ( P = 2 \/ -. 2 || P ) )