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 e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> ( P e. Odd /\ Q e. Odd ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	|- ( P e. Prime -> P e. ZZ )
2	1	zcnd	|- ( P e. Prime -> P e. CC )
3		prmz	|- ( Q e. Prime -> Q e. ZZ )
4	3	zcnd	|- ( Q e. Prime -> Q e. CC )
5		addcom	|- ( ( P e. CC /\ Q e. CC ) -> ( P + Q ) = ( Q + P ) )
6	2 4 5	syl2anr	|- ( ( Q e. Prime /\ P e. Prime ) -> ( P + Q ) = ( Q + P ) )
7	6	eqeq2d	|- ( ( Q e. Prime /\ P e. Prime ) -> ( N = ( P + Q ) <-> N = ( Q + P ) ) )
8	7	3anbi3d	|- ( ( Q e. Prime /\ P e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) <-> ( N e. Even /\ 4 < N /\ N = ( Q + P ) ) ) )
9		sbgoldbaltlem1	|- ( ( Q e. Prime /\ P e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( Q + P ) ) -> P e. Odd ) )
10	8 9	sylbid	|- ( ( Q e. Prime /\ P e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> P e. Odd ) )
11	10	ancoms	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> P e. Odd ) )
12		sbgoldbaltlem1	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )
13	11 12	jcad	|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> ( P e. Odd /\ Q e. Odd ) ) )