Metamath Proof Explorer

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 e. CC
2 3cn 
 |-  3 e. CC
3 5p3e8 
 |-  ( 5 + 3 ) = 8
4 1 2 3 addcomli 
 |-  ( 3 + 5 ) = 8
5 4 eqcomi 
 |-  8 = ( 3 + 5 )