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