Theorem 2cn 11091

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	⊢ 2 ∈ ℂ

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 11090	. 2 ⊢ 2 ∈ ℝ
2	1	recni 10052	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 1990  ℂcc 9934  2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-2 11079

This theorem is referenced by:  2ex  11092  2cnd  11093  2m1e1  11135  3m1e2  11137  2p2e4  11144  times2  11146  2div2e1  11150  1p2e3  11152  3p3e6  11161  4p3e7  11163  5p3e8  11166  6p3e9  11170  7p3e10OLD  11173  2t1e2  11176  2t2e4  11177  3t3e9  11180  2t0e0  11183  4d2e2  11184  2cnne0  11242  halfcn  11247  1mhlfehlf  11251  8th4div3  11252  halfpm6th  11253  2mulicn  11255  2muline0  11256  halfcl  11257  half0  11259  2halves  11260  halfaddsub  11265  div4p1lem1div2  11287  3halfnz  11456  zneo  11460  nneo  11461  zeo  11463  7p3e10  11603  4t4e16  11633  6t3e18  11642  7t7e49  11653  8t5e40  11657  8t5e40OLD  11658  9t9e81  11670  decbin0  11682  decbin2  11683  halfthird  11685  fztpval  12402  fz0tp  12440  fz0to4untppr  12442  fzo0to3tp  12554  fzo1to4tp  12556  expubnd  12921  sq2  12960  sq4e2t8  12962  cu2  12963  subsq2  12973  binom2sub  12981  binom3  12985  zesq  12987  fac2  13066  fac3  13067  faclbnd2  13078  faclbnd4lem1  13080  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd5  13085  bcn2  13106  4bc2eq6  13116  swrd2lsw  13695  crre  13854  addcj  13888  imval2  13891  sqrlem7  13989  absmax  14069  rddif  14080  sqreulem  14099  amgm2  14109  abs3lemi  14149  iseraltlem2  14413  ackbijnn  14560  climcndslem1  14581  climcndslem2  14582  arisum  14592  arisum2  14593  geo2sum2  14605  geo2lim  14606  geoihalfsum  14614  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  efcllem  14808  ege2le3  14820  efgt0  14833  tanval2  14863  tanval3  14864  efi4p  14867  efival  14882  sinadd  14894  cosadd  14895  sinmul  14902  cos2tsin  14909  ef01bndlem  14914  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  cos01gt0  14921  sin02gt0  14922  sin4lt0  14925  znnenlem  14940  sqrt2irrlemOLD  14978  odd2np1lem  15064  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  nno  15098  nn0o  15099  flodddiv4  15137  bits0  15150  bitsfzolem  15156  0bits  15161  bitsinv1  15164  sadcadd  15180  smumullem  15214  6gcd4e2  15255  3lcm2e6woprm  15328  6lcm4e12  15329  pythagtriplem1  15521  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem15  15534  pythagtriplem16  15535  pythagtriplem17  15536  iserodd  15540  prmreclem5  15624  prmreclem6  15625  4sqlem11  15659  4sqlem12  15660  prmo2  15744  prmo3  15745  dec5dvds  15768  dec2nprm  15771  decexp2  15779  2exp6  15795  2exp8  15796  2exp16  15797  7prm  15817  11prm  15822  13prm  15823  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  psgnunilem2  17915  efgtlen  18139  efgredleme  18156  frgpnabllem1  18276  lt6abl  18296  htpycc  22779  pcoval2  22816  pcocn  22817  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  csbren  23182  minveclem2  23197  ovolunlem1a  23264  ovolunlem1  23265  vitalilem4  23380  mbfi1fseqlem5  23486  dvmptre  23732  dvsincos  23744  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem8  24100  coscn  24199  sinhalfpilem  24215  cospi  24224  ef2pi  24229  ef2kpi  24230  efper  24231  sinperlem  24232  sin2kpi  24235  cos2kpi  24236  sin2pim  24237  cos2pim  24238  sinhalfpip  24244  sinhalfpim  24245  coshalfpip  24246  coshalfpim  24247  sincosq3sgn  24252  sincosq4sgn  24253  tangtx  24257  sinq12gt0  24259  sincosq1eq  24264  sincos4thpi  24265  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  abssinper  24270  coskpi  24272  sineq0  24273  coseq1  24274  efeq1  24275  efif1olem4  24291  eflogeq  24348  tanarg  24365  cxpsqrtlem  24448  cxpsqrt  24449  logsqrt  24450  root1eq1  24496  cxpeq  24498  ang180lem2  24540  ang180lem3  24541  quad2  24566  1cubrlem  24568  1cubr  24569  dcubic2  24571  dcubic1  24572  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1lem  24582  quart1  24583  quartlem1  24584  quartlem2  24585  quartlem3  24586  quart  24588  sinasin  24616  asinsin  24619  atancj  24637  efiatan  24639  efiatan2  24644  2efiatan  24645  tanatan  24646  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl2  24665  leibpilem1  24667  leibpilem2  24668  log2cnv  24671  log2tlbnd  24672  log2ublem2  24674  log2ublem3  24675  log2ub  24676  birthday  24681  zetacvg  24741  basellem1  24807  basellem3  24809  basellem8  24814  basellem9  24815  cht3  24899  1sgm2ppw  24925  ppiub  24929  chtublem  24936  chtub  24937  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  bcmax  25003  bcp1ctr  25004  bclbnd  25005  bpos1lem  25007  bpos1  25008  bposlem1  25009  bposlem2  25010  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem8  25016  bposlem9  25017  lgsdir2lem2  25051  gausslemma2dlem6  25097  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem2  25110  m1lgs  25113  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgsoddprmlem2  25134  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  rplogsumlem1  25173  dchrisum0fno1  25200  dchrisum0lem1  25205  dchrisum0lem2  25207  logdivsum  25222  mulog2sumlem3  25225  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberg2  25240  selberg4lem1  25249  selberg3r  25258  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemk  25295  ax5seglem7  25815  axlowdimlem13  25834  elwspths2spth  26862  clwlkclwwlklem2a4  26898  numclwwlkovf2ex  27219  ex-fl  27304  ex-ceil  27305  ex-exp  27307  ex-fac  27308  ex-abs  27312  ex-ind-dvds  27318  ipidsq  27565  cncph  27674  ip0i  27680  ip1ilem  27681  ipdirilem  27684  minvecolem2  27731  hvsubcan2i  27921  norm-ii-i  27994  norm3lem  28006  normpar2i  28013  polid2i  28014  hhph  28035  mayete3i  28587  nmcexi  28885  opsqrlem6  29004  addltmulALT  29305  omssubadd  30362  oddpwdc  30416  fib5  30467  ballotlem2  30550  ballotth  30599  efmul2picn  30674  itgexpif  30684  vtscl  30716  circlemeth  30718  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  hgt750lem2  30730  problem4  31562  problem5  31563  quad3  31564  cnndvlem1  32528  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem29  33438  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  itg2addnclem3  33463  dvasin  33496  areacirc  33505  heiborlem6  33615  rmxluc  37501  rmyluc  37502  jm2.17a  37527  jm2.18  37555  jm2.23  37563  jm3.1lem1  37584  proot1ex  37779  areaquad  37802  lhe4.4ex1a  38528  sineq0ALT  39173  coskpi2  40077  cosnegpi  40078  cosknegpi  40080  stoweidlem26  40243  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  stirlinglem8  40298  dirkerper  40313  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem76  40399  fourierdlem103  40426  fourierdlem104  40427  sqwvfourb  40446  fourierswlem  40447  fmtnoge3  41442  fmtnorec1  41449  fmtno0  41452  fmtno1  41453  fmtnorec3  41460  fmtnorec4  41461  fmtno5lem2  41466  fmtno5lem4  41468  257prm  41473  fmtnoprmfac2lem1  41478  fmtno4prmfac  41484  fmtno5faclem2  41492  fmtno5faclem3  41493  fmtno5fac  41494  2exp5  41507  139prmALT  41511  31prm  41512  2exp7  41514  127prm  41515  2exp11  41517  mod42tp1mod8  41519  lighneallem2  41523  lighneallem3  41524  lighneallem4a  41525  3exp4mod41  41533  41prothprmlem1  41534  41prothprmlem2  41535  41prothprm  41536  bits0ALTV  41590  0evenALTV  41599  6even  41620  8even  41622  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  mogoldbb  41673  nnsum3primes4  41676  bgoldbtbndlem1  41693  0nodd  41810  0even  41931  2even  41933  2zrngamgm  41939  2t6m3t4e0  42126  linevalexample  42184  zlmodzxzequap  42288  pw2m1lepw2m1  42310  nnlog2ge0lt1  42360  logbpw2m1  42361  nnpw2blen  42374  nnpw2pmod  42377  blen1  42378  blen2  42379  blennnt2  42383  nnolog2flm1  42384  0dig2nn0e  42406  0dig2nn0o  42407  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  nn0sumshdiglem2  42416  sinhpcosh  42481