Metamath Proof Explorer


Theorem 2times

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 · 𝐴 ) = ( 𝐴 + 𝐴 ) )