gbegt5

Description: Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020)

		Ref	Expression
	Assertion	gbegt5	$⊢ Z \in GoldbachEven \to 5 < Z$

Proof

Step	Hyp	Ref	Expression
1		isgbe	$⊢ Z \in GoldbachEven \leftrightarrow (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q))$
2		oddprmuzge3	$⊢ (p \in ℙ \land p \in Odd) \to p \in ℤ_{\geq 3}$
3	2	ancoms	$⊢ (p \in Odd \land p \in ℙ) \to p \in ℤ_{\geq 3}$
4		oddprmuzge3	$⊢ (q \in ℙ \land q \in Odd) \to q \in ℤ_{\geq 3}$
5	4	ancoms	$⊢ (q \in Odd \land q \in ℙ) \to q \in ℤ_{\geq 3}$
6		eluz2	$⊢ p \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land p \in ℤ \land 3 \leq p)$
7		eluz2	$⊢ q \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land q \in ℤ \land 3 \leq q)$
8		zre	$⊢ q \in ℤ \to q \in ℝ$
9		zre	$⊢ p \in ℤ \to p \in ℝ$
10		3re	$⊢ 3 \in ℝ$
11	10 10	pm3.2i	$⊢ (3 \in ℝ \land 3 \in ℝ)$
12		pm3.22	$⊢ (q \in ℝ \land p \in ℝ) \to (p \in ℝ \land q \in ℝ)$
13		le2add	$⊢ ((3 \in ℝ \land 3 \in ℝ) \land (p \in ℝ \land q \in ℝ)) \to ((3 \leq p \land 3 \leq q) \to 3 + 3 \leq p + q)$
14	11 12 13	sylancr	$⊢ (q \in ℝ \land p \in ℝ) \to ((3 \leq p \land 3 \leq q) \to 3 + 3 \leq p + q)$
15	14	ancomsd	$⊢ (q \in ℝ \land p \in ℝ) \to ((3 \leq q \land 3 \leq p) \to 3 + 3 \leq p + q)$
16		3p3e6	$⊢ 3 + 3 = 6$
17	16	breq1i	$⊢ 3 + 3 \leq p + q \leftrightarrow 6 \leq p + q$
18		5lt6	$⊢ 5 < 6$
19		5re	$⊢ 5 \in ℝ$
20	19	a1i	$⊢ (q \in ℝ \land p \in ℝ) \to 5 \in ℝ$
21		6re	$⊢ 6 \in ℝ$
22	21	a1i	$⊢ (q \in ℝ \land p \in ℝ) \to 6 \in ℝ$
23		readdcl	$⊢ (p \in ℝ \land q \in ℝ) \to p + q \in ℝ$
24	23	ancoms	$⊢ (q \in ℝ \land p \in ℝ) \to p + q \in ℝ$
25		ltletr	$⊢ (5 \in ℝ \land 6 \in ℝ \land p + q \in ℝ) \to ((5 < 6 \land 6 \leq p + q) \to 5 < p + q)$
26	20 22 24 25	syl3anc	$⊢ (q \in ℝ \land p \in ℝ) \to ((5 < 6 \land 6 \leq p + q) \to 5 < p + q)$
27	18 26	mpani	$⊢ (q \in ℝ \land p \in ℝ) \to (6 \leq p + q \to 5 < p + q)$
28	17 27	biimtrid	$⊢ (q \in ℝ \land p \in ℝ) \to (3 + 3 \leq p + q \to 5 < p + q)$
29	15 28	syld	$⊢ (q \in ℝ \land p \in ℝ) \to ((3 \leq q \land 3 \leq p) \to 5 < p + q)$
30	8 9 29	syl2an	$⊢ (q \in ℤ \land p \in ℤ) \to ((3 \leq q \land 3 \leq p) \to 5 < p + q)$
31	30	ex	$⊢ q \in ℤ \to (p \in ℤ \to ((3 \leq q \land 3 \leq p) \to 5 < p + q))$
32	31	adantl	$⊢ (3 \in ℤ \land q \in ℤ) \to (p \in ℤ \to ((3 \leq q \land 3 \leq p) \to 5 < p + q))$
33	32	com23	$⊢ (3 \in ℤ \land q \in ℤ) \to ((3 \leq q \land 3 \leq p) \to (p \in ℤ \to 5 < p + q))$
34	33	exp4b	$⊢ 3 \in ℤ \to (q \in ℤ \to (3 \leq q \to (3 \leq p \to (p \in ℤ \to 5 < p + q))))$
35	34	3imp	$⊢ (3 \in ℤ \land q \in ℤ \land 3 \leq q) \to (3 \leq p \to (p \in ℤ \to 5 < p + q))$
36	35	com13	$⊢ p \in ℤ \to (3 \leq p \to ((3 \in ℤ \land q \in ℤ \land 3 \leq q) \to 5 < p + q))$
37	36	imp	$⊢ (p \in ℤ \land 3 \leq p) \to ((3 \in ℤ \land q \in ℤ \land 3 \leq q) \to 5 < p + q)$
38	37	3adant1	$⊢ (3 \in ℤ \land p \in ℤ \land 3 \leq p) \to ((3 \in ℤ \land q \in ℤ \land 3 \leq q) \to 5 < p + q)$
39	7 38	biimtrid	$⊢ (3 \in ℤ \land p \in ℤ \land 3 \leq p) \to (q \in ℤ_{\geq 3} \to 5 < p + q)$
40	6 39	sylbi	$⊢ p \in ℤ_{\geq 3} \to (q \in ℤ_{\geq 3} \to 5 < p + q)$
41	40	imp	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to 5 < p + q$
42	3 5 41	syl2an	$⊢ ((p \in Odd \land p \in ℙ) \land (q \in Odd \land q \in ℙ)) \to 5 < p + q$
43	42	an4s	$⊢ ((p \in Odd \land q \in Odd) \land (p \in ℙ \land q \in ℙ)) \to 5 < p + q$
44	43	ex	$⊢ (p \in Odd \land q \in Odd) \to ((p \in ℙ \land q \in ℙ) \to 5 < p + q)$
45	44	3adant3	$⊢ (p \in Odd \land q \in Odd \land Z = p + q) \to ((p \in ℙ \land q \in ℙ) \to 5 < p + q)$
46	45	impcom	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land Z = p + q)) \to 5 < p + q$
47		breq2	$⊢ Z = p + q \to (5 < Z \leftrightarrow 5 < p + q)$
48	47	3ad2ant3	$⊢ (p \in Odd \land q \in Odd \land Z = p + q) \to (5 < Z \leftrightarrow 5 < p + q)$
49	48	adantl	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land Z = p + q)) \to (5 < Z \leftrightarrow 5 < p + q)$
50	46 49	mpbird	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land Z = p + q)) \to 5 < Z$
51	50	ex	$⊢ (p \in ℙ \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land Z = p + q) \to 5 < Z)$
52	51	a1i	$⊢ Z \in Even \to ((p \in ℙ \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land Z = p + q) \to 5 < Z))$
53	52	rexlimdvv	$⊢ Z \in Even \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q) \to 5 < Z)$
54	53	imp	$⊢ (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q)) \to 5 < Z$
55	1 54	sylbi	$⊢ Z \in GoldbachEven \to 5 < Z$

Metamath Proof Explorer

Theorem gbegt5

Proof