sbgoldbalt

Description: An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020)

		Ref	Expression
	Assertion	sbgoldbalt	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \leftrightarrow \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		evenz	$⊢ n \in Even \to n \in ℤ$
3		zltp1le	$⊢ (2 \in ℤ \land n \in ℤ) \to (2 < n \leftrightarrow 2 + 1 \leq n)$
4	1 2 3	sylancr	$⊢ n \in Even \to (2 < n \leftrightarrow 2 + 1 \leq n)$
5		2p1e3	$⊢ 2 + 1 = 3$
6	5	breq1i	$⊢ 2 + 1 \leq n \leftrightarrow 3 \leq n$
7		3re	$⊢ 3 \in ℝ$
8	7	a1i	$⊢ n \in Even \to 3 \in ℝ$
9	2	zred	$⊢ n \in Even \to n \in ℝ$
10	8 9	leloed	$⊢ n \in Even \to (3 \leq n \leftrightarrow (3 < n \lor 3 = n))$
11		3z	$⊢ 3 \in ℤ$
12		zltp1le	$⊢ (3 \in ℤ \land n \in ℤ) \to (3 < n \leftrightarrow 3 + 1 \leq n)$
13	11 2 12	sylancr	$⊢ n \in Even \to (3 < n \leftrightarrow 3 + 1 \leq n)$
14		3p1e4	$⊢ 3 + 1 = 4$
15	14	breq1i	$⊢ 3 + 1 \leq n \leftrightarrow 4 \leq n$
16		4re	$⊢ 4 \in ℝ$
17	16	a1i	$⊢ n \in Even \to 4 \in ℝ$
18	17 9	leloed	$⊢ n \in Even \to (4 \leq n \leftrightarrow (4 < n \lor 4 = n))$
19		pm3.35	$⊢ (4 < n \land (4 < n \to n \in GoldbachEven)) \to n \in GoldbachEven$
20		isgbe	$⊢ n \in GoldbachEven \leftrightarrow (n \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q))$
21		simp3	$⊢ (p \in Odd \land q \in Odd \land n = p + q) \to n = p + q$
22	21	a1i	$⊢ ((n \in Even \land p \in ℙ) \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land n = p + q) \to n = p + q)$
23	22	reximdva	$⊢ (n \in Even \land p \in ℙ) \to (\exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q) \to \exists q \in ℙ n = p + q)$
24	23	reximdva	$⊢ n \in Even \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q) \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
25	24	imp	$⊢ (n \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q)) \to \exists p \in ℙ \exists q \in ℙ n = p + q$
26	20 25	sylbi	$⊢ n \in GoldbachEven \to \exists p \in ℙ \exists q \in ℙ n = p + q$
27	26	a1d	$⊢ n \in GoldbachEven \to (n \in Even \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
28	19 27	syl	$⊢ (4 < n \land (4 < n \to n \in GoldbachEven)) \to (n \in Even \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
29	28	ex	$⊢ 4 < n \to ((4 < n \to n \in GoldbachEven) \to (n \in Even \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
30	29	com23	$⊢ 4 < n \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
31		2prm	$⊢ 2 \in ℙ$
32		2p2e4	$⊢ 2 + 2 = 4$
33	32	eqcomi	$⊢ 4 = 2 + 2$
34		rspceov	$⊢ (2 \in ℙ \land 2 \in ℙ \land 4 = 2 + 2) \to \exists p \in ℙ \exists q \in ℙ 4 = p + q$
35	31 31 33 34	mp3an	$⊢ \exists p \in ℙ \exists q \in ℙ 4 = p + q$
36		eqeq1	$⊢ 4 = n \to (4 = p + q \leftrightarrow n = p + q)$
37	36	2rexbidv	$⊢ 4 = n \to (\exists p \in ℙ \exists q \in ℙ 4 = p + q \leftrightarrow \exists p \in ℙ \exists q \in ℙ n = p + q)$
38	35 37	mpbii	$⊢ 4 = n \to \exists p \in ℙ \exists q \in ℙ n = p + q$
39	38	a1d	$⊢ 4 = n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
40	39	a1d	$⊢ 4 = n \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
41	30 40	jaoi	$⊢ (4 < n \lor 4 = n) \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
42	41	com12	$⊢ n \in Even \to ((4 < n \lor 4 = n) \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
43	18 42	sylbid	$⊢ n \in Even \to (4 \leq n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
44	15 43	biimtrid	$⊢ n \in Even \to (3 + 1 \leq n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
45	13 44	sylbid	$⊢ n \in Even \to (3 < n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
46	45	com12	$⊢ 3 < n \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
47		3odd	$⊢ 3 \in Odd$
48		eleq1	$⊢ 3 = n \to (3 \in Odd \leftrightarrow n \in Odd)$
49	47 48	mpbii	$⊢ 3 = n \to n \in Odd$
50		oddneven	$⊢ n \in Odd \to \neg n \in Even$
51	49 50	syl	$⊢ 3 = n \to \neg n \in Even$
52	51	pm2.21d	$⊢ 3 = n \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
53	46 52	jaoi	$⊢ (3 < n \lor 3 = n) \to (n \in Even \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
54	53	com12	$⊢ n \in Even \to ((3 < n \lor 3 = n) \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
55	10 54	sylbid	$⊢ n \in Even \to (3 \leq n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
56	6 55	biimtrid	$⊢ n \in Even \to (2 + 1 \leq n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
57	4 56	sylbid	$⊢ n \in Even \to (2 < n \to ((4 < n \to n \in GoldbachEven) \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
58	57	com23	$⊢ n \in Even \to ((4 < n \to n \in GoldbachEven) \to (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
59		2lt4	$⊢ 2 < 4$
60		2re	$⊢ 2 \in ℝ$
61	60	a1i	$⊢ n \in Even \to 2 \in ℝ$
62		lttr	$⊢ (2 \in ℝ \land 4 \in ℝ \land n \in ℝ) \to ((2 < 4 \land 4 < n) \to 2 < n)$
63	61 17 9 62	syl3anc	$⊢ n \in Even \to ((2 < 4 \land 4 < n) \to 2 < n)$
64	59 63	mpani	$⊢ n \in Even \to (4 < n \to 2 < n)$
65	64	imp	$⊢ (n \in Even \land 4 < n) \to 2 < n$
66		simpll	$⊢ ((n \in Even \land 4 < n) \land \exists p \in ℙ \exists q \in ℙ n = p + q) \to n \in Even$
67		simpr	$⊢ ((n \in Even \land 4 < n) \land p \in ℙ) \to p \in ℙ$
68	67	anim1i	$⊢ (((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \to (p \in ℙ \land q \in ℙ)$
69	68	adantr	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to (p \in ℙ \land q \in ℙ)$
70		simpll	$⊢ (((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \to (n \in Even \land 4 < n)$
71	70	anim1i	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to ((n \in Even \land 4 < n) \land n = p + q)$
72		df-3an	$⊢ (n \in Even \land 4 < n \land n = p + q) \leftrightarrow ((n \in Even \land 4 < n) \land n = p + q)$
73	71 72	sylibr	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to (n \in Even \land 4 < n \land n = p + q)$
74		sbgoldbaltlem2	$⊢ (p \in ℙ \land q \in ℙ) \to ((n \in Even \land 4 < n \land n = p + q) \to (p \in Odd \land q \in Odd))$
75	69 73 74	sylc	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to (p \in Odd \land q \in Odd)$
76		simpr	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to n = p + q$
77		df-3an	$⊢ (p \in Odd \land q \in Odd \land n = p + q) \leftrightarrow ((p \in Odd \land q \in Odd) \land n = p + q)$
78	75 76 77	sylanbrc	$⊢ ((((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \land n = p + q) \to (p \in Odd \land q \in Odd \land n = p + q)$
79	78	ex	$⊢ (((n \in Even \land 4 < n) \land p \in ℙ) \land q \in ℙ) \to (n = p + q \to (p \in Odd \land q \in Odd \land n = p + q))$
80	79	reximdva	$⊢ ((n \in Even \land 4 < n) \land p \in ℙ) \to (\exists q \in ℙ n = p + q \to \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q))$
81	80	reximdva	$⊢ (n \in Even \land 4 < n) \to (\exists p \in ℙ \exists q \in ℙ n = p + q \to \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q))$
82	81	imp	$⊢ ((n \in Even \land 4 < n) \land \exists p \in ℙ \exists q \in ℙ n = p + q) \to \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q)$
83	66 82	jca	$⊢ ((n \in Even \land 4 < n) \land \exists p \in ℙ \exists q \in ℙ n = p + q) \to (n \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q))$
84	83	ex	$⊢ (n \in Even \land 4 < n) \to (\exists p \in ℙ \exists q \in ℙ n = p + q \to (n \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land n = p + q)))$
85	84 20	imbitrrdi	$⊢ (n \in Even \land 4 < n) \to (\exists p \in ℙ \exists q \in ℙ n = p + q \to n \in GoldbachEven)$
86	65 85	embantd	$⊢ (n \in Even \land 4 < n) \to ((2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q) \to n \in GoldbachEven)$
87	86	ex	$⊢ n \in Even \to (4 < n \to ((2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q) \to n \in GoldbachEven))$
88	87	com23	$⊢ n \in Even \to ((2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q) \to (4 < n \to n \in GoldbachEven))$
89	58 88	impbid	$⊢ n \in Even \to ((4 < n \to n \in GoldbachEven) \leftrightarrow (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
90	89	ralbiia	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \leftrightarrow \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$

Metamath Proof Explorer

Theorem sbgoldbalt

Proof