gboge9

Description: Any odd Goldbach number is greater than or equal to 9. Because of 9gbo , this bound is strict. (Contributed by AV, 26-Jul-2020)

		Ref	Expression
	Assertion	gboge9	$⊢ Z \in GoldbachOdd \to 9 \leq Z$

Proof

Step	Hyp	Ref	Expression
1		isgbo	$⊢ Z \in GoldbachOdd \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$
2		df-3an	$⊢ (p \in ℙ \land q \in ℙ \land r \in ℙ) \leftrightarrow ((p \in ℙ \land q \in ℙ) \land r \in ℙ)$
3		an6	$⊢ ((p \in ℙ \land q \in ℙ \land r \in ℙ) \land (p \in Odd \land q \in Odd \land r \in Odd)) \leftrightarrow ((p \in ℙ \land p \in Odd) \land (q \in ℙ \land q \in Odd) \land (r \in ℙ \land r \in Odd))$
4		oddprmuzge3	$⊢ (p \in ℙ \land p \in Odd) \to p \in ℤ_{\geq 3}$
5		oddprmuzge3	$⊢ (q \in ℙ \land q \in Odd) \to q \in ℤ_{\geq 3}$
6		oddprmuzge3	$⊢ (r \in ℙ \land r \in Odd) \to r \in ℤ_{\geq 3}$
7		6p3e9	$⊢ 6 + 3 = 9$
8		eluzelz	$⊢ p \in ℤ_{\geq 3} \to p \in ℤ$
9		eluzelz	$⊢ q \in ℤ_{\geq 3} \to q \in ℤ$
10		zaddcl	$⊢ (p \in ℤ \land q \in ℤ) \to p + q \in ℤ$
11	8 9 10	syl2an	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to p + q \in ℤ$
12	11	zred	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to p + q \in ℝ$
13		eluzelre	$⊢ r \in ℤ_{\geq 3} \to r \in ℝ$
14	12 13	anim12i	$⊢ ((p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \land r \in ℤ_{\geq 3}) \to (p + q \in ℝ \land r \in ℝ)$
15	14	3impa	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to (p + q \in ℝ \land r \in ℝ)$
16		6re	$⊢ 6 \in ℝ$
17		3re	$⊢ 3 \in ℝ$
18	16 17	pm3.2i	$⊢ (6 \in ℝ \land 3 \in ℝ)$
19	15 18	jctil	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to ((6 \in ℝ \land 3 \in ℝ) \land (p + q \in ℝ \land r \in ℝ))$
20		3p3e6	$⊢ 3 + 3 = 6$
21		eluzelre	$⊢ p \in ℤ_{\geq 3} \to p \in ℝ$
22		eluzelre	$⊢ q \in ℤ_{\geq 3} \to q \in ℝ$
23	21 22	anim12i	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to (p \in ℝ \land q \in ℝ)$
24	17 17	pm3.2i	$⊢ (3 \in ℝ \land 3 \in ℝ)$
25	23 24	jctil	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to ((3 \in ℝ \land 3 \in ℝ) \land (p \in ℝ \land q \in ℝ))$
26		eluzle	$⊢ p \in ℤ_{\geq 3} \to 3 \leq p$
27		eluzle	$⊢ q \in ℤ_{\geq 3} \to 3 \leq q$
28	26 27	anim12i	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to (3 \leq p \land 3 \leq q)$
29		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)$
30	25 28 29	sylc	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to 3 + 3 \leq p + q$
31	20 30	eqbrtrrid	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3}) \to 6 \leq p + q$
32	31	3adant3	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to 6 \leq p + q$
33		eluzle	$⊢ r \in ℤ_{\geq 3} \to 3 \leq r$
34	33	3ad2ant3	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to 3 \leq r$
35	32 34	jca	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to (6 \leq p + q \land 3 \leq r)$
36		le2add	$⊢ ((6 \in ℝ \land 3 \in ℝ) \land (p + q \in ℝ \land r \in ℝ)) \to ((6 \leq p + q \land 3 \leq r) \to 6 + 3 \leq p + q + r)$
37	19 35 36	sylc	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to 6 + 3 \leq p + q + r$
38	7 37	eqbrtrrid	$⊢ (p \in ℤ_{\geq 3} \land q \in ℤ_{\geq 3} \land r \in ℤ_{\geq 3}) \to 9 \leq p + q + r$
39	4 5 6 38	syl3an	$⊢ ((p \in ℙ \land p \in Odd) \land (q \in ℙ \land q \in Odd) \land (r \in ℙ \land r \in Odd)) \to 9 \leq p + q + r$
40	3 39	sylbi	$⊢ ((p \in ℙ \land q \in ℙ \land r \in ℙ) \land (p \in Odd \land q \in Odd \land r \in Odd)) \to 9 \leq p + q + r$
41	2 40	sylanbr	$⊢ (((p \in ℙ \land q \in ℙ) \land r \in ℙ) \land (p \in Odd \land q \in Odd \land r \in Odd)) \to 9 \leq p + q + r$
42		breq2	$⊢ Z = p + q + r \to (9 \leq Z \leftrightarrow 9 \leq p + q + r)$
43	41 42	syl5ibrcom	$⊢ (((p \in ℙ \land q \in ℙ) \land r \in ℙ) \land (p \in Odd \land q \in Odd \land r \in Odd)) \to (Z = p + q + r \to 9 \leq Z)$
44	43	expimpd	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to 9 \leq Z)$
45	44	rexlimdva	$⊢ (p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to 9 \leq Z)$
46	45	a1i	$⊢ Z \in Odd \to ((p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to 9 \leq Z))$
47	46	rexlimdvv	$⊢ Z \in Odd \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to 9 \leq Z)$
48	47	imp	$⊢ (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r)) \to 9 \leq Z$
49	1 48	sylbi	$⊢ Z \in GoldbachOdd \to 9 \leq Z$

Metamath Proof Explorer

Theorem gboge9

Proof