mogoldbblem

		Ref	Expression
	Assertion	mogoldbblem	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q$

Proof

Step	Hyp	Ref	Expression
1		2evenALTV	$⊢ 2 \in Even$
2		epee	$⊢ (N \in Even \land 2 \in Even) \to N + 2 \in Even$
3	1 2	mpan2	$⊢ N \in Even \to N + 2 \in Even$
4	3	3ad2ant2	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to N + 2 \in Even$
5		simp1	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to (P \in ℙ \land Q \in ℙ \land R \in ℙ)$
6		simp3	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to N + 2 = P + Q + R$
7		even3prm2	$⊢ (N + 2 \in Even \land (P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N + 2 = P + Q + R) \to (P = 2 \lor Q = 2 \lor R = 2)$
8	4 5 6 7	syl3anc	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to (P = 2 \lor Q = 2 \lor R = 2)$
9		oveq1	$⊢ P = 2 \to P + Q = 2 + Q$
10	9	oveq1d	$⊢ P = 2 \to P + Q + R = 2 + Q + R$
11	10	eqeq2d	$⊢ P = 2 \to (N + 2 = P + Q + R \leftrightarrow N + 2 = 2 + Q + R)$
12		2cnd	$⊢ (Q \in ℙ \land R \in ℙ) \to 2 \in ℂ$
13		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
14	13	zcnd	$⊢ Q \in ℙ \to Q \in ℂ$
15	14	adantr	$⊢ (Q \in ℙ \land R \in ℙ) \to Q \in ℂ$
16		prmz	$⊢ R \in ℙ \to R \in ℤ$
17	16	zcnd	$⊢ R \in ℙ \to R \in ℂ$
18	17	adantl	$⊢ (Q \in ℙ \land R \in ℙ) \to R \in ℂ$
19		simp1	$⊢ (2 \in ℂ \land Q \in ℂ \land R \in ℂ) \to 2 \in ℂ$
20		addcl	$⊢ (Q \in ℂ \land R \in ℂ) \to Q + R \in ℂ$
21	20	3adant1	$⊢ (2 \in ℂ \land Q \in ℂ \land R \in ℂ) \to Q + R \in ℂ$
22		addass	$⊢ (2 \in ℂ \land Q \in ℂ \land R \in ℂ) \to 2 + Q + R = 2 + Q + R$
23	19 21 22	comraddd	$⊢ (2 \in ℂ \land Q \in ℂ \land R \in ℂ) \to 2 + Q + R = Q + R + 2$
24	12 15 18 23	syl3anc	$⊢ (Q \in ℙ \land R \in ℙ) \to 2 + Q + R = Q + R + 2$
25	24	eqeq2d	$⊢ (Q \in ℙ \land R \in ℙ) \to (N + 2 = 2 + Q + R \leftrightarrow N + 2 = Q + R + 2)$
26	25	adantr	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = 2 + Q + R \leftrightarrow N + 2 = Q + R + 2)$
27		evenz	$⊢ N \in Even \to N \in ℤ$
28	27	zcnd	$⊢ N \in Even \to N \in ℂ$
29	28	adantl	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to N \in ℂ$
30		zaddcl	$⊢ (Q \in ℤ \land R \in ℤ) \to Q + R \in ℤ$
31	13 16 30	syl2an	$⊢ (Q \in ℙ \land R \in ℙ) \to Q + R \in ℤ$
32	31	zcnd	$⊢ (Q \in ℙ \land R \in ℙ) \to Q + R \in ℂ$
33	32	adantr	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to Q + R \in ℂ$
34		2cnd	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to 2 \in ℂ$
35	29 33 34	addcan2d	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = Q + R + 2 \leftrightarrow N = Q + R)$
36	26 35	bitrd	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = 2 + Q + R \leftrightarrow N = Q + R)$
37		simpll	$⊢ ((Q \in ℙ \land R \in ℙ) \land N = Q + R) \to Q \in ℙ$
38		oveq1	$⊢ p = Q \to p + q = Q + q$
39	38	eqeq2d	$⊢ p = Q \to (N = p + q \leftrightarrow N = Q + q)$
40	39	rexbidv	$⊢ p = Q \to (\exists q \in ℙ N = p + q \leftrightarrow \exists q \in ℙ N = Q + q)$
41	40	adantl	$⊢ (((Q \in ℙ \land R \in ℙ) \land N = Q + R) \land p = Q) \to (\exists q \in ℙ N = p + q \leftrightarrow \exists q \in ℙ N = Q + q)$
42		simplr	$⊢ ((Q \in ℙ \land R \in ℙ) \land N = Q + R) \to R \in ℙ$
43		simpr	$⊢ ((Q \in ℙ \land R \in ℙ) \land N = Q + R) \to N = Q + R$
44		oveq2	$⊢ q = R \to Q + q = Q + R$
45	44	eqcomd	$⊢ q = R \to Q + R = Q + q$
46	43 45	sylan9eq	$⊢ (((Q \in ℙ \land R \in ℙ) \land N = Q + R) \land q = R) \to N = Q + q$
47	42 46	rspcedeq2vd	$⊢ ((Q \in ℙ \land R \in ℙ) \land N = Q + R) \to \exists q \in ℙ N = Q + q$
48	37 41 47	rspcedvd	$⊢ ((Q \in ℙ \land R \in ℙ) \land N = Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q$
49	48	ex	$⊢ (Q \in ℙ \land R \in ℙ) \to (N = Q + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
50	49	adantr	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N = Q + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
51	36 50	sylbid	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = 2 + Q + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
52	51	com12	$⊢ N + 2 = 2 + Q + R \to (((Q \in ℙ \land R \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
53	11 52	biimtrdi	$⊢ P = 2 \to (N + 2 = P + Q + R \to (((Q \in ℙ \land R \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
54	53	com13	$⊢ ((Q \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + Q + R \to (P = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
55	54	ex	$⊢ (Q \in ℙ \land R \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (P = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
56	55	3adant1	$⊢ (P \in ℙ \land Q \in ℙ \land R \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (P = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
57	56	3imp	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to (P = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
58	57	com12	$⊢ P = 2 \to (((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
59		oveq2	$⊢ Q = 2 \to P + Q = P + 2$
60	59	oveq1d	$⊢ Q = 2 \to P + Q + R = P + 2 + R$
61	60	eqeq2d	$⊢ Q = 2 \to (N + 2 = P + Q + R \leftrightarrow N + 2 = P + 2 + R)$
62		prmz	$⊢ P \in ℙ \to P \in ℤ$
63	62	zcnd	$⊢ P \in ℙ \to P \in ℂ$
64	63	adantr	$⊢ (P \in ℙ \land R \in ℙ) \to P \in ℂ$
65		2cnd	$⊢ (P \in ℙ \land R \in ℙ) \to 2 \in ℂ$
66	17	adantl	$⊢ (P \in ℙ \land R \in ℙ) \to R \in ℂ$
67	64 65 66	3jca	$⊢ (P \in ℙ \land R \in ℙ) \to (P \in ℂ \land 2 \in ℂ \land R \in ℂ)$
68	67	adantr	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (P \in ℂ \land 2 \in ℂ \land R \in ℂ)$
69		add32	$⊢ (P \in ℂ \land 2 \in ℂ \land R \in ℂ) \to P + 2 + R = P + R + 2$
70	68 69	syl	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to P + 2 + R = P + R + 2$
71	70	eqeq2d	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + 2 + R \leftrightarrow N + 2 = P + R + 2)$
72	28	adantl	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to N \in ℂ$
73		zaddcl	$⊢ (P \in ℤ \land R \in ℤ) \to P + R \in ℤ$
74	62 16 73	syl2an	$⊢ (P \in ℙ \land R \in ℙ) \to P + R \in ℤ$
75	74	zcnd	$⊢ (P \in ℙ \land R \in ℙ) \to P + R \in ℂ$
76	75	adantr	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to P + R \in ℂ$
77		2cnd	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to 2 \in ℂ$
78	72 76 77	addcan2d	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + R + 2 \leftrightarrow N = P + R)$
79	71 78	bitrd	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + 2 + R \leftrightarrow N = P + R)$
80		simpll	$⊢ ((P \in ℙ \land R \in ℙ) \land N = P + R) \to P \in ℙ$
81		oveq1	$⊢ p = P \to p + q = P + q$
82	81	eqeq2d	$⊢ p = P \to (N = p + q \leftrightarrow N = P + q)$
83	82	rexbidv	$⊢ p = P \to (\exists q \in ℙ N = p + q \leftrightarrow \exists q \in ℙ N = P + q)$
84	83	adantl	$⊢ (((P \in ℙ \land R \in ℙ) \land N = P + R) \land p = P) \to (\exists q \in ℙ N = p + q \leftrightarrow \exists q \in ℙ N = P + q)$
85		simplr	$⊢ ((P \in ℙ \land R \in ℙ) \land N = P + R) \to R \in ℙ$
86		simpr	$⊢ ((P \in ℙ \land R \in ℙ) \land N = P + R) \to N = P + R$
87		oveq2	$⊢ q = R \to P + q = P + R$
88	87	eqcomd	$⊢ q = R \to P + R = P + q$
89	86 88	sylan9eq	$⊢ (((P \in ℙ \land R \in ℙ) \land N = P + R) \land q = R) \to N = P + q$
90	85 89	rspcedeq2vd	$⊢ ((P \in ℙ \land R \in ℙ) \land N = P + R) \to \exists q \in ℙ N = P + q$
91	80 84 90	rspcedvd	$⊢ ((P \in ℙ \land R \in ℙ) \land N = P + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q$
92	91	ex	$⊢ (P \in ℙ \land R \in ℙ) \to (N = P + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
93	92	adantr	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N = P + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
94	79 93	sylbid	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + 2 + R \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
95	94	com12	$⊢ N + 2 = P + 2 + R \to (((P \in ℙ \land R \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
96	61 95	biimtrdi	$⊢ Q = 2 \to (N + 2 = P + Q + R \to (((P \in ℙ \land R \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
97	96	com13	$⊢ ((P \in ℙ \land R \in ℙ) \land N \in Even) \to (N + 2 = P + Q + R \to (Q = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
98	97	ex	$⊢ (P \in ℙ \land R \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (Q = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
99	98	3adant2	$⊢ (P \in ℙ \land Q \in ℙ \land R \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (Q = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
100	99	3imp	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to (Q = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
101	100	com12	$⊢ Q = 2 \to (((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
102		oveq2	$⊢ R = 2 \to P + Q + R = P + Q + 2$
103	102	eqeq2d	$⊢ R = 2 \to (N + 2 = P + Q + R \leftrightarrow N + 2 = P + Q + 2)$
104	28	adantl	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to N \in ℂ$
105		zaddcl	$⊢ (P \in ℤ \land Q \in ℤ) \to P + Q \in ℤ$
106	62 13 105	syl2an	$⊢ (P \in ℙ \land Q \in ℙ) \to P + Q \in ℤ$
107	106	zcnd	$⊢ (P \in ℙ \land Q \in ℙ) \to P + Q \in ℂ$
108	107	adantr	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to P + Q \in ℂ$
109		2cnd	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to 2 \in ℂ$
110	104 108 109	addcan2d	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to (N + 2 = P + Q + 2 \leftrightarrow N = P + Q)$
111		simpll	$⊢ ((P \in ℙ \land Q \in ℙ) \land N = P + Q) \to P \in ℙ$
112	83	adantl	$⊢ (((P \in ℙ \land Q \in ℙ) \land N = P + Q) \land p = P) \to (\exists q \in ℙ N = p + q \leftrightarrow \exists q \in ℙ N = P + q)$
113		simplr	$⊢ ((P \in ℙ \land Q \in ℙ) \land N = P + Q) \to Q \in ℙ$
114		simpr	$⊢ ((P \in ℙ \land Q \in ℙ) \land N = P + Q) \to N = P + Q$
115		oveq2	$⊢ q = Q \to P + q = P + Q$
116	115	eqcomd	$⊢ q = Q \to P + Q = P + q$
117	114 116	sylan9eq	$⊢ (((P \in ℙ \land Q \in ℙ) \land N = P + Q) \land q = Q) \to N = P + q$
118	113 117	rspcedeq2vd	$⊢ ((P \in ℙ \land Q \in ℙ) \land N = P + Q) \to \exists q \in ℙ N = P + q$
119	111 112 118	rspcedvd	$⊢ ((P \in ℙ \land Q \in ℙ) \land N = P + Q) \to \exists p \in ℙ \exists q \in ℙ N = p + q$
120	119	ex	$⊢ (P \in ℙ \land Q \in ℙ) \to (N = P + Q \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
121	120	adantr	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to (N = P + Q \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
122	110 121	sylbid	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to (N + 2 = P + Q + 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
123	122	com12	$⊢ N + 2 = P + Q + 2 \to (((P \in ℙ \land Q \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
124	103 123	biimtrdi	$⊢ R = 2 \to (N + 2 = P + Q + R \to (((P \in ℙ \land Q \in ℙ) \land N \in Even) \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
125	124	com13	$⊢ ((P \in ℙ \land Q \in ℙ) \land N \in Even) \to (N + 2 = P + Q + R \to (R = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q))$
126	125	ex	$⊢ (P \in ℙ \land Q \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (R = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
127	126	3adant3	$⊢ (P \in ℙ \land Q \in ℙ \land R \in ℙ) \to (N \in Even \to (N + 2 = P + Q + R \to (R = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)))$
128	127	3imp	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to (R = 2 \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
129	128	com12	$⊢ R = 2 \to (((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
130	58 101 129	3jaoi	$⊢ (P = 2 \lor Q = 2 \lor R = 2) \to (((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q)$
131	8 130	mpcom	$⊢ ((P \in ℙ \land Q \in ℙ \land R \in ℙ) \land N \in Even \land N + 2 = P + Q + R) \to \exists p \in ℙ \exists q \in ℙ N = p + q$

Metamath Proof Explorer

Theorem mogoldbblem

Proof