Metamath Proof Explorer


Theorem gbopos

Description: Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gbopos
|- ( Z e. GoldbachOdd -> Z e. NN )

Proof

Step Hyp Ref Expression
1 gbogbow
 |-  ( Z e. GoldbachOdd -> Z e. GoldbachOddW )
2 gbowpos
 |-  ( Z e. GoldbachOddW -> Z e. NN )
3 1 2 syl
 |-  ( Z e. GoldbachOdd -> Z e. NN )