Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension 2)
Goldbach's conjectures
gboodd
Next ⟩
gbepos
Metamath Proof Explorer
Ascii
Unicode
Theorem
gboodd
Description:
An odd Goldbach number is odd.
(Contributed by
AV
, 26-Jul-2020)
Ref
Expression
Assertion
gboodd
⊢
Z
∈
GoldbachOdd
→
Z
∈
Odd
Proof
Step
Hyp
Ref
Expression
1
gbogbow
⊢
Z
∈
GoldbachOdd
→
Z
∈
GoldbachOddW
2
gbowodd
⊢
Z
∈
GoldbachOddW
→
Z
∈
Odd
3
1
2
syl
⊢
Z
∈
GoldbachOdd
→
Z
∈
Odd