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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → ( 𝑃 ∈ Odd ∧ 𝑄 ∈ Odd ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
2	1	zcnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
3		prmz	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
4	3	zcnd	⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℂ )
5		addcom	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ) → ( 𝑃 + 𝑄 ) = ( 𝑄 + 𝑃 ) )
6	2 4 5	syl2anr	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 + 𝑄 ) = ( 𝑄 + 𝑃 ) )
7	6	eqeq2d	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑄 + 𝑃 ) ) )
8	7	3anbi3d	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) ↔ ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑄 + 𝑃 ) ) ) )
9		sbgoldbaltlem1	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑄 + 𝑃 ) ) → 𝑃 ∈ Odd ) )
10	8 9	sylbid	⊢ ( ( 𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑃 ∈ Odd ) )
11	10	ancoms	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑃 ∈ Odd ) )
12		sbgoldbaltlem1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )
13	11 12	jcad	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → ( 𝑃 ∈ Odd ∧ 𝑄 ∈ Odd ) ) )