Theorem 2timesd 11275

Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
2timesd.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
2timesd	|- ( ph -> ( 2 x. A ) = ( A + A ) )

Proof of Theorem 2timesd

Step	Hyp	Ref	Expression
1		2timesd.1	. 2 |- ( ph -> A e. CC )
2		2times 11145	. 2 |- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
3	1, 2	syl 17	1 |- ( ph -> ( 2 x. A ) = ( A + A ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939   x. cmul 9941   2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079

This theorem is referenced by:  lt2addmuld  11282  fzctr  12451  flhalf  12631  2submod  12731  modaddmodup  12733  m1expeven  12907  expmulnbnd  12996  discr  13001  crre  13854  imval2  13891  abslem2  14079  sqreulem  14099  amgm2  14109  caucvgrlem  14403  iseraltlem2  14413  iseraltlem3  14414  arisum2  14593  fallrisefac  14756  efival  14882  sinadd  14894  cosadd  14895  addsin  14900  subsin  14901  cosmul  14903  addcos  14904  subcos  14905  sin2t  14907  cos2t  14908  eirrlem  14932  sadadd2lem2  15172  pythagtriplem12  15531  pythagtriplem15  15534  pythagtriplem17  15536  difsqpwdvds  15591  prmreclem6  15625  4sqlem11  15659  4sqlem12  15660  vdwlem3  15687  vdwlem8  15692  vdwlem9  15693  vdwlem10  15694  bl2in  22205  tchcphlem1  23034  nmparlem  23038  cphipval2  23040  minveclem2  23197  minveclem4  23203  ovolunlem1  23265  uniioombllem5  23355  sineq0  24273  cosordlem  24277  tanarg  24365  heron  24565  dcubic1  24572  dquartlem1  24578  quart1lem  24582  sinasin  24616  asinsin  24619  cosasin  24631  efiatan2  24644  2efiatan  24645  atantan  24650  atantayl2  24665  leibpi  24669  log2cnv  24671  lgamgulmlem2  24756  lgamgulmlem3  24757  basellem5  24811  basellem6  24812  ppiub  24929  chtublem  24936  chtub  24937  bcctr  25000  pcbcctr  25001  bcmono  25002  bcmax  25003  bcp1ctr  25004  bposlem1  25009  bposlem2  25010  bposlem9  25017  gausslemma2d  25099  lgsquadlem1  25105  chebbnd1lem2  25159  dchrisumlem2  25179  dchrisum0lem1b  25204  mulog2sumlem1  25223  logdivbnd  25245  selberg3lem1  25246  pntrsumbnd2  25256  selbergr  25257  selberg3r  25258  selberg34r  25260  pntpbnd1a  25274  pntpbnd2  25276  pntlemg  25287  pntlemr  25291  pntlemo  25296  ostth2lem1  25307  ostth3  25327  finsumvtxdg2ssteplem4  26444  nvge0  27528  minvecolem2  27731  minvecolem4  27736  cdj3lem1  29293  sqsscirc1  29954  bcprod  31624  unbdqndv2lem1  32500  mblfinlem3  33448  ftc1anclem7  33491  areacirclem1  33500  areacirc  33505  isbnd3  33583  pellfundex  37450  rmxluc  37501  rmyluc  37502  rmxdbl  37504  rmydbl  37505  jm2.24nn  37526  acongeq  37550  jm2.16nn0  37571  jm3.1lem1  37584  jm3.1lem2  37585  imo72b2lem0  38465  sineq0ALT  39173  sinmulcos  40076  stirlinglem5  40295  fourierdlem79  40402  fouriercnp  40443  hoicvrrex  40770  2leaddle2  41312  lighneallem4a  41525  nnpw2pmod  42377  sinhpcosh  42481