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

Metamath Proof Explorer

Theorem even3prm2

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

Ref Expression
Assertion even3prm2 
|- ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( P = 2 \/ Q = 2 \/ R = 2 ) )

Proof

Step Hyp Ref Expression
1 olc 
 |-  ( R = 2 -> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) )
2 1 a1d 
 |-  ( R = 2 -> ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) ) )
3 df-ne 
 |-  ( R =/= 2 <-> -. R = 2 )
4 eldifsn 
 |-  ( R e. ( Prime \ { 2 } ) <-> ( R e. Prime /\ R =/= 2 ) )
5 oddprmALTV 
 |-  ( R e. ( Prime \ { 2 } ) -> R e. Odd )
6 emoo 
 |-  ( ( N e. Even /\ R e. Odd ) -> ( N - R ) e. Odd )
7 6 expcom 
 |-  ( R e. Odd -> ( N e. Even -> ( N - R ) e. Odd ) )
8 5 7 syl 
 |-  ( R e. ( Prime \ { 2 } ) -> ( N e. Even -> ( N - R ) e. Odd ) )
9 4 8 sylbir 
 |-  ( ( R e. Prime /\ R =/= 2 ) -> ( N e. Even -> ( N - R ) e. Odd ) )
10 9 ex 
 |-  ( R e. Prime -> ( R =/= 2 -> ( N e. Even -> ( N - R ) e. Odd ) ) )
11 3 10 biimtrrid 
 |-  ( R e. Prime -> ( -. R = 2 -> ( N e. Even -> ( N - R ) e. Odd ) ) )
12 11 com23 
 |-  ( R e. Prime -> ( N e. Even -> ( -. R = 2 -> ( N - R ) e. Odd ) ) )
13 12 3ad2ant3 
 |-  ( ( P e. Prime /\ Q e. Prime /\ R e. Prime ) -> ( N e. Even -> ( -. R = 2 -> ( N - R ) e. Odd ) ) )
14 13 impcom 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> ( -. R = 2 -> ( N - R ) e. Odd ) )
15 14 3adant3 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( -. R = 2 -> ( N - R ) e. Odd ) )
16 15 impcom 
 |-  ( ( -. R = 2 /\ ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) ) -> ( N - R ) e. Odd )
17 3simpa 
 |-  ( ( P e. Prime /\ Q e. Prime /\ R e. Prime ) -> ( P e. Prime /\ Q e. Prime ) )
18 17 3ad2ant2 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( P e. Prime /\ Q e. Prime ) )
19 18 adantl 
 |-  ( ( -. R = 2 /\ ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) ) -> ( P e. Prime /\ Q e. Prime ) )
20 eqcom 
 |-  ( N = ( ( P + Q ) + R ) <-> ( ( P + Q ) + R ) = N )
21 evenz 
 |-  ( N e. Even -> N e. ZZ )
22 21 zcnd 
 |-  ( N e. Even -> N e. CC )
23 22 adantr 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> N e. CC )
24 prmz 
 |-  ( R e. Prime -> R e. ZZ )
25 24 zcnd 
 |-  ( R e. Prime -> R e. CC )
26 25 3ad2ant3 
 |-  ( ( P e. Prime /\ Q e. Prime /\ R e. Prime ) -> R e. CC )
27 26 adantl 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> R e. CC )
28 prmz 
 |-  ( P e. Prime -> P e. ZZ )
29 prmz 
 |-  ( Q e. Prime -> Q e. ZZ )
30 zaddcl 
 |-  ( ( P e. ZZ /\ Q e. ZZ ) -> ( P + Q ) e. ZZ )
31 28 29 30 syl2an 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( P + Q ) e. ZZ )
32 31 zcnd 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( P + Q ) e. CC )
33 32 3adant3 
 |-  ( ( P e. Prime /\ Q e. Prime /\ R e. Prime ) -> ( P + Q ) e. CC )
34 33 adantl 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> ( P + Q ) e. CC )
35 23 27 34 subadd2d 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> ( ( N - R ) = ( P + Q ) <-> ( ( P + Q ) + R ) = N ) )
36 35 biimprd 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> ( ( ( P + Q ) + R ) = N -> ( N - R ) = ( P + Q ) ) )
37 20 36 biimtrid 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) ) -> ( N = ( ( P + Q ) + R ) -> ( N - R ) = ( P + Q ) ) )
38 37 3impia 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( N - R ) = ( P + Q ) )
39 38 adantl 
 |-  ( ( -. R = 2 /\ ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) ) -> ( N - R ) = ( P + Q ) )
40 odd2prm2 
 |-  ( ( ( N - R ) e. Odd /\ ( P e. Prime /\ Q e. Prime ) /\ ( N - R ) = ( P + Q ) ) -> ( P = 2 \/ Q = 2 ) )
41 16 19 39 40 syl3anc 
 |-  ( ( -. R = 2 /\ ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) ) -> ( P = 2 \/ Q = 2 ) )
42 41 orcd 
 |-  ( ( -. R = 2 /\ ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) ) -> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) )
43 42 ex 
 |-  ( -. R = 2 -> ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) ) )
44 2 43 pm2.61i 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) )
45 df-3or 
 |-  ( ( P = 2 \/ Q = 2 \/ R = 2 ) <-> ( ( P = 2 \/ Q = 2 ) \/ R = 2 ) )
46 44 45 sylibr 
 |-  ( ( N e. Even /\ ( P e. Prime /\ Q e. Prime /\ R e. Prime ) /\ N = ( ( P + Q ) + R ) ) -> ( P = 2 \/ Q = 2 \/ R = 2 ) )