Theorem 2cn 10607

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 10606	. 2 |- 2 e. RR
2	1	recni 9606	1 |- 2 e. CC

Syntax hints:   e. wcel 1802   CCcc 9488   2c2 10586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rrecex 9562  ax-cnre 9563

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-2 10595

This theorem is referenced by:  2ex  10608  2cnd  10609  2m1e1  10651  3m1e2  10653  2p2e4  10654  times2  10656  2div2e1  10659  1p2e3  10661  3p3e6  10670  4p3e7  10672  5p3e8  10675  6p3e9  10679  7p3e10  10682  2t1e2  10685  2t2e4  10686  3t3e9  10689  2t0e0  10692  4d2e2  10693  2cnne0  10751  halfcn  10756  1mhlfehlf  10759  8th4div3  10760  halfpm6th  10761  2mulicn  10763  2muline0  10764  halfcl  10765  half0  10767  2halves  10768  halfaddsub  10773  zneo  10946  nneo  10947  zeo  10949  4t4e16  11052  6t3e18  11057  7t7e49  11066  8t5e40  11070  9t9e81  11081  decbin0  11082  decbin2  11083  fztpval  11745  fz0tp  11780  fzo0to3tp  11874  expubnd  12200  sq2  12238  cu2  12240  subsq2  12250  binom2sub  12259  binom3  12261  zesq  12263  fac2  12333  fac3  12334  faclbnd2  12343  faclbnd4lem1  12345  faclbnd4lem3  12347  faclbnd4lem4  12348  faclbnd5  12350  bcn2  12371  swrd2lsw  12864  crre  12921  addcj  12955  imval2  12958  sqrlem7  13056  absmax  13136  rddif  13147  sqreulem  13166  amgm2  13176  abs3lemi  13216  iseraltlem2  13479  ackbijnn  13614  climcndslem1  13635  climcndslem2  13636  arisum  13645  arisum2  13646  geo2sum2  13657  geo2lim  13658  geoihalfsum  13665  efcllem  13686  ege2le3  13698  efgt0  13710  tanval2  13740  tanval3  13741  efi4p  13744  efival  13759  sinadd  13771  cosadd  13772  sinmul  13779  cos2tsin  13786  ef01bndlem  13791  cos01bnd  13793  cos1bnd  13794  cos2bnd  13795  cos01gt0  13798  sin02gt0  13799  sin4lt0  13802  znnenlem  13817  sqr2irrlem  13853  odd2np1lem  13917  odd2np1  13918  bits0  13950  bitsfzolem  13956  0bits  13961  bitsinv1  13964  sadcadd  13980  smumullem  14014  opoe  14207  omoe  14208  opeo  14209  omeo  14210  pythagtriplem1  14212  pythagtriplem12  14222  pythagtriplem14  14224  pythagtriplem15  14225  pythagtriplem16  14226  pythagtriplem17  14227  iserodd  14231  prmreclem5  14310  prmreclem6  14311  4sqlem11  14345  4sqlem12  14346  dec5dvds  14422  dec2nprm  14425  decexp2  14433  2exp6OLD  14444  2exp6  14445  2exp8  14446  2exp16  14447  7prm  14468  11prm  14472  13prm  14473  37prm  14478  43prm  14479  83prm  14480  139prm  14481  163prm  14482  317prm  14483  631prm  14484  1259lem1  14485  1259lem2  14486  1259lem3  14487  1259lem4  14488  1259lem5  14489  1259prm  14490  2503lem1  14491  2503lem2  14492  2503lem3  14493  4001lem1  14495  4001lem2  14496  4001lem3  14497  4001lem4  14498  4001prm  14499  psgnunilem2  16389  efgtlen  16613  efgredleme  16630  frgpnabllem1  16746  lt6abl  16766  htpycc  21346  pcoval2  21382  pcocn  21383  pcohtpylem  21385  pcopt  21388  pcopt2  21389  pcoass  21390  pcorevlem  21392  csbren  21692  minveclem2  21707  ovolunlem1a  21773  ovolunlem1  21774  vitalilem4  21886  mbfi1fseqlem5  21992  dvmptre  22238  dvsincos  22248  aaliou3lem2  22604  aaliou3lem3  22605  aaliou3lem8  22606  coscn  22705  sinhalfpilem  22721  cospi  22730  ef2pi  22735  ef2kpi  22736  efper  22737  sinperlem  22738  sin2kpi  22741  cos2kpi  22742  sin2pim  22743  cos2pim  22744  sinhalfpip  22750  sinhalfpim  22751  coshalfpip  22752  coshalfpim  22753  sincosq3sgn  22758  sincosq4sgn  22759  tangtx  22763  sinq12gt0  22765  sincosq1eq  22770  sincos4thpi  22771  sincos6thpi  22773  sincos3rdpi  22774  pige3  22775  abssinper  22776  coskpi  22778  sineq0  22779  coseq1  22780  efeq1  22781  efif1olem4  22797  eflogeq  22851  tanarg  22869  cxpsqrtlem  22948  cxpsqrt  22949  logsqrt  22950  root1eq1  22994  cxpeq  22996  ang180lem2  23007  ang180lem3  23008  quad2  23035  1cubrlem  23037  1cubr  23038  dcubic2  23040  dcubic1  23041  dcubic  23042  mcubic  23043  cubic2  23044  cubic  23045  dquartlem1  23047  dquartlem2  23048  dquart  23049  quart1lem  23051  quart1  23052  quartlem1  23053  quartlem2  23054  quartlem3  23055  quart  23057  sinasin  23085  asinsin  23088  atancj  23106  efiatan  23108  efiatan2  23113  2efiatan  23114  tanatan  23115  atantan  23119  atanbndlem  23121  atans2  23127  dvatan  23131  atantayl2  23134  leibpilem1  23136  leibpilem2  23137  log2cnv  23140  log2tlbnd  23141  log2ublem2  23143  log2ublem3  23144  log2ub  23145  birthday  23149  basellem1  23219  basellem3  23221  basellem8  23226  basellem9  23227  cht3  23312  1sgm2ppw  23340  ppiub  23344  chtublem  23351  chtub  23352  perfect1  23368  perfectlem1  23369  perfectlem2  23370  perfect  23371  bcmax  23418  bcp1ctr  23419  bclbnd  23420  bpos1lem  23422  bpos1  23423  bposlem1  23424  bposlem2  23425  bposlem4  23427  bposlem5  23428  bposlem6  23429  bposlem8  23431  bposlem9  23432  lgsdir2lem2  23464  lgsquadlem1  23494  lgsquadlem2  23495  lgsquad2lem2  23499  m1lgs  23502  rplogsumlem1  23534  dchrisum0fno1  23561  dchrisum0lem1  23566  dchrisum0lem2  23568  logdivsum  23583  mulog2sumlem3  23586  log2sumbnd  23594  selberglem1  23595  selberglem2  23596  selberg2  23601  selberg4lem1  23610  selberg3r  23619  pntpbnd1a  23635  pntpbnd2  23637  pntibndlem2  23641  pntlemk  23656  ax5seglem7  24103  axlowdimlem13  24122  usgraexvlem  24260  wlkdvspthlem  24474  clwlkisclwwlklem2a4  24649  numclwwlkovf2ex  24951  ex-fl  25033  ex-ind-dvds  25035  ipidsq  25488  cncph  25599  ip0i  25605  ip1ilem  25606  ipdirilem  25609  minvecolem2  25656  hvsubcan2i  25846  norm-ii-i  25919  norm3lem  25931  normpar2i  25938  polid2i  25939  hhph  25960  mayete3i  26511  mayete3iOLD  26512  nmcexi  26810  opsqrlem6  26929  addltmulALT  27230  oddpwdc  28159  fib5  28210  ballotlem2  28293  ballotth  28342  zetacvg  28423  problem4  28888  problem5  28889  quad3  28890  4bc2eq6  28978  halfthird  28979  bpoly2  29787  bpoly3  29788  bpoly4  29789  fsumcube  29790  sin2h  30013  cos2h  30014  tan2h  30015  mblfinlem1  30019  mblfinlem2  30020  mblfinlem3  30021  itg2addnclem3  30036  dvasin  30071  areacirc  30080  heiborlem6  30280  rmxluc  30840  rmyluc  30841  jm2.17a  30866  jm2.18  30898  jm2.23  30906  jm3.1lem1  30927  proot1ex  31130  areaquad  31153  lhe4.4ex1a  31203  coskpi2  31569  cosnegpi  31570  cosknegpi  31572  stoweidlem26  31693  wallispilem4  31735  wallispi  31737  wallispi2lem1  31738  stirlinglem8  31748  dirkerper  31763  dirkertrigeqlem3  31767  dirkertrigeq  31768  dirkeritg  31769  dirkercncflem1  31770  dirkercncflem2  31771  fourierdlem57  31831  fourierdlem58  31832  fourierdlem62  31836  fourierdlem76  31850  fourierdlem103  31877  fourierdlem104  31878  sqwvfourb  31897  fourierswlem  31898  0nodd  32331  0even  32437  2even  32439  2zrngamgm  32445  2t6m3t4e0  32645  linevalexample  32706  zlmodzxzequap  32810  sinhpcosh  32844  sineq0ALT  33445