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 syl6bi
 |-  ( P = 2 -> ( 4 < ( P + 2 ) -> Q e. Odd ) )
28 19 27 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 ) )