Metamath Proof Explorer


Theorem gbowodd

Description: A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion gbowodd ⊢ Z ∈ GoldbachOddW → Z ∈ Odd

Proof

Step Hyp Ref Expression
1 isgbow ⊢ Z ∈ GoldbachOddW ↔ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
2 1 simplbi ⊢ Z ∈ GoldbachOddW → Z ∈ Odd