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

Proof

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

Metamath Proof Explorer

Theorem even3prm2

Proof