Metamath Proof Explorer

Theorem sbgoldbaltlem1

Description: Lemma 1 for sbgoldbalt : If an even number greater than 4 is the sum of two primes, one of the prime summands must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020)

Ref Expression
Assertion sbgoldbaltlem1 
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
2 nneoALTV 
 |-  ( Q e. NN -> ( Q e. Even <-> -. Q e. Odd ) )
3 2 bicomd 
 |-  ( Q e. NN -> ( -. Q e. Odd <-> Q e. Even ) )
4 1 3 syl 
 |-  ( Q e. Prime -> ( -. Q e. Odd <-> Q e. Even ) )
5 evenprm2 
 |-  ( Q e. Prime -> ( Q e. Even <-> Q = 2 ) )
6 4 5 bitrd 
 |-  ( Q e. Prime -> ( -. Q e. Odd <-> Q = 2 ) )
7 6 adantl 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( -. Q e. Odd <-> Q = 2 ) )
8 oveq2 
 |-  ( Q = 2 -> ( P + Q ) = ( P + 2 ) )
9 8 eqeq2d 
 |-  ( Q = 2 -> ( N = ( P + Q ) <-> N = ( P + 2 ) ) )
10 9 adantl 
 |-  ( ( P e. Prime /\ Q = 2 ) -> ( N = ( P + Q ) <-> N = ( P + 2 ) ) )
11 10 3anbi3d 
 |-  ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) <-> ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) ) )
12 breq2 
 |-  ( N = ( P + 2 ) -> ( 4 < N <-> 4 < ( P + 2 ) ) )
13 eleq1 
 |-  ( N = ( P + 2 ) -> ( N e. Even <-> ( P + 2 ) e. Even ) )
14 12 13 anbi12d 
 |-  ( N = ( P + 2 ) -> ( ( 4 < N /\ N e. Even ) <-> ( 4 < ( P + 2 ) /\ ( P + 2 ) e. Even ) ) )
15 prmz 
 |-  ( P e. Prime -> P e. ZZ )
16 2evenALTV 
 |-  2 e. Even
17 evensumeven 
 |-  ( ( P e. ZZ /\ 2 e. Even ) -> ( P e. Even <-> ( P + 2 ) e. Even ) )
18 15 16 17 sylancl 
 |-  ( P e. Prime -> ( P e. Even <-> ( P + 2 ) e. Even ) )
19 evenprm2 
 |-  ( P e. Prime -> ( P e. Even <-> P = 2 ) )
20 oveq1 
 |-  ( P = 2 -> ( P + 2 ) = ( 2 + 2 ) )
21 2p2e4 
 |-  ( 2 + 2 ) = 4
22 20 21 eqtrdi 
 |-  ( P = 2 -> ( P + 2 ) = 4 )
23 22 breq2d 
 |-  ( P = 2 -> ( 4 < ( P + 2 ) <-> 4 < 4 ) )
24 4re 
 |-  4 e. RR
25 24 ltnri 
 |-  -. 4 < 4
26 25 pm2.21i 
 |-  ( 4 < 4 -> Q e. Odd )
27 23 26 biimtrdi 
 |-  ( P = 2 -> ( 4 < ( P + 2 ) -> Q e. Odd ) )
28 19 27 biimtrdi 
 |-  ( P e. Prime -> ( P e. Even -> ( 4 < ( P + 2 ) -> Q e. Odd ) ) )
29 18 28 sylbird 
 |-  ( P e. Prime -> ( ( P + 2 ) e. Even -> ( 4 < ( P + 2 ) -> Q e. Odd ) ) )
30 29 com13 
 |-  ( 4 < ( P + 2 ) -> ( ( P + 2 ) e. Even -> ( P e. Prime -> Q e. Odd ) ) )
31 30 imp 
 |-  ( ( 4 < ( P + 2 ) /\ ( P + 2 ) e. Even ) -> ( P e. Prime -> Q e. Odd ) )
32 14 31 biimtrdi 
 |-  ( N = ( P + 2 ) -> ( ( 4 < N /\ N e. Even ) -> ( P e. Prime -> Q e. Odd ) ) )
33 32 expd 
 |-  ( N = ( P + 2 ) -> ( 4 < N -> ( N e. Even -> ( P e. Prime -> Q e. Odd ) ) ) )
34 33 com13 
 |-  ( N e. Even -> ( 4 < N -> ( N = ( P + 2 ) -> ( P e. Prime -> Q e. Odd ) ) ) )
35 34 3imp 
 |-  ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> ( P e. Prime -> Q e. Odd ) )
36 35 com12 
 |-  ( P e. Prime -> ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> Q e. Odd ) )
37 36 adantr 
 |-  ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> Q e. Odd ) )
38 11 37 sylbid 
 |-  ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )
39 38 ex 
 |-  ( P e. Prime -> ( Q = 2 -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) )
40 39 adantr 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( Q = 2 -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) )
41 7 40 sylbid 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( -. Q e. Odd -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) )
42 ax-1 
 |-  ( Q e. Odd -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )
43 41 42 pm2.61d2 
 |-  ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )