Theorem 2times 12374

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.)

Assertion

Ref	Expression
2times	⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Proof of Theorem 2times

Step	Hyp	Ref	Expression
1		df-2 12301	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7413	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11404	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2782	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   + caddc 11130   · cmul 11132  2c2 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301

This theorem is referenced by:  times2  12375  2timesi  12376  2txmxeqx  12378  2halves  12457  halfaddsub  12472  avglt2  12478  2timesd  12482  expubnd  14194  absmax  15346  sinmul  16188  sin2t  16193  cos2t  16194  sadadd2lem2  16467  pythagtriplem4  16837  pythagtriplem14  16846  pythagtriplem16  16848  2sqreultlem  27408  2sqreunnltlem  27411  cncph  30746  pellexlem2  42800  acongrep  42951  sub2times  45249  2timesgt  45265  gpg3nbgrvtxlem  48017