Theorem 2cn 10682

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 10681	. 2 |- 2 e. RR
2	1	recni 9657	1 |- 2 e. CC

Syntax hints:   e. wcel 1869   CCcc 9539   2c2 10661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-i2m1 9609  ax-1ne0 9610  ax-rrecex 9613  ax-cnre 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306  df-2 10670

This theorem is referenced by:  2ex  10683  2cnd  10684  2m1e1  10726  3m1e2  10728  2p2e4  10729  times2  10731  2div2e1  10734  1p2e3  10736  3p3e6  10745  4p3e7  10747  5p3e8  10750  6p3e9  10754  7p3e10  10757  2t1e2  10760  2t2e4  10761  3t3e9  10764  2t0e0  10767  4d2e2  10768  2cnne0  10826  halfcn  10831  1mhlfehlf  10834  8th4div3  10835  halfpm6th  10836  2mulicn  10838  2muline0  10839  halfcl  10840  half0  10842  2halves  10843  halfaddsub  10848  zneo  11020  nneo  11021  zeo  11023  4t4e16  11126  6t3e18  11131  7t7e49  11140  8t5e40  11144  9t9e81  11155  decbin0  11156  decbin2  11157  halfthird  11159  fztpval  11859  fz0tp  11895  fzo0to3tp  12000  expubnd  12334  sq2  12372  cu2  12374  subsq2  12384  binom2sub  12392  binom3  12394  zesq  12396  fac2  12466  fac3  12467  faclbnd2  12477  faclbnd4lem1  12479  faclbnd4lem3  12481  faclbnd4lem4  12482  faclbnd5  12484  bcn2  12505  4bc2eq6  12515  swrd2lsw  13021  crre  13171  addcj  13205  imval2  13208  sqrlem7  13306  absmax  13386  rddif  13397  sqreulem  13416  amgm2  13426  abs3lemi  13466  iseraltlem2  13742  ackbijnn  13879  climcndslem1  13900  climcndslem2  13901  arisum  13911  arisum2  13912  geo2sum2  13923  geo2lim  13924  geoihalfsum  13931  bpoly2  14103  bpoly3  14104  bpoly4  14105  fsumcube  14106  efcllem  14125  ege2le3  14137  efgt0  14150  tanval2  14180  tanval3  14181  efi4p  14184  efival  14199  sinadd  14211  cosadd  14212  sinmul  14219  cos2tsin  14226  ef01bndlem  14231  cos01bnd  14233  cos1bnd  14234  cos2bnd  14235  cos01gt0  14238  sin02gt0  14239  sin4lt0  14242  znnenlem  14257  sqr2irrlem  14293  odd2np1lem  14357  odd2np1  14358  bits0  14394  bitsfzolem  14400  bitsfzolemOLD  14401  0bits  14406  bitsinv1  14409  sadcadd  14425  smumullem  14459  6gcd4e2  14495  3lcm2e6woprm  14573  6lcm4e12  14574  opoe  14754  omoe  14755  opeo  14756  omeo  14757  pythagtriplem1  14759  pythagtriplem12  14769  pythagtriplem14  14771  pythagtriplem15  14772  pythagtriplem16  14773  pythagtriplem17  14774  iserodd  14778  prmreclem5  14857  prmreclem6  14858  4sqlem11  14892  4sqlem12  14893  prmo2  14991  prmo3  14992  dec5dvds  15029  dec2nprm  15032  decexp2  15040  2exp6  15051  2exp6OLD  15052  2exp8  15053  2exp16  15054  7prm  15075  11prm  15079  13prm  15080  37prm  15085  43prm  15086  83prm  15087  139prm  15088  163prm  15089  317prm  15090  631prm  15091  1259lem1  15095  1259lem2  15096  1259lem3  15097  1259lem4  15098  1259lem5  15099  1259prm  15100  2503lem1  15101  2503lem2  15102  2503lem3  15103  4001lem1  15105  4001lem2  15106  4001lem3  15107  4001lem4  15108  4001prm  15109  psgnunilem2  17129  efgtlen  17369  efgredleme  17386  frgpnabllem1  17502  lt6abl  17522  htpycc  22003  pcoval2  22039  pcocn  22040  pcohtpylem  22042  pcopt  22045  pcopt2  22046  pcoass  22047  pcorevlem  22049  csbren  22345  minveclem2  22360  minveclem2OLD  22372  ovolunlem1a  22441  ovolunlem1  22442  vitalilem4  22561  mbfi1fseqlem5  22669  dvmptre  22915  dvsincos  22925  aaliou3lem2  23291  aaliou3lem3  23292  aaliou3lem8  23293  coscn  23392  sinhalfpilem  23410  cospi  23419  ef2pi  23424  ef2kpi  23425  efper  23426  sinperlem  23427  sin2kpi  23430  cos2kpi  23431  sin2pim  23432  cos2pim  23433  sinhalfpip  23439  sinhalfpim  23440  coshalfpip  23441  coshalfpim  23442  sincosq3sgn  23447  sincosq4sgn  23448  tangtx  23452  sinq12gt0  23454  sincosq1eq  23459  sincos4thpi  23460  sincos6thpi  23462  sincos3rdpi  23463  pige3  23464  abssinper  23465  coskpi  23467  sineq0  23468  coseq1  23469  efeq1  23470  efif1olem4  23486  eflogeq  23543  tanarg  23560  cxpsqrtlem  23639  cxpsqrt  23640  logsqrt  23641  root1eq1  23687  cxpeq  23689  ang180lem2  23731  ang180lem3  23732  quad2  23757  1cubrlem  23759  1cubr  23760  dcubic2  23762  dcubic1  23763  dcubic  23764  mcubic  23765  cubic2  23766  cubic  23767  dquartlem1  23769  dquartlem2  23770  dquart  23771  quart1lem  23773  quart1  23774  quartlem1  23775  quartlem2  23776  quartlem3  23777  quart  23779  sinasin  23807  asinsin  23810  atancj  23828  efiatan  23830  efiatan2  23835  2efiatan  23836  tanatan  23837  atantan  23841  atanbndlem  23843  atans2  23849  dvatan  23853  atantayl2  23856  leibpilem1  23858  leibpilem2  23859  log2cnv  23862  log2tlbnd  23863  log2ublem2  23865  log2ublem3  23866  log2ub  23867  birthday  23872  zetacvg  23932  basellem1  23999  basellem3  24001  basellem8  24006  basellem9  24007  cht3  24092  1sgm2ppw  24120  ppiub  24124  chtublem  24131  chtub  24132  perfect1  24148  perfectlem1  24149  perfectlem2  24150  perfect  24151  bcmax  24198  bcp1ctr  24199  bclbnd  24200  bpos1lem  24202  bpos1  24203  bposlem1  24204  bposlem2  24205  bposlem4  24207  bposlem5  24208  bposlem6  24209  bposlem8  24211  bposlem9  24212  lgsdir2lem2  24244  lgsquadlem1  24274  lgsquadlem2  24275  lgsquad2lem2  24279  m1lgs  24282  rplogsumlem1  24314  dchrisum0fno1  24341  dchrisum0lem1  24346  dchrisum0lem2  24348  logdivsum  24363  mulog2sumlem3  24366  log2sumbnd  24374  selberglem1  24375  selberglem2  24376  selberg2  24381  selberg4lem1  24390  selberg3r  24399  pntpbnd1a  24415  pntpbnd2  24417  pntibndlem2  24421  pntlemk  24436  ax5seglem7  24957  axlowdimlem13  24976  usgraexmplvtxlem  25114  wlkdvspthlem  25329  clwlkisclwwlklem2a4  25504  numclwwlkovf2ex  25806  ex-fl  25889  ex-ind-dvds  25891  ipidsq  26341  cncph  26452  ip0i  26458  ip1ilem  26459  ipdirilem  26462  minvecolem2  26509  minvecolem2OLD  26519  hvsubcan2i  26709  norm-ii-i  26782  norm3lem  26794  normpar2i  26801  polid2i  26802  hhph  26823  mayete3i  27373  nmcexi  27671  opsqrlem6  27790  addltmulALT  28091  omssubadd  29130  omssubaddOLD  29134  oddpwdc  29189  fib5  29240  ballotlem2  29323  ballotth  29372  ballotthOLD  29410  problem4  30302  problem5  30303  quad3  30304  sin2h  31893  cos2h  31894  tan2h  31895  poimirlem29  31927  mblfinlem1  31935  mblfinlem2  31936  mblfinlem3  31937  itg2addnclem3  31953  dvasin  31986  areacirc  31995  heiborlem6  32106  rmxluc  35748  rmyluc  35749  jm2.17a  35774  jm2.18  35807  jm2.23  35815  jm3.1lem1  35836  proot1ex  36042  areaquad  36065  lhe4.4ex1a  36580  sineq0ALT  37239  coskpi2  37605  cosnegpi  37606  cosknegpi  37608  stoweidlem26  37750  wallispilem4  37794  wallispi  37796  wallispi2lem1  37797  stirlinglem8  37807  dirkerper  37822  dirkertrigeqlem3  37826  dirkertrigeq  37827  dirkeritg  37828  dirkercncflem1  37829  dirkercncflem2  37830  fourierdlem57  37891  fourierdlem58  37892  fourierdlem62  37896  fourierdlem76  37910  fourierdlem103  37937  fourierdlem104  37938  sqwvfourb  37957  fourierswlem  37958  bits0ALTV  38564  0evenALTV  38573  6even  38594  8even  38596  perfectALTVlem1  38599  perfectALTVlem2  38600  perfectALTV  38601  nnsum3primes4  38639  bgoldbtbndlem1  38656  3exp4mod41  38672  41prothprmlem1  38673  41prothprmlem2  38674  41prothprm  38675  0nodd  39152  0even  39273  2even  39275  2zrngamgm  39281  2t6m3t4e0  39473  linevalexample  39532  zlmodzxzequap  39636  3halfnz  39661  pw2m1lepw2m1  39662  nno  39672  nn0o  39673  nnlog2ge0lt1  39721  logbpw2m1  39722  nnpw2blen  39735  nnpw2pmod  39738  blen1  39739  blen2  39740  blennnt2  39744  nnolog2flm1  39745  0dig2nn0e  39767  0dig2nn0o  39768  nn0sumshdiglemA  39774  nn0sumshdiglemB  39775  nn0sumshdiglem1  39776  nn0sumshdiglem2  39777  sinhpcosh  39804