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 \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2)$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ N = P + Q \to (N \in Odd \leftrightarrow P + Q \in Odd)$
2		evennodd	$⊢ P + Q \in Even \to \neg P + Q \in Odd$
3	2	pm2.21d	$⊢ P + Q \in Even \to (P + Q \in Odd \to (P = 2 \lor Q = 2))$
4		df-ne	$⊢ P \neq 2 \leftrightarrow \neg P = 2$
5		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
6		oddprmALTV	$⊢ P \in (ℙ ∖ \{2\}) \to P \in Odd$
7	5 6	sylbir	$⊢ (P \in ℙ \land P \neq 2) \to P \in Odd$
8	7	ex	$⊢ P \in ℙ \to (P \neq 2 \to P \in Odd)$
9	4 8	biimtrrid	$⊢ P \in ℙ \to (\neg P = 2 \to P \in Odd)$
10		df-ne	$⊢ Q \neq 2 \leftrightarrow \neg Q = 2$
11		eldifsn	$⊢ Q \in (ℙ ∖ \{2\}) \leftrightarrow (Q \in ℙ \land Q \neq 2)$
12		oddprmALTV	$⊢ Q \in (ℙ ∖ \{2\}) \to Q \in Odd$
13	11 12	sylbir	$⊢ (Q \in ℙ \land Q \neq 2) \to Q \in Odd$
14	13	ex	$⊢ Q \in ℙ \to (Q \neq 2 \to Q \in Odd)$
15	10 14	biimtrrid	$⊢ Q \in ℙ \to (\neg Q = 2 \to Q \in Odd)$
16	9 15	im2anan9	$⊢ (P \in ℙ \land Q \in ℙ) \to ((\neg P = 2 \land \neg Q = 2) \to (P \in Odd \land Q \in Odd))$
17	16	imp	$⊢ ((P \in ℙ \land Q \in ℙ) \land (\neg P = 2 \land \neg Q = 2)) \to (P \in Odd \land Q \in Odd)$
18		opoeALTV	$⊢ (P \in Odd \land Q \in Odd) \to P + Q \in Even$
19	17 18	syl	$⊢ ((P \in ℙ \land Q \in ℙ) \land (\neg P = 2 \land \neg Q = 2)) \to P + Q \in Even$
20	3 19	syl11	$⊢ P + Q \in Odd \to (((P \in ℙ \land Q \in ℙ) \land (\neg P = 2 \land \neg Q = 2)) \to (P = 2 \lor Q = 2))$
21	20	expd	$⊢ P + Q \in Odd \to ((P \in ℙ \land Q \in ℙ) \to ((\neg P = 2 \land \neg Q = 2) \to (P = 2 \lor Q = 2)))$
22	1 21	syl6bi	$⊢ N = P + Q \to (N \in Odd \to ((P \in ℙ \land Q \in ℙ) \to ((\neg P = 2 \land \neg Q = 2) \to (P = 2 \lor Q = 2))))$
23	22	3imp231	$⊢ (N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to ((\neg P = 2 \land \neg Q = 2) \to (P = 2 \lor Q = 2))$
24	23	com12	$⊢ (\neg P = 2 \land \neg Q = 2) \to ((N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2))$
25	24	ex	$⊢ \neg P = 2 \to (\neg Q = 2 \to ((N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2)))$
26		orc	$⊢ P = 2 \to (P = 2 \lor Q = 2)$
27	26	a1d	$⊢ P = 2 \to ((N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2))$
28		olc	$⊢ Q = 2 \to (P = 2 \lor Q = 2)$
29	28	a1d	$⊢ Q = 2 \to ((N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2))$
30	25 27 29	pm2.61ii	$⊢ (N \in Odd \land (P \in ℙ \land Q \in ℙ) \land N = P + Q) \to (P = 2 \lor Q = 2)$

Metamath Proof Explorer

Theorem odd2prm2

Proof