Metamath Proof Explorer


Theorem gbopos

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

Ref Expression
Assertion gbopos ( 𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ )

Proof

Step Hyp Ref Expression
1 gbogbow ( 𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )
2 gbowpos ( 𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ )
3 1 2 syl ( 𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ )