Theorem 2cn 10493

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 10492	. 2 |- 2 e. RR
2	1	recni 9499	1 |- 2 e. CC

Syntax hints:   e. wcel 1758   CCcc 9381   2c2 10472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rrecex 9455  ax-cnre 9456

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-2 10481

This theorem is referenced by:  2ex  10494  2cnd  10495  2m1e1  10537  3m1e2  10539  2p2e4  10540  times2  10542  2div2e1  10545  1p2e3  10547  3p3e6  10556  4p3e7  10558  5p3e8  10561  6p3e9  10565  7p3e10  10568  2t1e2  10571  2t2e4  10572  3t3e9  10575  2t0e0  10578  4d2e2  10579  2cnne0  10637  halfcn  10642  1mhlfehlf  10645  8th4div3  10646  halfpm6th  10647  2mulicn  10649  2muline0  10650  halfcl  10651  half0  10653  2halves  10654  halfaddsub  10659  zneo  10825  nneo  10826  zeo  10828  4t4e16  10929  6t3e18  10934  7t7e49  10943  8t5e40  10947  9t9e81  10958  decbin0  10959  decbin2  10960  fz0tp  11614  fztpval  11619  fzo0to3tp  11716  expubnd  12025  sq2  12063  cu2  12065  subsq2  12075  binom2sub  12084  binom3  12086  zesq  12088  fac2  12158  fac3  12159  faclbnd2  12168  faclbnd4lem1  12170  faclbnd4lem3  12172  faclbnd4lem4  12173  faclbnd5  12175  bcn2  12196  swrd2lsw  12654  crre  12705  addcj  12739  imval2  12742  sqrlem7  12840  absmax  12919  rddif  12930  sqreulem  12949  amgm2  12959  abs3lemi  12999  iseraltlem2  13262  ackbijnn  13393  climcndslem1  13414  climcndslem2  13415  arisum  13424  arisum2  13425  geo2sum2  13436  geo2lim  13437  geoihalfsum  13444  efcllem  13465  ege2le3  13477  efgt0  13489  tanval2  13519  tanval3  13520  efi4p  13523  efival  13538  sinadd  13550  cosadd  13551  sinmul  13558  cos2tsin  13565  ef01bndlem  13570  cos01bnd  13572  cos1bnd  13573  cos2bnd  13574  cos01gt0  13577  sin02gt0  13578  sin4lt0  13581  znnenlem  13596  sqr2irrlem  13632  odd2np1lem  13693  odd2np1  13694  bits0  13726  bitsfzolem  13732  0bits  13737  bitsinv1  13740  sadcadd  13756  smumullem  13790  opoe  13980  omoe  13981  opeo  13982  omeo  13983  pythagtriplem1  13985  pythagtriplem12  13995  pythagtriplem14  13997  pythagtriplem15  13998  pythagtriplem16  13999  pythagtriplem17  14000  iserodd  14004  prmreclem5  14083  prmreclem6  14084  4sqlem11  14118  4sqlem12  14119  dec5dvds  14195  dec2nprm  14198  decexp2  14206  2exp6  14217  2exp8  14218  2exp16  14219  7prm  14240  11prm  14244  13prm  14245  37prm  14250  43prm  14251  83prm  14252  139prm  14253  163prm  14254  317prm  14255  631prm  14256  1259lem1  14257  1259lem2  14258  1259lem3  14259  1259lem4  14260  1259lem5  14261  1259prm  14262  2503lem1  14263  2503lem2  14264  2503lem3  14265  4001lem1  14267  4001lem2  14268  4001lem3  14269  4001lem4  14270  4001prm  14271  psgnunilem2  16103  efgtlen  16327  efgredleme  16344  frgpnabllem1  16455  lt6abl  16475  htpycc  20668  pcoval2  20704  pcocn  20705  pcohtpylem  20707  pcopt  20710  pcopt2  20711  pcoass  20712  pcorevlem  20714  csbren  21014  minveclem2  21029  ovolunlem1a  21095  ovolunlem1  21096  vitalilem4  21207  mbfi1fseqlem5  21313  dvmptre  21559  dvsincos  21569  aaliou3lem2  21925  aaliou3lem3  21926  aaliou3lem8  21927  coscn  22026  sinhalfpilem  22041  cospi  22050  ef2pi  22055  ef2kpi  22056  efper  22057  sinperlem  22058  sin2kpi  22061  cos2kpi  22062  sin2pim  22063  cos2pim  22064  sinhalfpip  22070  sinhalfpim  22071  coshalfpip  22072  coshalfpim  22073  sincosq3sgn  22078  sincosq4sgn  22079  tangtx  22083  sinq12gt0  22085  sincosq1eq  22090  sincos4thpi  22091  sincos6thpi  22093  sincos3rdpi  22094  pige3  22095  abssinper  22096  coskpi  22098  sineq0  22099  coseq1  22100  efeq1  22101  efif1olem4  22117  eflogeq  22166  tanarg  22184  cxpsqrlem  22263  cxpsqr  22264  logsqr  22265  root1eq1  22309  cxpeq  22311  ang180lem2  22322  ang180lem3  22323  quad2  22350  1cubrlem  22352  1cubr  22353  dcubic2  22355  dcubic1  22356  dcubic  22357  mcubic  22358  cubic2  22359  cubic  22360  dquartlem1  22362  dquartlem2  22363  dquart  22364  quart1lem  22366  quart1  22367  quartlem1  22368  quartlem2  22369  quartlem3  22370  quart  22372  sinasin  22400  asinsin  22403  atancj  22421  efiatan  22423  efiatan2  22428  2efiatan  22429  tanatan  22430  atantan  22434  atanbndlem  22436  atans2  22442  dvatan  22446  atantayl2  22449  leibpilem1  22451  leibpilem2  22452  log2cnv  22455  log2tlbnd  22456  log2ublem2  22458  log2ublem3  22459  log2ub  22460  birthday  22464  basellem1  22534  basellem3  22536  basellem8  22541  basellem9  22542  cht3  22627  1sgm2ppw  22655  ppiub  22659  chtublem  22666  chtub  22667  perfect1  22683  perfectlem1  22684  perfectlem2  22685  perfect  22686  bcmax  22733  bcp1ctr  22734  bclbnd  22735  bpos1lem  22737  bpos1  22738  bposlem1  22739  bposlem2  22740  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem8  22746  bposlem9  22747  lgsdir2lem2  22779  lgsquadlem1  22809  lgsquadlem2  22810  lgsquad2lem2  22814  m1lgs  22817  rplogsumlem1  22849  dchrisum0fno1  22876  dchrisum0lem1  22881  dchrisum0lem2  22883  logdivsum  22898  mulog2sumlem3  22901  log2sumbnd  22909  selberglem1  22910  selberglem2  22911  selberg2  22916  selberg4lem1  22925  selberg3r  22934  pntpbnd1a  22950  pntpbnd2  22952  pntibndlem2  22956  pntlemk  22971  ax5seglem7  23316  axlowdimlem13  23335  usgraexvlem  23448  wlkdvspthlem  23641  ex-fl  23789  ipidsq  24243  cncph  24354  ip0i  24360  ip1ilem  24361  ipdirilem  24364  minvecolem2  24411  hvsubcan2i  24601  norm-ii-i  24674  norm3lem  24686  normpar2i  24693  polid2i  24694  hhph  24715  mayete3i  25266  mayete3iOLD  25267  nmcexi  25565  opsqrlem6  25684  addltmulALT  25985  oddpwdc  26871  fib5  26922  ballotlem2  27005  ballotth  27054  zetacvg  27135  problem4  27435  problem5  27436  quad3  27437  4bc2eq6  27525  halfthird  27526  bpoly2  28334  bpoly3  28335  bpoly4  28336  fsumcube  28337  sin2h  28560  cos2h  28561  tan2h  28562  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  itg2addnclem3  28583  dvasin  28618  areacirc  28627  heiborlem6  28853  rmxluc  29415  rmyluc  29416  jm2.17a  29441  jm2.18  29475  jm2.23  29483  jm3.1lem1  29504  proot1ex  29707  areaquad  29730  lhe4.4ex1a  29741  stoweidlem26  29959  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  wallispi2lem2  30005  wallispi2  30006  stirlinglem8  30014  stirlinglem11  30017  clwlkisclwwlklem2a4  30584  numclwwlkovf2ex  30817  2t6m3t4e0  30878  linevalexample  31002  zlmodzxzequap  31148  sinhpcosh  31371  sineq0ALT  31973