This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ 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 ) ) )