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 )