Theorem 2cn 10627

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 10626	. 2 |- 2 e. RR
2	1	recni 9625	1 |- 2 e. CC

Syntax hints:   e. wcel 1819   CCcc 9507   2c2 10606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-i2m1 9577  ax-1ne0 9578  ax-rrecex 9581  ax-cnre 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-2 10615

This theorem is referenced by:  2ex  10628  2cnd  10629  2m1e1  10671  3m1e2  10673  2p2e4  10674  times2  10676  2div2e1  10679  1p2e3  10681  3p3e6  10690  4p3e7  10692  5p3e8  10695  6p3e9  10699  7p3e10  10702  2t1e2  10705  2t2e4  10706  3t3e9  10709  2t0e0  10712  4d2e2  10713  2cnne0  10771  halfcn  10776  1mhlfehlf  10779  8th4div3  10780  halfpm6th  10781  2mulicn  10783  2muline0  10784  halfcl  10785  half0  10787  2halves  10788  halfaddsub  10793  zneo  10966  nneo  10967  zeo  10969  4t4e16  11073  6t3e18  11078  7t7e49  11087  8t5e40  11091  9t9e81  11102  decbin0  11103  decbin2  11104  fztpval  11767  fz0tp  11803  fzo0to3tp  11903  expubnd  12229  sq2  12267  cu2  12269  subsq2  12279  binom2sub  12288  binom3  12290  zesq  12292  fac2  12362  fac3  12363  faclbnd2  12372  faclbnd4lem1  12374  faclbnd4lem3  12376  faclbnd4lem4  12377  faclbnd5  12379  bcn2  12400  swrd2lsw  12902  crre  12959  addcj  12993  imval2  12996  sqrlem7  13094  absmax  13174  rddif  13185  sqreulem  13204  amgm2  13214  abs3lemi  13254  iseraltlem2  13517  ackbijnn  13652  climcndslem1  13673  climcndslem2  13674  arisum  13683  arisum2  13684  geo2sum2  13695  geo2lim  13696  geoihalfsum  13703  efcllem  13825  ege2le3  13837  efgt0  13850  tanval2  13880  tanval3  13881  efi4p  13884  efival  13899  sinadd  13911  cosadd  13912  sinmul  13919  cos2tsin  13926  ef01bndlem  13931  cos01bnd  13933  cos1bnd  13934  cos2bnd  13935  cos01gt0  13938  sin02gt0  13939  sin4lt0  13942  znnenlem  13957  sqr2irrlem  13993  odd2np1lem  14057  odd2np1  14058  bits0  14090  bitsfzolem  14096  0bits  14101  bitsinv1  14104  sadcadd  14120  smumullem  14154  opoe  14347  omoe  14348  opeo  14349  omeo  14350  pythagtriplem1  14352  pythagtriplem12  14362  pythagtriplem14  14364  pythagtriplem15  14365  pythagtriplem16  14366  pythagtriplem17  14367  iserodd  14371  prmreclem5  14450  prmreclem6  14451  4sqlem11  14485  4sqlem12  14486  dec5dvds  14562  dec2nprm  14565  decexp2  14573  2exp6  14584  2exp6OLD  14585  2exp8  14586  2exp16  14587  7prm  14608  11prm  14612  13prm  14613  37prm  14618  43prm  14619  83prm  14620  139prm  14621  163prm  14622  317prm  14623  631prm  14624  1259lem1  14625  1259lem2  14626  1259lem3  14627  1259lem4  14628  1259lem5  14629  1259prm  14630  2503lem1  14631  2503lem2  14632  2503lem3  14633  4001lem1  14635  4001lem2  14636  4001lem3  14637  4001lem4  14638  4001prm  14639  psgnunilem2  16647  efgtlen  16871  efgredleme  16888  frgpnabllem1  17004  lt6abl  17024  htpycc  21606  pcoval2  21642  pcocn  21643  pcohtpylem  21645  pcopt  21648  pcopt2  21649  pcoass  21650  pcorevlem  21652  csbren  21952  minveclem2  21967  ovolunlem1a  22033  ovolunlem1  22034  vitalilem4  22146  mbfi1fseqlem5  22252  dvmptre  22498  dvsincos  22508  aaliou3lem2  22865  aaliou3lem3  22866  aaliou3lem8  22867  coscn  22966  sinhalfpilem  22982  cospi  22991  ef2pi  22996  ef2kpi  22997  efper  22998  sinperlem  22999  sin2kpi  23002  cos2kpi  23003  sin2pim  23004  cos2pim  23005  sinhalfpip  23011  sinhalfpim  23012  coshalfpip  23013  coshalfpim  23014  sincosq3sgn  23019  sincosq4sgn  23020  tangtx  23024  sinq12gt0  23026  sincosq1eq  23031  sincos4thpi  23032  sincos6thpi  23034  sincos3rdpi  23035  pige3  23036  abssinper  23037  coskpi  23039  sineq0  23040  coseq1  23041  efeq1  23042  efif1olem4  23058  eflogeq  23112  tanarg  23130  cxpsqrtlem  23209  cxpsqrt  23210  logsqrt  23211  root1eq1  23255  cxpeq  23257  ang180lem2  23268  ang180lem3  23269  quad2  23296  1cubrlem  23298  1cubr  23299  dcubic2  23301  dcubic1  23302  dcubic  23303  mcubic  23304  cubic2  23305  cubic  23306  dquartlem1  23308  dquartlem2  23309  dquart  23310  quart1lem  23312  quart1  23313  quartlem1  23314  quartlem2  23315  quartlem3  23316  quart  23318  sinasin  23346  asinsin  23349  atancj  23367  efiatan  23369  efiatan2  23374  2efiatan  23375  tanatan  23376  atantan  23380  atanbndlem  23382  atans2  23388  dvatan  23392  atantayl2  23395  leibpilem1  23397  leibpilem2  23398  log2cnv  23401  log2tlbnd  23402  log2ublem2  23404  log2ublem3  23405  log2ub  23406  birthday  23410  basellem1  23480  basellem3  23482  basellem8  23487  basellem9  23488  cht3  23573  1sgm2ppw  23601  ppiub  23605  chtublem  23612  chtub  23613  perfect1  23629  perfectlem1  23630  perfectlem2  23631  perfect  23632  bcmax  23679  bcp1ctr  23680  bclbnd  23681  bpos1lem  23683  bpos1  23684  bposlem1  23685  bposlem2  23686  bposlem4  23688  bposlem5  23689  bposlem6  23690  bposlem8  23692  bposlem9  23693  lgsdir2lem2  23725  lgsquadlem1  23755  lgsquadlem2  23756  lgsquad2lem2  23760  m1lgs  23763  rplogsumlem1  23795  dchrisum0fno1  23822  dchrisum0lem1  23827  dchrisum0lem2  23829  logdivsum  23844  mulog2sumlem3  23847  log2sumbnd  23855  selberglem1  23856  selberglem2  23857  selberg2  23862  selberg4lem1  23871  selberg3r  23880  pntpbnd1a  23896  pntpbnd2  23898  pntibndlem2  23902  pntlemk  23917  ax5seglem7  24365  axlowdimlem13  24384  usgraexvlem  24522  wlkdvspthlem  24736  clwlkisclwwlklem2a4  24911  numclwwlkovf2ex  25213  ex-fl  25295  ex-ind-dvds  25297  ipidsq  25750  cncph  25861  ip0i  25867  ip1ilem  25868  ipdirilem  25871  minvecolem2  25918  hvsubcan2i  26108  norm-ii-i  26181  norm3lem  26193  normpar2i  26200  polid2i  26201  hhph  26222  mayete3i  26773  mayete3iOLD  26774  nmcexi  27072  opsqrlem6  27191  addltmulALT  27492  omssubadd  28444  oddpwdc  28490  fib5  28541  ballotlem2  28624  ballotth  28673  zetacvg  28754  problem4  29219  problem5  29220  quad3  29221  4bc2eq6  29330  halfthird  29331  bpoly2  30024  bpoly3  30025  bpoly4  30026  fsumcube  30027  sin2h  30250  cos2h  30251  tan2h  30252  mblfinlem1  30256  mblfinlem2  30257  mblfinlem3  30258  itg2addnclem3  30273  dvasin  30308  areacirc  30317  heiborlem6  30517  rmxluc  31076  rmyluc  31077  jm2.17a  31102  jm2.18  31134  jm2.23  31142  jm3.1lem1  31163  proot1ex  31365  areaquad  31388  lhe4.4ex1a  31438  coskpi2  31869  cosnegpi  31870  cosknegpi  31872  stoweidlem26  32011  wallispilem4  32053  wallispi  32055  wallispi2lem1  32056  stirlinglem8  32066  dirkerper  32081  dirkertrigeqlem3  32085  dirkertrigeq  32086  dirkeritg  32087  dirkercncflem1  32088  dirkercncflem2  32089  fourierdlem57  32149  fourierdlem58  32150  fourierdlem62  32154  fourierdlem76  32168  fourierdlem103  32195  fourierdlem104  32196  sqwvfourb  32215  fourierswlem  32216  0nodd  32760  0even  32881  2even  32883  2zrngamgm  32889  2t6m3t4e0  33081  linevalexample  33140  zlmodzxzequap  33244  sinhpcosh  33278  sineq0ALT  33880