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

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 biimtrdi ⊢ ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) )
28 19 27 biimtrdi ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ 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 biimtrdi ⊢ ( 𝑁 = ( 𝑃 + 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 ) )