Metamath Proof Explorer


Theorem sbgoldbaltlem2

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

Ref Expression
Assertion sbgoldbaltlem2 P Q N Even 4 < N N = P + Q P Odd Q Odd

Proof

Step Hyp Ref Expression
1 prmz P P
2 1 zcnd P P
3 prmz Q Q
4 3 zcnd Q Q
5 addcom P Q P + Q = Q + P
6 2 4 5 syl2anr Q P P + Q = Q + P
7 6 eqeq2d Q P N = P + Q N = Q + P
8 7 3anbi3d Q P N Even 4 < N N = P + Q N Even 4 < N N = Q + P
9 sbgoldbaltlem1 Q P N Even 4 < N N = Q + P P Odd
10 8 9 sylbid Q P N Even 4 < N N = P + Q P Odd
11 10 ancoms P Q N Even 4 < N N = P + Q P Odd
12 sbgoldbaltlem1 P Q N Even 4 < N N = P + Q Q Odd
13 11 12 jcad P Q N Even 4 < N N = P + Q P Odd Q Odd