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 ⊢ P ∈ ℙ ∧ Q ∈ ℙ → N ∈ Even ∧ 4 < N ∧ N = P + Q → Q ∈ Odd

Proof

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