Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension 2)
Goldbach's conjectures
gbowodd
Next ⟩
gbogbow
Metamath Proof Explorer
Ascii
Unicode
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