Theorem 2cn 10595

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 10594	. 2 |- 2 e. RR
2	1	recni 9597	1 |- 2 e. CC

Syntax hints:   e. wcel 1762   CCcc 9479   2c2 10574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-2 10583

This theorem is referenced by:  2ex  10596  2cnd  10597  2m1e1  10639  3m1e2  10641  2p2e4  10642  times2  10644  2div2e1  10647  1p2e3  10649  3p3e6  10658  4p3e7  10660  5p3e8  10663  6p3e9  10667  7p3e10  10670  2t1e2  10673  2t2e4  10674  3t3e9  10677  2t0e0  10680  4d2e2  10681  2cnne0  10739  halfcn  10744  1mhlfehlf  10747  8th4div3  10748  halfpm6th  10749  2mulicn  10751  2muline0  10752  halfcl  10753  half0  10755  2halves  10756  halfaddsub  10761  zneo  10932  nneo  10933  zeo  10935  4t4e16  11038  6t3e18  11043  7t7e49  11052  8t5e40  11056  9t9e81  11067  decbin0  11068  decbin2  11069  fztpval  11730  fz0tp  11764  fzo0to3tp  11857  expubnd  12181  sq2  12219  cu2  12221  subsq2  12231  binom2sub  12240  binom3  12242  zesq  12244  fac2  12314  fac3  12315  faclbnd2  12324  faclbnd4lem1  12326  faclbnd4lem3  12328  faclbnd4lem4  12329  faclbnd5  12331  bcn2  12352  swrd2lsw  12840  crre  12897  addcj  12931  imval2  12934  sqrlem7  13032  absmax  13111  rddif  13122  sqreulem  13141  amgm2  13151  abs3lemi  13191  iseraltlem2  13454  ackbijnn  13592  climcndslem1  13613  climcndslem2  13614  arisum  13623  arisum2  13624  geo2sum2  13635  geo2lim  13636  geoihalfsum  13643  efcllem  13664  ege2le3  13676  efgt0  13688  tanval2  13718  tanval3  13719  efi4p  13722  efival  13737  sinadd  13749  cosadd  13750  sinmul  13757  cos2tsin  13764  ef01bndlem  13769  cos01bnd  13771  cos1bnd  13772  cos2bnd  13773  cos01gt0  13776  sin02gt0  13777  sin4lt0  13780  znnenlem  13795  sqr2irrlem  13831  odd2np1lem  13893  odd2np1  13894  bits0  13926  bitsfzolem  13932  0bits  13937  bitsinv1  13940  sadcadd  13956  smumullem  13990  opoe  14183  omoe  14184  opeo  14185  omeo  14186  pythagtriplem1  14188  pythagtriplem12  14198  pythagtriplem14  14200  pythagtriplem15  14201  pythagtriplem16  14202  pythagtriplem17  14203  iserodd  14207  prmreclem5  14286  prmreclem6  14287  4sqlem11  14321  4sqlem12  14322  dec5dvds  14398  dec2nprm  14401  decexp2  14409  2exp6  14420  2exp8  14421  2exp16  14422  7prm  14443  11prm  14447  13prm  14448  37prm  14453  43prm  14454  83prm  14455  139prm  14456  163prm  14457  317prm  14458  631prm  14459  1259lem1  14460  1259lem2  14461  1259lem3  14462  1259lem4  14463  1259lem5  14464  1259prm  14465  2503lem1  14466  2503lem2  14467  2503lem3  14468  4001lem1  14470  4001lem2  14471  4001lem3  14472  4001lem4  14473  4001prm  14474  psgnunilem2  16309  efgtlen  16533  efgredleme  16550  frgpnabllem1  16661  lt6abl  16681  htpycc  21208  pcoval2  21244  pcocn  21245  pcohtpylem  21247  pcopt  21250  pcopt2  21251  pcoass  21252  pcorevlem  21254  csbren  21554  minveclem2  21569  ovolunlem1a  21635  ovolunlem1  21636  vitalilem4  21748  mbfi1fseqlem5  21854  dvmptre  22100  dvsincos  22110  aaliou3lem2  22466  aaliou3lem3  22467  aaliou3lem8  22468  coscn  22567  sinhalfpilem  22582  cospi  22591  ef2pi  22596  ef2kpi  22597  efper  22598  sinperlem  22599  sin2kpi  22602  cos2kpi  22603  sin2pim  22604  cos2pim  22605  sinhalfpip  22611  sinhalfpim  22612  coshalfpip  22613  coshalfpim  22614  sincosq3sgn  22619  sincosq4sgn  22620  tangtx  22624  sinq12gt0  22626  sincosq1eq  22631  sincos4thpi  22632  sincos6thpi  22634  sincos3rdpi  22635  pige3  22636  abssinper  22637  coskpi  22639  sineq0  22640  coseq1  22641  efeq1  22642  efif1olem4  22658  eflogeq  22707  tanarg  22725  cxpsqrlem  22804  cxpsqr  22805  logsqr  22806  root1eq1  22850  cxpeq  22852  ang180lem2  22863  ang180lem3  22864  quad2  22891  1cubrlem  22893  1cubr  22894  dcubic2  22896  dcubic1  22897  dcubic  22898  mcubic  22899  cubic2  22900  cubic  22901  dquartlem1  22903  dquartlem2  22904  dquart  22905  quart1lem  22907  quart1  22908  quartlem1  22909  quartlem2  22910  quartlem3  22911  quart  22913  sinasin  22941  asinsin  22944  atancj  22962  efiatan  22964  efiatan2  22969  2efiatan  22970  tanatan  22971  atantan  22975  atanbndlem  22977  atans2  22983  dvatan  22987  atantayl2  22990  leibpilem1  22992  leibpilem2  22993  log2cnv  22996  log2tlbnd  22997  log2ublem2  22999  log2ublem3  23000  log2ub  23001  birthday  23005  basellem1  23075  basellem3  23077  basellem8  23082  basellem9  23083  cht3  23168  1sgm2ppw  23196  ppiub  23200  chtublem  23207  chtub  23208  perfect1  23224  perfectlem1  23225  perfectlem2  23226  perfect  23227  bcmax  23274  bcp1ctr  23275  bclbnd  23276  bpos1lem  23278  bpos1  23279  bposlem1  23280  bposlem2  23281  bposlem4  23283  bposlem5  23284  bposlem6  23285  bposlem8  23287  bposlem9  23288  lgsdir2lem2  23320  lgsquadlem1  23350  lgsquadlem2  23351  lgsquad2lem2  23355  m1lgs  23358  rplogsumlem1  23390  dchrisum0fno1  23417  dchrisum0lem1  23422  dchrisum0lem2  23424  logdivsum  23439  mulog2sumlem3  23442  log2sumbnd  23450  selberglem1  23451  selberglem2  23452  selberg2  23457  selberg4lem1  23466  selberg3r  23475  pntpbnd1a  23491  pntpbnd2  23493  pntibndlem2  23497  pntlemk  23512  ax5seglem7  23907  axlowdimlem13  23926  usgraexvlem  24057  wlkdvspthlem  24271  clwlkisclwwlklem2a4  24446  ex-fl  24695  ipidsq  25149  cncph  25260  ip0i  25266  ip1ilem  25267  ipdirilem  25270  minvecolem2  25317  hvsubcan2i  25507  norm-ii-i  25580  norm3lem  25592  normpar2i  25599  polid2i  25600  hhph  25621  mayete3i  26172  mayete3iOLD  26173  nmcexi  26471  opsqrlem6  26590  addltmulALT  26891  oddpwdc  27783  fib5  27834  ballotlem2  27917  ballotth  27966  zetacvg  28047  problem4  28347  problem5  28348  quad3  28349  4bc2eq6  28437  halfthird  28438  bpoly2  29246  bpoly3  29247  bpoly4  29248  fsumcube  29249  sin2h  29473  cos2h  29474  tan2h  29475  mblfinlem1  29479  mblfinlem2  29480  mblfinlem3  29481  itg2addnclem3  29496  dvasin  29531  areacirc  29540  heiborlem6  29766  rmxluc  30327  rmyluc  30328  jm2.17a  30353  jm2.18  30387  jm2.23  30395  jm3.1lem1  30416  proot1ex  30619  areaquad  30642  lhe4.4ex1a  30653  0ellimcdiv  31010  coseq0  31018  sinmulcos  31020  coskpi2  31021  cosnegpi  31022  sinaover2ne0  31023  cosknegpi  31024  stoweidlem26  31145  wallispilem4  31187  wallispi  31189  wallispi2lem1  31190  wallispi2lem2  31191  wallispi2  31192  stirlinglem8  31200  stirlinglem11  31203  dirker2re  31211  dirkerdenne0  31212  dirkerval2  31213  dirkerre  31214  dirkerper  31215  dirkertrigeqlem1  31217  dirkertrigeqlem2  31218  dirkertrigeqlem3  31219  dirkertrigeq  31220  dirkeritg  31221  dirkercncflem1  31222  dirkercncflem2  31223  dirkercncflem4  31225  fourierdlem43  31269  fourierdlem44  31270  fourierdlem56  31282  fourierdlem57  31283  fourierdlem58  31284  fourierdlem62  31288  fourierdlem66  31292  fourierdlem68  31294  fourierdlem72  31298  fourierdlem76  31302  fourierdlem80  31306  fourierdlem95  31321  fourierdlem103  31329  fourierdlem104  31330  fourierdlem112  31338  sqwvfourb  31349  fourierswlem  31350  numclwwlkovf2ex  31805  2t6m3t4e0  31876  linevalexample  31944  zlmodzxzequap  32056  sinhpcosh  32090  sineq0ALT  32692