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

Metamath Proof Explorer

Theorem odd2prm2

Description: If an odd number is the sum of two prime numbers, one of the prime numbers must be 2. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion odd2prm2 
|- ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( N = ( P + Q ) -> ( N e. Odd <-> ( P + Q ) e. Odd ) )
2 evennodd 
 |-  ( ( P + Q ) e. Even -> -. ( P + Q ) e. Odd )
3 2 pm2.21d 
 |-  ( ( P + Q ) e. Even -> ( ( P + Q ) e. Odd -> ( P = 2 \/ Q = 2 ) ) )
4 df-ne 
 |-  ( P =/= 2 <-> -. P = 2 )
5 eldifsn 
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
6 oddprmALTV 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Odd )
7 5 6 sylbir 
 |-  ( ( P e. Prime /\ P =/= 2 ) -> P e. Odd )
8 7 ex 
 |-  ( P e. Prime -> ( P =/= 2 -> P e. Odd ) )
9 4 8 biimtrrid 
 |-  ( P e. Prime -> ( -. P = 2 -> P e. Odd ) )
10 df-ne 
 |-  ( Q =/= 2 <-> -. Q = 2 )
11 eldifsn 
 |-  ( Q e. ( Prime \ { 2 } ) <-> ( Q e. Prime /\ Q =/= 2 ) )
12 oddprmALTV 
 |-  ( Q e. ( Prime \ { 2 } ) -> Q e. Odd )
13 11 12 sylbir 
 |-  ( ( Q e. Prime /\ Q =/= 2 ) -> Q e. Odd )
14 13 ex 
 |-  ( Q e. Prime -> ( Q =/= 2 -> Q e. Odd ) )
15 10 14 biimtrrid 
 |-  ( Q e. Prime -> ( -. Q = 2 -> Q e. Odd ) )
16 9 15 im2anan9 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( -. P = 2 /\ -. Q = 2 ) -> ( P e. Odd /\ Q e. Odd ) ) )
17 16 imp 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( -. P = 2 /\ -. Q = 2 ) ) -> ( P e. Odd /\ Q e. Odd ) )
18 opoeALTV 
 |-  ( ( P e. Odd /\ Q e. Odd ) -> ( P + Q ) e. Even )
19 17 18 syl 
 |-  ( ( ( P e. Prime /\ Q e. Prime ) /\ ( -. P = 2 /\ -. Q = 2 ) ) -> ( P + Q ) e. Even )
20 3 19 syl11 
 |-  ( ( P + Q ) e. Odd -> ( ( ( P e. Prime /\ Q e. Prime ) /\ ( -. P = 2 /\ -. Q = 2 ) ) -> ( P = 2 \/ Q = 2 ) ) )
21 20 expd 
 |-  ( ( P + Q ) e. Odd -> ( ( P e. Prime /\ Q e. Prime ) -> ( ( -. P = 2 /\ -. Q = 2 ) -> ( P = 2 \/ Q = 2 ) ) ) )
22 1 21 biimtrdi 
 |-  ( N = ( P + Q ) -> ( N e. Odd -> ( ( P e. Prime /\ Q e. Prime ) -> ( ( -. P = 2 /\ -. Q = 2 ) -> ( P = 2 \/ Q = 2 ) ) ) ) )
23 22 3imp231 
 |-  ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( ( -. P = 2 /\ -. Q = 2 ) -> ( P = 2 \/ Q = 2 ) ) )
24 23 com12 
 |-  ( ( -. P = 2 /\ -. Q = 2 ) -> ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) ) )
25 24 ex 
 |-  ( -. P = 2 -> ( -. Q = 2 -> ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) ) ) )
26 orc 
 |-  ( P = 2 -> ( P = 2 \/ Q = 2 ) )
27 26 a1d 
 |-  ( P = 2 -> ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) ) )
28 olc 
 |-  ( Q = 2 -> ( P = 2 \/ Q = 2 ) )
29 28 a1d 
 |-  ( Q = 2 -> ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) ) )
30 25 27 29 pm2.61ii 
 |-  ( ( N e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ N = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) )