This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )