Theorem gbege6

Description: Any even Goldbach number is greater than or equal to 6. Because of 6gbe , this bound is strict. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	gbege6	$$⊢Z\in \mathrm{GoldbachEven}\to 6\le Z$$

Proof

Step	Hyp	Ref	Expression
1		gbepos	$$⊢Z\in \mathrm{GoldbachEven}\to Z\in \mathbb{N}$$
2		gbegt5	$$⊢Z\in \mathrm{GoldbachEven}\to 5<Z$$
3		5nn	$$⊢5\in \mathbb{N}$$
4	3	nnzi	$$⊢5\in \mathbb{Z}$$
5		nnz	$$⊢Z\in \mathbb{N}\to Z\in \mathbb{Z}$$
6		zltp1le	$$⊢\left(5\in \mathbb{Z}\wedge Z\in \mathbb{Z}\right)\to \left(5<Z\leftrightarrow 5+1\le Z\right)$$
7	4 5 6	sylancr	$$⊢Z\in \mathbb{N}\to \left(5<Z\leftrightarrow 5+1\le Z\right)$$
8	7	biimpd	$$⊢Z\in \mathbb{N}\to \left(5<Z\to 5+1\le Z\right)$$
9		5p1e6	$$⊢5+1=6$$
10	9	breq1i	$$⊢5+1\le Z\leftrightarrow 6\le Z$$
11	8 10	imbitrdi	$$⊢Z\in \mathbb{N}\to \left(5<Z\to 6\le Z\right)$$
12	1 2 11	sylc	$$⊢Z\in \mathrm{GoldbachEven}\to 6\le Z$$