Metamath Proof Explorer


Theorem gbpart7

Description: The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbpart7 7=2+2+3

Proof

Step Hyp Ref Expression
1 2p2e4 2+2=4
2 1 oveq1i 2+2+3=4+3
3 4p3e7 4+3=7
4 2 3 eqtr2i 7=2+2+3