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

Proof

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