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 |