Metamath Proof Explorer

Theorem even3prm2

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

Ref Expression
Assertion even3prm2 ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2

Proof

Step Hyp Ref Expression
1 olc ⊢ R = 2 → P = 2 ∨ Q = 2 ∨ R = 2
2 1 a1d ⊢ R = 2 → N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2
3 df-ne ⊢ R ≠ 2 ↔ ¬ R = 2
4 eldifsn ⊢ R ∈ ℙ ∖ 2 ↔ R ∈ ℙ ∧ R ≠ 2
5 oddprmALTV ⊢ R ∈ ℙ ∖ 2 → R ∈ Odd
6 emoo ⊢ N ∈ Even ∧ R ∈ Odd → N − R ∈ Odd
7 6 expcom ⊢ R ∈ Odd → N ∈ Even → N − R ∈ Odd
8 5 7 syl ⊢ R ∈ ℙ ∖ 2 → N ∈ Even → N − R ∈ Odd
9 4 8 sylbir ⊢ R ∈ ℙ ∧ R ≠ 2 → N ∈ Even → N − R ∈ Odd
10 9 ex ⊢ R ∈ ℙ → R ≠ 2 → N ∈ Even → N − R ∈ Odd
11 3 10 syl5bir ⊢ R ∈ ℙ → ¬ R = 2 → N ∈ Even → N − R ∈ Odd
12 11 com23 ⊢ R ∈ ℙ → N ∈ Even → ¬ R = 2 → N − R ∈ Odd
13 12 3ad2ant3 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → N ∈ Even → ¬ R = 2 → N − R ∈ Odd
14 13 impcom ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → ¬ R = 2 → N − R ∈ Odd
15 14 3adant3 ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → ¬ R = 2 → N − R ∈ Odd
16 15 impcom ⊢ ¬ R = 2 ∧ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → N − R ∈ Odd
17 3simpa ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → P ∈ ℙ ∧ Q ∈ ℙ
18 17 3ad2ant2 ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P ∈ ℙ ∧ Q ∈ ℙ
19 18 adantl ⊢ ¬ R = 2 ∧ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P ∈ ℙ ∧ Q ∈ ℙ
20 eqcom ⊢ N = P + Q + R ↔ P + Q + R = N
21 evenz ⊢ N ∈ Even → N ∈ ℤ
22 21 zcnd ⊢ N ∈ Even → N ∈ ℂ
23 22 adantr ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → N ∈ ℂ
24 prmz ⊢ R ∈ ℙ → R ∈ ℤ
25 24 zcnd ⊢ R ∈ ℙ → R ∈ ℂ
26 25 3ad2ant3 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → R ∈ ℂ
27 26 adantl ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → R ∈ ℂ
28 prmz ⊢ P ∈ ℙ → P ∈ ℤ
29 prmz ⊢ Q ∈ ℙ → Q ∈ ℤ
30 zaddcl ⊢ P ∈ ℤ ∧ Q ∈ ℤ → P + Q ∈ ℤ
31 28 29 30 syl2an ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P + Q ∈ ℤ
32 31 zcnd ⊢ P ∈ ℙ ∧ Q ∈ ℙ → P + Q ∈ ℂ
33 32 3adant3 ⊢ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → P + Q ∈ ℂ
34 33 adantl ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → P + Q ∈ ℂ
35 23 27 34 subadd2d ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → N − R = P + Q ↔ P + Q + R = N
36 35 biimprd ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → P + Q + R = N → N − R = P + Q
37 20 36 syl5bi ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ → N = P + Q + R → N − R = P + Q
38 37 3impia ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → N − R = P + Q
39 38 adantl ⊢ ¬ R = 2 ∧ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → N − R = P + Q
40 odd2prm2 ⊢ N − R ∈ Odd ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ N − R = P + Q → P = 2 ∨ Q = 2
41 16 19 39 40 syl3anc ⊢ ¬ R = 2 ∧ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2
42 41 orcd ⊢ ¬ R = 2 ∧ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2
43 42 ex ⊢ ¬ R = 2 → N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2
44 2 43 pm2.61i ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2
45 df-3or ⊢ P = 2 ∨ Q = 2 ∨ R = 2 ↔ P = 2 ∨ Q = 2 ∨ R = 2
46 44 45 sylibr ⊢ N ∈ Even ∧ P ∈ ℙ ∧ Q ∈ ℙ ∧ R ∈ ℙ ∧ N = P + Q + R → P = 2 ∨ Q = 2 ∨ R = 2