Metamath Proof Explorer

Theorem odd2prm2

Description: If an odd number is the sum of two prime numbers, one of the prime numbers must be 2. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion odd2prm2 ⊢ N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ N = P + Q → N ∈ Odd ↔ P + Q ∈ Odd
2 evennodd ⊢ P + Q ∈ Even → ¬ P + Q ∈ Odd
3 2 pm2.21d ⊢ P + Q ∈ Even → P + Q ∈ Odd → P = 2 ∨ Q = 2
4 df-ne ⊢ P ≠ 2 ↔ ¬ P = 2
5 eldifsn ⊢ P ∈ ℙ ∖ 2 ↔ P ∈ ℙ ∧ P ≠ 2
6 oddprmALTV ⊢ P ∈ ℙ ∖ 2 → P ∈ Odd
7 5 6 sylbir ⊢ P ∈ ℙ ∧ P ≠ 2 → P ∈ Odd
8 7 ex ⊢ P ∈ ℙ → P ≠ 2 → P ∈ Odd
9 4 8 biimtrrid ⊢ P ∈ ℙ → ¬ P = 2 → P ∈ Odd
10 df-ne ⊢ Q ≠ 2 ↔ ¬ Q = 2
11 eldifsn ⊢ Q ∈ ℙ ∖ 2 ↔ Q ∈ ℙ ∧ Q ≠ 2
12 oddprmALTV ⊢ Q ∈ ℙ ∖ 2 → Q ∈ Odd
13 11 12 sylbir ⊢ Q ∈ ℙ ∧ Q ≠ 2 → Q ∈ Odd
14 13 ex ⊢ Q ∈ ℙ → Q ≠ 2 → Q ∈ Odd
15 10 14 biimtrrid ⊢ Q ∈ ℙ → ¬ Q = 2 → Q ∈ Odd
16 9 15 im2anan9 ⊢ P ∈ ℙ ∧ Q ∈ ℙ → ¬ P = 2 ∧ ¬ Q = 2 → P ∈ Odd ∧ Q ∈ Odd
17 16 imp ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ ¬ P = 2 ∧ ¬ Q = 2 → P ∈ Odd ∧ Q ∈ Odd
18 opoeALTV ⊢ P ∈ Odd ∧ Q ∈ Odd → P + Q ∈ Even
19 17 18 syl ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ ¬ P = 2 ∧ ¬ Q = 2 → P + Q ∈ Even
20 3 19 syl11 ⊢ P + Q ∈ Odd → P ∈ ℙ ∧ Q ∈ ℙ ∧ ¬ P = 2 ∧ ¬ Q = 2 → P = 2 ∨ Q = 2
21 20 expd ⊢ P + Q ∈ Odd → P ∈ ℙ ∧ Q ∈ ℙ → ¬ P = 2 ∧ ¬ Q = 2 → P = 2 ∨ Q = 2
22 1 21 biimtrdi ⊢ N = P + Q → N ∈ Odd → P ∈ ℙ ∧ Q ∈ ℙ → ¬ P = 2 ∧ ¬ Q = 2 → P = 2 ∨ Q = 2
23 22 3imp231 ⊢ N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → ¬ P = 2 ∧ ¬ Q = 2 → P = 2 ∨ Q = 2
24 23 com12 ⊢ ¬ P = 2 ∧ ¬ Q = 2 → N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2
25 24 ex ⊢ ¬ P = 2 → ¬ Q = 2 → N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2
26 orc ⊢ P = 2 → P = 2 ∨ Q = 2
27 26 a1d ⊢ P = 2 → N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2
28 olc ⊢ Q = 2 → P = 2 ∨ Q = 2
29 28 a1d ⊢ Q = 2 → N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2
30 25 27 29 pm2.61ii ⊢ N ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N = P + Q → P = 2 ∨ Q = 2