Description: The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | gbpart9 | |- 9 = ( ( 3 + 3 ) + 3 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3p3e6 | |- ( 3 + 3 ) = 6 |
|
2 | 1 | oveq1i | |- ( ( 3 + 3 ) + 3 ) = ( 6 + 3 ) |
3 | 6p3e9 | |- ( 6 + 3 ) = 9 |
|
4 | 2 3 | eqtr2i | |- 9 = ( ( 3 + 3 ) + 3 ) |