This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Two times a number. (Contributed by NM, 10-Oct-2004) (Revised by Mario
Carneiro, 27-May-2016) (Proof shortened by AV, 26-Feb-2020)
|
|
Ref |
Expression |
|
Assertion |
2times |
⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 2 |
1
|
oveq1i |
⊢ ( 2 · 𝐴 ) = ( ( 1 + 1 ) · 𝐴 ) |
| 3 |
|
1p1times |
⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 1 ) · 𝐴 ) = ( 𝐴 + 𝐴 ) ) |
| 4 |
2 3
|
eqtrid |
⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) ) |