Metamath Proof Explorer


Theorem gbeeven

Description: An even Goldbach number is even. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion gbeeven Z GoldbachEven Z Even

Proof

Step Hyp Ref Expression
1 isgbe Z GoldbachEven Z Even p q p Odd q Odd Z = p + q
2 1 simplbi Z GoldbachEven Z Even