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 Q N Even 4 < N N = P + Q Q Odd

Proof

Step Hyp Ref Expression
1 prmnn Q Q
2 nneoALTV Q Q Even ¬ Q Odd
3 2 bicomd Q ¬ Q Odd Q Even
4 1 3 syl Q ¬ Q Odd Q Even
5 evenprm2 Q Q Even Q = 2
6 4 5 bitrd Q ¬ Q Odd Q = 2
7 6 adantl P Q ¬ Q 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 Q = 2 N = P + Q N = P + 2
11 10 3anbi3d P Q = 2 N Even 4 < N N = P + Q N Even 4 < N N = P + 2
12 breq2 N = P + 2 4 < N 4 < P + 2
13 eleq1 N = P + 2 N Even P + 2 Even
14 12 13 anbi12d N = P + 2 4 < N N Even 4 < P + 2 P + 2 Even
15 prmz P P
16 2evenALTV 2 Even
17 evensumeven P 2 Even P Even P + 2 Even
18 15 16 17 sylancl P P Even P + 2 Even
19 evenprm2 P P 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
25 24 ltnri ¬ 4 < 4
26 25 pm2.21i 4 < 4 Q Odd
27 23 26 syl6bi P = 2 4 < P + 2 Q Odd
28 19 27 syl6bi P P Even 4 < P + 2 Q Odd
29 18 28 sylbird P P + 2 Even 4 < P + 2 Q Odd
30 29 com13 4 < P + 2 P + 2 Even P Q Odd
31 30 imp 4 < P + 2 P + 2 Even P Q Odd
32 14 31 syl6bi N = P + 2 4 < N N Even P Q Odd
33 32 expd N = P + 2 4 < N N Even P Q Odd
34 33 com13 N Even 4 < N N = P + 2 P Q Odd
35 34 3imp N Even 4 < N N = P + 2 P Q Odd
36 35 com12 P N Even 4 < N N = P + 2 Q Odd
37 36 adantr P Q = 2 N Even 4 < N N = P + 2 Q Odd
38 11 37 sylbid P Q = 2 N Even 4 < N N = P + Q Q Odd
39 38 ex P Q = 2 N Even 4 < N N = P + Q Q Odd
40 39 adantr P Q Q = 2 N Even 4 < N N = P + Q Q Odd
41 7 40 sylbid P Q ¬ Q Odd N Even 4 < N N = P + Q Q Odd
42 ax-1 Q Odd N Even 4 < N N = P + Q Q Odd
43 41 42 pm2.61d2 P Q N Even 4 < N N = P + Q Q Odd