This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: 8 + 2 = 10. (Contributed by NM, 5-Feb-2007) (Revised by Stanislas Polu, 7-Apr-2020) (Revised by AV, 6-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
8p2e10 |
⊢ ( 8 + 2 ) = ; 1 0 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 2 |
1
|
oveq2i |
⊢ ( 8 + 2 ) = ( 8 + ( 1 + 1 ) ) |
| 3 |
|
8cn |
⊢ 8 ∈ ℂ |
| 4 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 5 |
3 4 4
|
addassi |
⊢ ( ( 8 + 1 ) + 1 ) = ( 8 + ( 1 + 1 ) ) |
| 6 |
2 5
|
eqtr4i |
⊢ ( 8 + 2 ) = ( ( 8 + 1 ) + 1 ) |
| 7 |
|
df-9 |
⊢ 9 = ( 8 + 1 ) |
| 8 |
7
|
oveq1i |
⊢ ( 9 + 1 ) = ( ( 8 + 1 ) + 1 ) |
| 9 |
|
9p1e10 |
⊢ ( 9 + 1 ) = ; 1 0 |
| 10 |
6 8 9
|
3eqtr2i |
⊢ ( 8 + 2 ) = ; 1 0 |