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