Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension 2)
Goldbach's conjectures
gbpart8
Next ⟩
gbpart9
Metamath Proof Explorer
Ascii
Unicode
Theorem
gbpart8
Description:
The Goldbach partition of 8.
(Contributed by
AV
, 20-Jul-2020)
Ref
Expression
Assertion
gbpart8
⊢
8
=
3
+
5
Proof
Step
Hyp
Ref
Expression
1
5cn
⊢
5
∈
ℂ
2
3cn
⊢
3
∈
ℂ
3
5p3e8
⊢
5
+
3
=
8
4
1
2
3
addcomli
⊢
3
+
5
=
8
5
4
eqcomi
⊢
8
=
3
+
5