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 syl5bir ( 𝑅 ∈ ℙ → ( ¬ 𝑅 = 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 syl5bi ( ( 𝑁 ∈ 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 ) )