This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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