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