Theorem 2cn 10026

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 10025	. 2 |- 2 e. RR
2	1	recni 9058	1 |- 2 e. CC

Syntax hints:   e. wcel 1721   CCcc 8944   2c2 10005

This theorem is referenced by:  2m1e1  10051  3m1e2  10052  3m1e2OLD  10053  2p2e4  10054  times2  10056  3p3e6  10068  4p3e7  10070  5p3e8  10073  6p3e9  10077  7p3e10  10080  2t2e4  10083  3t3e9  10085  4d2e2  10088  1mhlfehlf  10146  8th4div3  10147  halfpm6th  10148  halfcl  10149  half0  10151  2halves  10152  halfaddsub  10157  zneo  10308  nneo  10309  zeo  10311  zeo2  10312  4t4e16  10411  6t3e18  10416  7t7e49  10425  8t5e40  10429  9t9e81  10440  decbin0  10441  decbin2  10442  fz0tp  11059  fztpval  11063  fzo0to3tp  11140  flhalf  11186  expubnd  11395  sq2  11432  cu2  11434  subsq2  11444  binom2sub  11453  binom3  11455  zesq  11457  expmulnbnd  11466  discr  11471  fac2  11527  fac3  11528  faclbnd2  11537  faclbnd4lem1  11539  faclbnd4lem3  11541  faclbnd4lem4  11542  faclbnd5  11544  bcn2  11565  crre  11874  addcj  11908  imval2  11911  sqrlem7  12009  absmax  12088  rddif  12099  sqreulem  12118  amgm2  12128  abs3lemi  12168  iseraltlem2  12431  iseralt  12433  ackbijnn  12562  climcndslem1  12584  climcndslem2  12585  arisum  12594  arisum2  12595  trirecip  12597  geo2sum  12605  geo2sum2  12606  geo2lim  12607  geoihalfsum  12614  efcllem  12635  ege2le3  12647  efgt0  12659  sinf  12680  tanval2  12689  tanval3  12690  efi4p  12693  sinneg  12702  efival  12708  sinhval  12710  tanhlt1  12716  sinadd  12720  cosadd  12721  sinmul  12728  cosmul  12729  cos2tsin  12735  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  cos01gt0  12747  sin02gt0  12748  sin4lt0  12751  znnenlem  12766  rpnnen2lem3  12771  rpnnen2lem11  12779  sqr2irrlem  12802  sqr2irr  12803  odd2np1lem  12862  odd2np1  12863  oddm1even  12864  oddp1even  12865  bits0  12895  bitsp1o  12900  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  0bits  12906  bitsinv1lem  12908  bitsinv1  12909  sadadd2lem2  12917  sadcadd  12925  bitsuz  12941  bitsshft  12942  smumullem  12959  prmdiv  13129  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pythagtriplem1  13145  pythagtriplem4  13148  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem15  13158  pythagtriplem16  13159  pythagtriplem17  13160  iserodd  13164  prmreclem5  13243  prmreclem6  13244  4sqlem7  13267  4sqlem10  13270  4sqlem11  13278  4sqlem12  13279  4sqlem19  13286  dec5dvds  13355  dec2nprm  13358  decexp2  13366  2exp6  13377  2exp8  13378  2exp16  13379  2expltfac  13381  prmlem1a  13384  7prm  13388  11prm  13392  13prm  13393  prmlem2  13397  37prm  13398  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  efgtlen  15313  efgredlemg  15329  efgredleme  15330  frgpnabllem1  15439  lt6abl  15459  metnrmlem3  18844  iihalf1cn  18910  iihalf2cn  18912  htpycc  18958  pco0  18992  pco1  18993  pcoval2  18994  pcocn  18995  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  minveclem2  19280  ovolunlem1a  19345  ovolunlem1  19346  uniioombllem5  19432  uniioombl  19434  dyaddisjlem  19440  vitalilem4  19456  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  dvmptre  19808  dvmptim  19809  dvsincos  19818  lhop1  19851  aaliou3lem2  20213  aaliou3lem3  20214  aaliou3lem8  20215  sincn  20313  coscn  20314  pilem2  20321  sinhalfpilem  20327  cospi  20333  sin2pi  20336  cos2pi  20337  ef2pi  20338  ef2kpi  20339  efper  20340  sinperlem  20341  sin2kpi  20344  cos2kpi  20345  sin2pim  20346  cos2pim  20347  sinhalfpip  20353  sinhalfpim  20354  coshalfpip  20355  coshalfpim  20356  ptolemy  20357  sincosq3sgn  20361  sincosq4sgn  20362  tangtx  20366  sinq12gt0  20368  sincosq1eq  20373  sincos4thpi  20374  sincos6thpi  20376  sincos3rdpi  20377  pige3  20378  abssinper  20379  coskpi  20381  sineq0  20382  coseq1  20383  efeq1  20384  efif1olem4  20400  eflogeq  20449  cosargd  20456  tanarg  20467  cxpsqrlem  20546  cxpsqr  20547  logsqr  20548  dvsqr  20581  root1id  20591  root1eq1  20592  cxpeq  20594  ang180lem2  20605  ang180lem3  20606  pythag  20612  ssscongptld  20619  chordthmlem  20626  chordthmlem2  20627  chordthmlem4  20629  quad2  20632  1cubrlem  20634  1cubr  20635  dcubic1lem  20636  dcubic2  20637  dcubic1  20638  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  quartlem2  20651  quartlem3  20652  quartlem4  20653  quart  20654  sinasin  20682  asinsin  20685  cosasin  20697  atancj  20703  efiatan  20705  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  atantan  20716  atanbndlem  20718  atan1  20721  atans2  20724  dvatan  20728  atantayl  20730  atantayl2  20731  atantayl3  20732  leibpilem1  20733  leibpilem2  20734  log2cnv  20737  log2tlbnd  20738  log2ublem2  20740  log2ublem3  20741  log2ub  20742  birthday  20746  cxp2limlem  20767  divsqrsumlem  20771  ftalem2  20809  basellem1  20816  basellem2  20817  basellem3  20818  basellem8  20823  basellem9  20824  cht3  20909  1sgm2ppw  20937  ppiub  20941  chtublem  20948  chtub  20949  logfaclbnd  20959  perfect1  20965  perfectlem1  20966  perfectlem2  20967  perfect  20968  bcmax  21015  bcp1ctr  21016  bclbnd  21017  bpos1lem  21019  bpos1  21020  bposlem1  21021  bposlem2  21022  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem8  21028  bposlem9  21029  lgslem1  21033  lgsdir2lem2  21061  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem1  21095  lgsquad2lem2  21096  m1lgs  21099  chebbnd1lem1  21116  chebbnd1lem3  21118  chto1ub  21123  rplogsumlem1  21131  dchrisumlem2  21137  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2  21165  logdivsum  21180  mulog2sumlem2  21182  mulog2sumlem3  21183  vmalogdivsum2  21185  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberg2  21198  chpdifbndlem1  21200  selberg3lem1  21204  selberg3  21206  selberg4lem1  21207  selberg4  21208  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntlemg  21245  pntlemh  21246  pntlemk  21253  pntlemo  21254  ostth2lem1  21265  usgraexvlem  21367  wlkdvspthlem  21560  eupath  21656  konigsberg  21662  1kp2ke3k  21707  ex-fl  21708  ipidsq  22162  cncph  22273  ip0i  22279  ip1ilem  22280  ipdirilem  22283  minvecolem2  22330  hvsubcan2i  22519  norm-ii-i  22592  norm3lem  22604  normpar2i  22611  polid2i  22612  hhph  22633  mayete3i  23183  mayete3iOLD  23184  nmcexi  23482  opsqrlem6  23601  cdj3lem1  23890  addltmulALT  23902  sqsscirc1  24259  dya2icoseg  24580  dya2iocucvr  24587  ballotlem2  24699  ballotth  24748  zetacvg  24752  lgamgulmlem4  24769  lgamucov  24775  subfacp1lem1  24818  subfacp1lem5  24823  4bc2eq6  25157  halfthird  25158  ax5seglem7  25778  axlowdimlem13  25797  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  itg2addnclem3  26157  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  areacirclem1  26184  areacirc  26187  csbrn  26346  trirn  26347  isbnd2  26382  heiborlem6  26415  rabren3dioph  26766  rmxluc  26889  rmyluc  26890  rmyluc2  26891  rmydbl  26893  jm2.17a  26915  jm2.18  26949  jm2.22  26956  jm2.23  26957  jm2.25  26960  jm2.27c  26968  jm3.1lem1  26978  jm3.1lem2  26979  psgnunilem2  27286  proot1ex  27388  lhe4.4ex1a  27414  refsum2cnlem1  27575  m1expeven  27592  itgsinexp  27616  stoweidlem1  27617  stoweidlem14  27630  stoweidlem24  27640  stoweidlem26  27642  stoweidlem62  27678  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem11  27700  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  sinhpcosh  28197

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-2 10014