MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2times Structured version   Unicode version

Theorem 2times 10571
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  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )

Proof of Theorem 2times
StepHypRef Expression
1 df-2 10511 . . 3  |-  2  =  ( 1  +  1 )
21oveq1i 6206 . 2  |-  ( 2  x.  A )  =  ( ( 1  +  1 )  x.  A
)
3 1p1times 9662 . 2  |-  ( A  e.  CC  ->  (
( 1  +  1 )  x.  A )  =  ( A  +  A ) )
42, 3syl5eq 2435 1  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1826  (class class class)co 6196   CCcc 9401   1c1 9404    + caddc 9406    x. cmul 9408   2c2 10502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-mulcl 9465  ax-mulcom 9467  ax-mulass 9469  ax-distr 9470  ax-1rid 9473  ax-cnre 9476
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199  df-2 10511
This theorem is referenced by:  times2  10572  2timesi  10573  2halves  10684  halfaddsub  10689  avglt2  10694  2timesd  10698  expubnd  12129  subsq2  12179  absmax  13164  sinmul  13909  sin2t  13914  cos2t  13915  sadadd2lem2  14102  pythagtriplem4  14345  pythagtriplem14  14354  pythagtriplem16  14356  cncph  25851  pellexlem2  30931  acongrep  31083  sub2times  31622  2timesgt  31642  2txmxeqx  32638
  Copyright terms: Public domain W3C validator