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 e. GoldbachEven -> 6 <_ Z )

Proof

Step	Hyp	Ref	Expression
1		gbepos	|- ( Z e. GoldbachEven -> Z e. NN )
2		gbegt5	|- ( Z e. GoldbachEven -> 5 < Z )
3		5nn	|- 5 e. NN
4	3	nnzi	|- 5 e. ZZ
5		nnz	|- ( Z e. NN -> Z e. ZZ )
6		zltp1le	|- ( ( 5 e. ZZ /\ Z e. ZZ ) -> ( 5 < Z <-> ( 5 + 1 ) <_ Z ) )
7	4 5 6	sylancr	|- ( Z e. NN -> ( 5 < Z <-> ( 5 + 1 ) <_ Z ) )
8	7	biimpd	|- ( Z e. NN -> ( 5 < Z -> ( 5 + 1 ) <_ Z ) )
9		5p1e6	|- ( 5 + 1 ) = 6
10	9	breq1i	|- ( ( 5 + 1 ) <_ Z <-> 6 <_ Z )
11	8 10	imbitrdi	|- ( Z e. NN -> ( 5 < Z -> 6 <_ Z ) )
12	1 2 11	sylc	|- ( Z e. GoldbachEven -> 6 <_ Z )