Metamath Proof Explorer


Theorem gbpart11

Description: The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020)

Ref Expression
Assertion gbpart11 11 = 3 + 3 + 5

Proof

Step Hyp Ref Expression
1 3p3e6 3 + 3 = 6
2 1 oveq1i 3 + 3 + 5 = 6 + 5
3 6p5e11 6 + 5 = 11
4 2 3 eqtr2i 11 = 3 + 3 + 5