Theorem 2cn 10707

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 10706	. 2 |- 2 e. RR
2	1	recni 9680	1 |- 2 e. CC

Syntax hints:   e. wcel 1897   CCcc 9562   2c2 10686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-i2m1 9632  ax-1ne0 9633  ax-rrecex 9636  ax-cnre 9637

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-iota 5564  df-fv 5608  df-ov 6317  df-2 10695

This theorem is referenced by:  2ex  10708  2cnd  10709  2m1e1  10751  3m1e2  10753  2p2e4  10755  times2  10757  2div2e1  10760  1p2e3  10762  3p3e6  10771  4p3e7  10773  5p3e8  10776  6p3e9  10780  7p3e10  10783  2t1e2  10786  2t2e4  10787  3t3e9  10790  2t0e0  10793  4d2e2  10794  2cnne0  10852  halfcn  10857  1mhlfehlf  10860  8th4div3  10861  halfpm6th  10862  2mulicn  10864  2muline0  10865  halfcl  10866  half0  10868  2halves  10869  halfaddsub  10874  zneo  11046  nneo  11047  zeo  11049  4t4e16  11152  6t3e18  11157  7t7e49  11166  8t5e40  11170  9t9e81  11181  decbin0  11182  decbin2  11183  halfthird  11185  fztpval  11885  fz0tp  11921  fzo0to3tp  12029  expubnd  12364  sq2  12402  cu2  12404  subsq2  12414  binom2sub  12422  binom3  12424  zesq  12426  fac2  12496  fac3  12497  faclbnd2  12507  faclbnd4lem1  12509  faclbnd4lem3  12511  faclbnd4lem4  12512  faclbnd5  12514  bcn2  12535  4bc2eq6  12545  swrd2lsw  13075  crre  13225  addcj  13259  imval2  13262  sqrlem7  13360  absmax  13440  rddif  13451  sqreulem  13470  amgm2  13480  abs3lemi  13520  iseraltlem2  13797  ackbijnn  13934  climcndslem1  13955  climcndslem2  13956  arisum  13966  arisum2  13967  geo2sum2  13978  geo2lim  13979  geoihalfsum  13986  bpoly2  14158  bpoly3  14159  bpoly4  14160  fsumcube  14161  efcllem  14180  ege2le3  14192  efgt0  14205  tanval2  14235  tanval3  14236  efi4p  14239  efival  14254  sinadd  14266  cosadd  14267  sinmul  14274  cos2tsin  14281  ef01bndlem  14286  cos01bnd  14288  cos1bnd  14289  cos2bnd  14290  cos01gt0  14293  sin02gt0  14294  sin4lt0  14297  znnenlem  14312  sqr2irrlem  14348  odd2np1lem  14412  odd2np1  14413  bits0  14449  bitsfzolem  14455  bitsfzolemOLD  14456  0bits  14461  bitsinv1  14464  sadcadd  14480  smumullem  14514  6gcd4e2  14550  3lcm2e6woprm  14628  6lcm4e12  14629  opoe  14809  omoe  14810  opeo  14811  omeo  14812  pythagtriplem1  14814  pythagtriplem12  14824  pythagtriplem14  14826  pythagtriplem15  14827  pythagtriplem16  14828  pythagtriplem17  14829  iserodd  14833  prmreclem5  14912  prmreclem6  14913  4sqlem11  14947  4sqlem12  14948  prmo2  15046  prmo3  15047  dec5dvds  15084  dec2nprm  15087  decexp2  15095  2exp6  15106  2exp6OLD  15107  2exp8  15108  2exp16  15109  7prm  15130  11prm  15134  13prm  15135  37prm  15140  43prm  15141  83prm  15142  139prm  15143  163prm  15144  317prm  15145  631prm  15146  1259lem1  15150  1259lem2  15151  1259lem3  15152  1259lem4  15153  1259lem5  15154  1259prm  15155  2503lem1  15156  2503lem2  15157  2503lem3  15158  4001lem1  15160  4001lem2  15161  4001lem3  15162  4001lem4  15163  4001prm  15164  psgnunilem2  17184  efgtlen  17424  efgredleme  17441  frgpnabllem1  17557  lt6abl  17577  htpycc  22059  pcoval2  22095  pcocn  22096  pcohtpylem  22098  pcopt  22101  pcopt2  22102  pcoass  22103  pcorevlem  22105  csbren  22401  minveclem2  22416  minveclem2OLD  22428  ovolunlem1a  22497  ovolunlem1  22498  vitalilem4  22617  mbfi1fseqlem5  22725  dvmptre  22971  dvsincos  22981  aaliou3lem2  23347  aaliou3lem3  23348  aaliou3lem8  23349  coscn  23448  sinhalfpilem  23466  cospi  23475  ef2pi  23480  ef2kpi  23481  efper  23482  sinperlem  23483  sin2kpi  23486  cos2kpi  23487  sin2pim  23488  cos2pim  23489  sinhalfpip  23495  sinhalfpim  23496  coshalfpip  23497  coshalfpim  23498  sincosq3sgn  23503  sincosq4sgn  23504  tangtx  23508  sinq12gt0  23510  sincosq1eq  23515  sincos4thpi  23516  sincos6thpi  23518  sincos3rdpi  23519  pige3  23520  abssinper  23521  coskpi  23523  sineq0  23524  coseq1  23525  efeq1  23526  efif1olem4  23542  eflogeq  23599  tanarg  23616  cxpsqrtlem  23695  cxpsqrt  23696  logsqrt  23697  root1eq1  23743  cxpeq  23745  ang180lem2  23787  ang180lem3  23788  quad2  23813  1cubrlem  23815  1cubr  23816  dcubic2  23818  dcubic1  23819  dcubic  23820  mcubic  23821  cubic2  23822  cubic  23823  dquartlem1  23825  dquartlem2  23826  dquart  23827  quart1lem  23829  quart1  23830  quartlem1  23831  quartlem2  23832  quartlem3  23833  quart  23835  sinasin  23863  asinsin  23866  atancj  23884  efiatan  23886  efiatan2  23891  2efiatan  23892  tanatan  23893  atantan  23897  atanbndlem  23899  atans2  23905  dvatan  23909  atantayl2  23912  leibpilem1  23914  leibpilem2  23915  log2cnv  23918  log2tlbnd  23919  log2ublem2  23921  log2ublem3  23922  log2ub  23923  birthday  23928  zetacvg  23988  basellem1  24055  basellem3  24057  basellem8  24062  basellem9  24063  cht3  24148  1sgm2ppw  24176  ppiub  24180  chtublem  24187  chtub  24188  perfect1  24204  perfectlem1  24205  perfectlem2  24206  perfect  24207  bcmax  24254  bcp1ctr  24255  bclbnd  24256  bpos1lem  24258  bpos1  24259  bposlem1  24260  bposlem2  24261  bposlem4  24263  bposlem5  24264  bposlem6  24265  bposlem8  24267  bposlem9  24268  lgsdir2lem2  24300  lgsquadlem1  24330  lgsquadlem2  24331  lgsquad2lem2  24335  m1lgs  24338  rplogsumlem1  24370  dchrisum0fno1  24397  dchrisum0lem1  24402  dchrisum0lem2  24404  logdivsum  24419  mulog2sumlem3  24422  log2sumbnd  24430  selberglem1  24431  selberglem2  24432  selberg2  24437  selberg4lem1  24446  selberg3r  24455  pntpbnd1a  24471  pntpbnd2  24473  pntibndlem2  24477  pntlemk  24492  ax5seglem7  25013  axlowdimlem13  25032  usgraexmplvtxlem  25170  wlkdvspthlem  25385  clwlkisclwwlklem2a4  25560  numclwwlkovf2ex  25862  ex-fl  25945  ex-ind-dvds  25947  ipidsq  26397  cncph  26508  ip0i  26514  ip1ilem  26515  ipdirilem  26518  minvecolem2  26565  minvecolem2OLD  26575  hvsubcan2i  26765  norm-ii-i  26838  norm3lem  26850  normpar2i  26857  polid2i  26858  hhph  26879  mayete3i  27429  nmcexi  27727  opsqrlem6  27846  addltmulALT  28147  omssubadd  29176  omssubaddOLD  29180  oddpwdc  29235  fib5  29286  ballotlem2  29369  ballotth  29418  ballotthOLD  29456  problem4  30348  problem5  30349  quad3  30350  sin2h  31979  cos2h  31980  tan2h  31981  poimirlem29  32013  mblfinlem1  32021  mblfinlem2  32022  mblfinlem3  32023  itg2addnclem3  32039  dvasin  32072  areacirc  32081  heiborlem6  32192  rmxluc  35828  rmyluc  35829  jm2.17a  35854  jm2.18  35887  jm2.23  35895  jm3.1lem1  35916  proot1ex  36122  areaquad  36145  lhe4.4ex1a  36721  sineq0ALT  37373  coskpi2  37778  cosnegpi  37779  cosknegpi  37781  stoweidlem26  37923  wallispilem4  37967  wallispi  37969  wallispi2lem1  37970  stirlinglem8  37980  dirkerper  37995  dirkertrigeqlem3  37999  dirkertrigeq  38000  dirkeritg  38001  dirkercncflem1  38002  dirkercncflem2  38003  fourierdlem57  38064  fourierdlem58  38065  fourierdlem62  38069  fourierdlem76  38083  fourierdlem103  38110  fourierdlem104  38111  sqwvfourb  38130  fourierswlem  38131  bits0ALTV  38845  0evenALTV  38854  6even  38875  8even  38877  perfectALTVlem1  38880  perfectALTVlem2  38881  perfectALTV  38882  nnsum3primes4  38920  bgoldbtbndlem1  38937  3exp4mod41  38953  41prothprmlem1  38954  41prothprmlem2  38955  41prothprm  38956  0nodd  40082  0even  40203  2even  40205  2zrngamgm  40211  2t6m3t4e0  40401  linevalexample  40460  zlmodzxzequap  40564  3halfnz  40589  pw2m1lepw2m1  40590  nno  40600  nn0o  40601  nnlog2ge0lt1  40649  logbpw2m1  40650  nnpw2blen  40663  nnpw2pmod  40666  blen1  40667  blen2  40668  blennnt2  40672  nnolog2flm1  40673  0dig2nn0e  40695  0dig2nn0o  40696  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703  nn0sumshdiglem1  40704  nn0sumshdiglem2  40705  sinhpcosh  40732