Theorem 2cn 12251

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
2cn	⊢ 2 ∈ ℂ

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		df-2 12239	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11092	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11147	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2837	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2121  (class class class)co 7359  ℂcc 11032  1c1 11035   + caddc 11037  2c2 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-addcl 11094

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-2 12239

This theorem is referenced by:  2ex  12253  2cnd  12254  3cn  12257  2m1e1  12297  3m1e2  12299  2p2e4  12306  times2  12308  2div2e1  12312  1p2e3ALT  12315  3p3e6  12323  4p3e7  12325  5p3e8  12328  6p3e9  12331  2t1e2  12334  2t2e4  12335  3t3e9  12338  2t0e0  12340  4div2e2  12341  2cnne0  12381  halfcn  12386  2halves  12390  8th4div3  12392  halfthird  12393  halfpm6th  12394  2mulicn  12396  2muline0  12397  halfcl  12398  half0  12400  halfaddsub  12405  div4p1lem1div2  12427  3halfnz  12603  zneo  12607  nneo  12608  zeo  12610  7p3e10  12714  4t4e16  12738  6t3e18  12744  7t7e49  12753  8t5e40  12757  9t9e81  12768  decbin0  12779  decbin2  12780  fztpval  13535  fz0tp  13577  fzo0to3tp  13702  fzo1to4tp  13704  expubnd  14135  sq2  14154  sq4e2t8  14156  cu2  14157  subsq2  14168  binom2sub  14177  binom3  14181  zesq  14183  fac2  14236  fac3  14237  faclbnd2  14248  faclbnd4lem1  14250  faclbnd4lem3  14252  faclbnd4lem4  14253  faclbnd5  14255  bcn2  14276  4bc2eq6  14286  swrd2lsw  14909  crre  15071  addcj  15105  imval2  15108  01sqrexlem7  15205  absmax  15287  rddif  15298  sqreulem  15317  amgm2  15327  abs3lemi  15368  iseraltlem2  15640  ackbijnn  15788  climcndslem1  15809  climcndslem2  15810  arisum  15820  arisum2  15821  geo2sum2  15834  geo2lim  15835  geoihalfsum  15842  bpoly2  16017  bpoly3  16018  bpoly4  16019  fsumcube  16020  efcllem  16037  ege2le3  16050  efgt0  16065  tanval2  16095  tanval3  16096  efi4p  16099  efival  16114  sinadd  16126  cosadd  16127  sinmul  16134  cos2tsin  16141  ef01bndlem  16146  cos01bnd  16148  cos1bnd  16149  cos2bnd  16150  cos01gt0  16153  sin02gt0  16154  sin4lt0  16157  odd2np1lem  16304  odd2np1  16305  opoe  16327  omoe  16328  opeo  16329  omeo  16330  nno  16346  nn0o  16347  flodddiv4  16379  bits0  16392  bitsfzolem  16398  0bits  16403  bitsinv1  16406  sadcadd  16422  smumullem  16456  6gcd4e2  16502  3lcm2e6woprm  16579  6lcm4e12  16580  pythagtriplem1  16782  pythagtriplem12  16792  pythagtriplem14  16794  pythagtriplem15  16795  pythagtriplem16  16796  pythagtriplem17  16797  iserodd  16801  prmreclem5  16886  prmreclem6  16887  4sqlem11  16921  4sqlem12  16922  prmo2  17006  prmo3  17007  dec5dvds  17030  dec2nprm  17033  2exp5  17051  2exp6  17052  2exp7  17053  2exp8  17054  2exp11  17055  2exp16  17056  7prm  17076  11prm  17080  13prm  17081  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  psgnunilem2  19464  efgtlen  19695  efgredleme  19712  frgpnabllem1  19842  lt6abl  19864  htpycc  24968  pcoval2  25004  pcocn  25005  pcohtpylem  25007  pcopt  25010  pcopt2  25011  pcoass  25012  pcorevlem  25014  csbren  25387  minveclem2  25414  ovolunlem1a  25484  ovolunlem1  25485  vitalilem4  25599  mbfi1fseqlem5  25707  dvmptre  25957  dvsincos  25969  aaliou3lem2  26330  aaliou3lem3  26331  aaliou3lem8  26332  coscn  26431  sinhalfpilem  26448  cospi  26457  ef2pi  26462  ef2kpi  26463  efper  26464  sinperlem  26465  sin2kpi  26468  cos2kpi  26469  sin2pim  26470  cos2pim  26471  sincosq3sgn  26485  sincosq4sgn  26486  tangtx  26490  sinq12gt0  26492  sincosq1eq  26497  sincos4thpi  26498  sincos6thpi  26501  sincos3rdpi  26502  pige3ALT  26505  abssinper  26506  coskpi  26508  sineq0  26509  coseq1  26510  efeq1  26513  efif1olem4  26530  eflogeq  26587  tanarg  26604  cxpsqrtlem  26687  cxpsqrt  26688  logsqrt  26689  2irrexpq  26716  root1eq1  26740  cxpeq  26742  2logb9irrALT  26783  sqrt2cxp2logb9e3  26784  ang180lem2  26795  ang180lem3  26796  quad2  26824  1cubrlem  26826  1cubr  26827  dcubic2  26829  dcubic1  26830  dcubic  26831  mcubic  26832  cubic2  26833  cubic  26834  dquartlem1  26836  dquartlem2  26837  dquart  26838  quart1lem  26840  quart1  26841  quartlem1  26842  quartlem2  26843  quartlem3  26844  quart  26846  sinasin  26874  asinsin  26877  atancj  26895  efiatan  26897  efiatan2  26902  2efiatan  26903  tanatan  26904  atantan  26908  atanbndlem  26910  atans2  26916  dvatan  26920  atantayl2  26923  leibpilem2  26926  log2cnv  26929  log2tlbnd  26930  log2ublem2  26932  log2ublem3  26933  log2ub  26934  birthday  26939  zetacvg  26999  basellem1  27065  basellem3  27067  basellem8  27072  basellem9  27073  cht3  27157  1sgm2ppw  27184  ppiub  27188  chtublem  27195  chtub  27196  perfect1  27212  perfectlem1  27213  perfectlem2  27214  perfect  27215  bcmax  27262  bcp1ctr  27263  bclbnd  27264  bpos1lem  27266  bpos1  27267  bposlem1  27268  bposlem2  27269  bposlem4  27271  bposlem5  27272  bposlem6  27273  bposlem8  27275  bposlem9  27276  lgsdir2lem2  27310  gausslemma2dlem6  27356  lgsquadlem1  27364  lgsquadlem2  27365  lgsquad2lem2  27369  m1lgs  27372  2lgslem3a  27380  2lgslem3b  27381  2lgslem3c  27382  2lgslem3d  27383  2lgsoddprmlem2  27393  2lgsoddprmlem3c  27396  2lgsoddprmlem3d  27397  addsqnreup  27427  addsq2nreurex  27428  rplogsumlem1  27468  dchrisum0fno1  27495  dchrisum0lem1  27500  dchrisum0lem2  27502  logdivsum  27517  mulog2sumlem3  27520  log2sumbnd  27528  selberglem1  27529  selberglem2  27530  selberg2  27535  selberg4lem1  27544  selberg3r  27553  pntpbnd1a  27569  pntpbnd2  27571  pntibndlem2  27575  pntlemk  27590  ax5seglem7  29024  axlowdimlem13  29043  elwspths2spth  30058  clwlkclwwlklem2a4  30087  clwwlknonex2  30199  2clwwlk2  30438  numclwlk1lem1  30459  ex-fl  30537  ex-ceil  30538  ex-exp  30540  ex-fac  30541  ex-abs  30545  ex-ind-dvds  30551  ipidsq  30801  cncph  30910  ip0i  30916  ip1ilem  30917  ipdirilem  30920  minvecolem2  30966  hvsubcan2i  31155  norm-ii-i  31228  norm3lem  31240  normpar2i  31247  polid2i  31248  hhph  31269  mayete3i  31819  nmcexi  32117  opsqrlem6  32236  addltmulALT  32537  ply1dg3rt0irred  33677  fldext2chn  33922  constrelextdg2  33941  2sqr3minply  33974  cos9thpiminplylem4  33979  cos9thpiminplylem5  33980  omssubadd  34494  oddpwdc  34548  fib5  34599  ballotlem2  34683  ballotth  34732  efmul2picn  34790  itgexpif  34800  vtscl  34832  circlemeth  34834  hgt750lemd  34842  logdivsqrle  34844  hgt750lem  34845  hgt750lem2  34846  problem4  35909  problem5  35910  quad3  35911  cnndvlem1  36856  sin2h  37990  cos2h  37991  tan2h  37992  poimirlem29  38029  mblfinlem1  38037  mblfinlem2  38038  mblfinlem3  38039  itg2addnclem3  38053  dvasin  38084  areacirc  38093  heiborlem6  38196  12gcd5e1  42501  12lcm5e60  42506  60lcm7e420  42508  420lcm8e840  42509  3exp7  42551  3lexlogpow5ineq1  42552  3lexlogpow2ineq2  42557  3lexlogpow5ineq5  42558  aks4d1p1p5  42573  aks4d1p1  42574  posbezout  42598  facp2  42641  1p3e4  42755  sqn5i  42775  235t711  42795  ex-decpmul  42796  cxp112d  42831  cxp111d  42832  cxpi11d  42833  tanhalfpim  42839  fltne  43107  flt4lem5e  43119  sum9cubes  43135  3cubeslem3l  43148  3cubeslem3r  43149  rmxluc  43394  rmyluc  43395  jm2.17a  43418  jm2.18  43446  jm2.23  43454  jm3.1lem1  43475  proot1ex  43654  areaquad  43674  sqrtcval  44098  resqrtvalex  44102  lhe4.4ex1a  44786  sineq0ALT  45393  coskpi2  46321  cosnegpi  46322  cosknegpi  46324  stoweidlem26  46481  wallispilem4  46523  wallispi  46525  wallispi2lem1  46526  stirlinglem8  46536  dirkerper  46551  dirkertrigeqlem3  46555  dirkertrigeq  46556  dirkeritg  46557  dirkercncflem1  46558  dirkercncflem2  46559  fourierdlem57  46618  fourierdlem58  46619  fourierdlem62  46623  fourierdlem76  46637  fourierdlem103  46664  fourierdlem104  46665  sqwvfourb  46684  fourierswlem  46685  nthrucw  47343  sin5tlem1  47348  sin5tlem5  47352  cos5t  47354  goldrasin  47357  goldracos5teq  47360  goldratmolem2  47361  rehalfge1  47814  ceil5half3  47821  modm2nep1  47847  modm1nep2  47849  modm1nem2  47850  fmtnoge3  48020  fmtnorec1  48027  fmtno0  48030  fmtno1  48031  fmtnorec3  48038  fmtnorec4  48039  fmtno5lem2  48044  fmtno5lem4  48046  257prm  48051  fmtnoprmfac2lem1  48056  fmtno4prmfac  48062  fmtno5faclem2  48070  fmtno5faclem3  48071  fmtno5fac  48072  139prmALT  48086  31prm  48087  127prm  48089  mod42tp1mod8  48092  lighneallem2  48096  lighneallem3  48097  lighneallem4a  48098  3exp4mod41  48106  41prothprmlem1  48107  41prothprmlem2  48108  41prothprm  48109  bits0ALTV  48182  0evenALTV  48191  6even  48214  8even  48216  perfectALTVlem1  48224  perfectALTVlem2  48225  perfectALTV  48226  2exp340mod341  48236  8exp8mod9  48239  mogoldbb  48288  nnsum3primes4  48291  bgoldbtbndlem1  48308  gpg5order  48563  gpg5edgnedg  48633  0nodd  48673  0even  48740  2even  48742  2zrngamgm  48748  2t6m3t4e0  48851  linevalexample  48898  zlmodzxzequap  49002  pw2m1lepw2m1  49023  nnlog2ge0lt1  49069  logbpw2m1  49070  nnpw2blen  49083  nnpw2pmod  49086  blen1  49087  blen2  49088  blennnt2  49092  nnolog2flm1  49093  0dig2nn0e  49115  0dig2nn0o  49116  nn0sumshdiglemA  49122  nn0sumshdiglemB  49123  nn0sumshdiglem1  49124  nn0sumshdiglem2  49125  ackval1012  49193  ackval2012  49194  ackval3012  49195  ackval42  49199  sinhpcosh  50242