Metamath Proof Explorer
Description: 7 + 3 = 10. (Contributed by NM, 5-Feb-2007) (Revised by Stanislas Polu, 7-Apr-2020) (Revised by AV, 6-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
7p3e10 |
⊢ ( 7 + 3 ) = ; 1 0 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
df-3 |
⊢ 3 = ( 2 + 1 ) |
2 |
1
|
oveq2i |
⊢ ( 7 + 3 ) = ( 7 + ( 2 + 1 ) ) |
3 |
|
7cn |
⊢ 7 ∈ ℂ |
4 |
|
2cn |
⊢ 2 ∈ ℂ |
5 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
6 |
3 4 5
|
addassi |
⊢ ( ( 7 + 2 ) + 1 ) = ( 7 + ( 2 + 1 ) ) |
7 |
2 6
|
eqtr4i |
⊢ ( 7 + 3 ) = ( ( 7 + 2 ) + 1 ) |
8 |
|
7p2e9 |
⊢ ( 7 + 2 ) = 9 |
9 |
8
|
oveq1i |
⊢ ( ( 7 + 2 ) + 1 ) = ( 9 + 1 ) |
10 |
|
9p1e10 |
⊢ ( 9 + 1 ) = ; 1 0 |
11 |
7 9 10
|
3eqtri |
⊢ ( 7 + 3 ) = ; 1 0 |