Theorem 2cn 10384

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 10383	. 2 |- 2 e. RR
2	1	recni 9390	1 |- 2 e. CC

Syntax hints:   e. wcel 1756   CCcc 9272   2c2 10363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-2 10372

This theorem is referenced by:  2ex  10385  2cnd  10386  2m1e1  10428  3m1e2  10430  2p2e4  10431  times2  10433  2div2e1  10436  1p2e3  10438  3p3e6  10447  4p3e7  10449  5p3e8  10452  6p3e9  10456  7p3e10  10459  2t1e2  10462  2t2e4  10463  3t3e9  10466  2t0e0  10469  4d2e2  10470  2cnne0  10528  halfcn  10533  1mhlfehlf  10536  8th4div3  10537  halfpm6th  10538  2mulicn  10540  2muline0  10541  halfcl  10542  half0  10544  2halves  10545  halfaddsub  10550  zneo  10716  nneo  10717  zeo  10719  4t4e16  10820  6t3e18  10825  7t7e49  10834  8t5e40  10838  9t9e81  10849  decbin0  10850  decbin2  10851  fz0tp  11505  fztpval  11510  fzo0to3tp  11607  expubnd  11916  sq2  11954  cu2  11956  subsq2  11966  binom2sub  11975  binom3  11977  zesq  11979  fac2  12049  fac3  12050  faclbnd2  12059  faclbnd4lem1  12061  faclbnd4lem3  12063  faclbnd4lem4  12064  faclbnd5  12066  bcn2  12087  swrd2lsw  12544  crre  12595  addcj  12629  imval2  12632  sqrlem7  12730  absmax  12809  rddif  12820  sqreulem  12839  amgm2  12849  abs3lemi  12889  iseraltlem2  13152  ackbijnn  13283  climcndslem1  13304  climcndslem2  13305  arisum  13314  arisum2  13315  geo2sum2  13326  geo2lim  13327  geoihalfsum  13334  efcllem  13355  ege2le3  13367  efgt0  13379  tanval2  13409  tanval3  13410  efi4p  13413  efival  13428  sinadd  13440  cosadd  13441  sinmul  13448  cos2tsin  13455  ef01bndlem  13460  cos01bnd  13462  cos1bnd  13463  cos2bnd  13464  cos01gt0  13467  sin02gt0  13468  sin4lt0  13471  znnenlem  13486  sqr2irrlem  13522  odd2np1lem  13583  odd2np1  13584  bits0  13616  bitsfzolem  13622  0bits  13627  bitsinv1  13630  sadcadd  13646  smumullem  13680  opoe  13870  omoe  13871  opeo  13872  omeo  13873  pythagtriplem1  13875  pythagtriplem12  13885  pythagtriplem14  13887  pythagtriplem15  13888  pythagtriplem16  13889  pythagtriplem17  13890  iserodd  13894  prmreclem5  13973  prmreclem6  13974  4sqlem11  14008  4sqlem12  14009  dec5dvds  14085  dec2nprm  14088  decexp2  14096  2exp6  14107  2exp8  14108  2exp16  14109  7prm  14130  11prm  14134  13prm  14135  37prm  14140  43prm  14141  83prm  14142  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  psgnunilem2  15992  efgtlen  16214  efgredleme  16231  frgpnabllem1  16342  lt6abl  16362  htpycc  20532  pcoval2  20568  pcocn  20569  pcohtpylem  20571  pcopt  20574  pcopt2  20575  pcoass  20576  pcorevlem  20578  csbren  20878  minveclem2  20893  ovolunlem1a  20959  ovolunlem1  20960  vitalilem4  21071  mbfi1fseqlem5  21177  dvmptre  21423  dvsincos  21433  aaliou3lem2  21789  aaliou3lem3  21790  aaliou3lem8  21791  coscn  21890  sinhalfpilem  21905  cospi  21914  ef2pi  21919  ef2kpi  21920  efper  21921  sinperlem  21922  sin2kpi  21925  cos2kpi  21926  sin2pim  21927  cos2pim  21928  sinhalfpip  21934  sinhalfpim  21935  coshalfpip  21936  coshalfpim  21937  sincosq3sgn  21942  sincosq4sgn  21943  tangtx  21947  sinq12gt0  21949  sincosq1eq  21954  sincos4thpi  21955  sincos6thpi  21957  sincos3rdpi  21958  pige3  21959  abssinper  21960  coskpi  21962  sineq0  21963  coseq1  21964  efeq1  21965  efif1olem4  21981  eflogeq  22030  tanarg  22048  cxpsqrlem  22127  cxpsqr  22128  logsqr  22129  root1eq1  22173  cxpeq  22175  ang180lem2  22186  ang180lem3  22187  quad2  22214  1cubrlem  22216  1cubr  22217  dcubic2  22219  dcubic1  22220  dcubic  22221  mcubic  22222  cubic2  22223  cubic  22224  dquartlem1  22226  dquartlem2  22227  dquart  22228  quart1lem  22230  quart1  22231  quartlem1  22232  quartlem2  22233  quartlem3  22234  quart  22236  sinasin  22264  asinsin  22267  atancj  22285  efiatan  22287  efiatan2  22292  2efiatan  22293  tanatan  22294  atantan  22298  atanbndlem  22300  atans2  22306  dvatan  22310  atantayl2  22313  leibpilem1  22315  leibpilem2  22316  log2cnv  22319  log2tlbnd  22320  log2ublem2  22322  log2ublem3  22323  log2ub  22324  birthday  22328  basellem1  22398  basellem3  22400  basellem8  22405  basellem9  22406  cht3  22491  1sgm2ppw  22519  ppiub  22523  chtublem  22530  chtub  22531  perfect1  22547  perfectlem1  22548  perfectlem2  22549  perfect  22550  bcmax  22597  bcp1ctr  22598  bclbnd  22599  bpos1lem  22601  bpos1  22602  bposlem1  22603  bposlem2  22604  bposlem4  22606  bposlem5  22607  bposlem6  22608  bposlem8  22610  bposlem9  22611  lgsdir2lem2  22643  lgsquadlem1  22673  lgsquadlem2  22674  lgsquad2lem2  22678  m1lgs  22681  rplogsumlem1  22713  dchrisum0fno1  22740  dchrisum0lem1  22745  dchrisum0lem2  22747  logdivsum  22762  mulog2sumlem3  22765  log2sumbnd  22773  selberglem1  22774  selberglem2  22775  selberg2  22780  selberg4lem1  22789  selberg3r  22798  pntpbnd1a  22814  pntpbnd2  22816  pntibndlem2  22820  pntlemk  22835  ax5seglem7  23149  axlowdimlem13  23168  usgraexvlem  23281  wlkdvspthlem  23474  ex-fl  23622  ipidsq  24076  cncph  24187  ip0i  24193  ip1ilem  24194  ipdirilem  24197  minvecolem2  24244  hvsubcan2i  24434  norm-ii-i  24507  norm3lem  24519  normpar2i  24526  polid2i  24527  hhph  24548  mayete3i  25099  mayete3iOLD  25100  nmcexi  25398  opsqrlem6  25517  addltmulALT  25818  oddpwdc  26706  fib5  26757  ballotlem2  26840  ballotth  26889  zetacvg  26970  problem4  27270  problem5  27271  quad3  27272  4bc2eq6  27360  halfthird  27361  bpoly2  28169  bpoly3  28170  bpoly4  28171  fsumcube  28172  sin2h  28393  cos2h  28394  tan2h  28395  mblfinlem1  28399  mblfinlem2  28400  mblfinlem3  28401  itg2addnclem3  28416  dvasin  28451  areacirc  28460  heiborlem6  28686  rmxluc  29248  rmyluc  29249  jm2.17a  29274  jm2.18  29308  jm2.23  29316  jm3.1lem1  29337  proot1ex  29540  areaquad  29563  lhe4.4ex1a  29574  stoweidlem26  29792  wallispilem4  29834  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  wallispi2  29839  stirlinglem8  29847  stirlinglem11  29850  clwlkisclwwlklem2a4  30417  numclwwlkovf2ex  30650  2t6m3t4e0  30710  linevalexample  30816  zlmodzxzequap  30972  sinhpcosh  31006  sineq0ALT  31602