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

Proof

Step Hyp Ref Expression
1 prmnn ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
2 nneoALTV ( 𝑄 ∈ ℕ → ( 𝑄 ∈ Even ↔ ¬ 𝑄 ∈ Odd ) )
3 2 bicomd ( 𝑄 ∈ ℕ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) )
4 1 3 syl ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) )
5 evenprm2 ( 𝑄 ∈ ℙ → ( 𝑄 ∈ Even ↔ 𝑄 = 2 ) )
6 4 5 bitrd ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) )
7 6 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) )
8 oveq2 ( 𝑄 = 2 → ( 𝑃 + 𝑄 ) = ( 𝑃 + 2 ) )
9 8 eqeq2d ( 𝑄 = 2 → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) )
10 9 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) )
11 10 3anbi3d ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) ↔ ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 2 ) ) ) )
12 breq2 ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 ↔ 4 < ( 𝑃 + 2 ) ) )
13 eleq1 ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑁 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
14 12 13 anbi12d ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁𝑁 ∈ Even ) ↔ ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) ) )
15 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
16 2evenALTV 2 ∈ Even
17 evensumeven ( ( 𝑃 ∈ ℤ ∧ 2 ∈ Even ) → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
18 15 16 17 sylancl ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) )
19 evenprm2 ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ 𝑃 = 2 ) )
20 oveq1 ( 𝑃 = 2 → ( 𝑃 + 2 ) = ( 2 + 2 ) )
21 2p2e4 ( 2 + 2 ) = 4
22 20 21 eqtrdi ( 𝑃 = 2 → ( 𝑃 + 2 ) = 4 )
23 22 breq2d ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) ↔ 4 < 4 ) )
24 4re 4 ∈ ℝ
25 24 ltnri ¬ 4 < 4
26 25 pm2.21i ( 4 < 4 → 𝑄 ∈ Odd )
27 23 26 syl6bi ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) )
28 19 27 syl6bi ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) )
29 18 28 sylbird ( 𝑃 ∈ ℙ → ( ( 𝑃 + 2 ) ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) )
30 29 com13 ( 4 < ( 𝑃 + 2 ) → ( ( 𝑃 + 2 ) ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) )
31 30 imp ( ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) )
32 14 31 syl6bi ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁𝑁 ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) )
33 32 expd ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 → ( 𝑁 ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) )
34 33 com13 ( 𝑁 ∈ Even → ( 4 < 𝑁 → ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) )
35 34 3imp ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 2 ) ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) )
36 35 com12 ( 𝑃 ∈ ℙ → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) )
37 36 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) )
38 11 37 sylbid ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )
39 38 ex ( 𝑃 ∈ ℙ → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
40 39 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
41 7 40 sylbid ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) )
42 ax-1 ( 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )
43 41 42 pm2.61d2 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) )