Theorem 2cn 12228

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 12216	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11109	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11161	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2834	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7357  ℂcc 11049  1c1 11052   + caddc 11054  2c2 12208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11109  ax-addcl 11111

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814  df-2 12216

This theorem is referenced by:  2ex  12230  2cnd  12231  3cn  12234  2m1e1  12279  3m1e2  12281  2p2e4  12288  times2  12290  2div2e1  12294  1p2e3ALT  12297  3p3e6  12305  4p3e7  12307  5p3e8  12310  6p3e9  12313  2t1e2  12316  2t2e4  12317  3t3e9  12320  2t0e0  12322  4d2e2  12323  2cnne0  12363  halfcn  12368  1mhlfehlf  12372  8th4div3  12373  halfpm6th  12374  2mulicn  12376  2muline0  12377  halfcl  12378  half0  12380  2halves  12381  halfaddsub  12386  div4p1lem1div2  12408  3halfnz  12582  zneo  12586  nneo  12587  zeo  12589  7p3e10  12693  4t4e16  12717  6t3e18  12723  7t7e49  12732  8t5e40  12736  9t9e81  12747  decbin0  12758  decbin2  12759  halfthird  12761  fztpval  13503  fz0tp  13542  fz0to4untppr  13544  fzo0to3tp  13658  fzo1to4tp  13660  expubnd  14082  sq2  14101  sq4e2t8  14103  cu2  14104  subsq2  14115  binom2sub  14123  binom3  14127  zesq  14129  fac2  14179  fac3  14180  faclbnd2  14191  faclbnd4lem1  14193  faclbnd4lem3  14195  faclbnd4lem4  14196  faclbnd5  14198  bcn2  14219  4bc2eq6  14229  swrd2lsw  14841  crre  14999  addcj  15033  imval2  15036  01sqrexlem7  15133  absmax  15214  rddif  15225  sqreulem  15244  amgm2  15254  abs3lemi  15295  iseraltlem2  15567  ackbijnn  15713  climcndslem1  15734  climcndslem2  15735  arisum  15745  arisum2  15746  geo2sum2  15759  geo2lim  15760  geoihalfsum  15767  bpoly2  15940  bpoly3  15941  bpoly4  15942  fsumcube  15943  efcllem  15960  ege2le3  15972  efgt0  15985  tanval2  16015  tanval3  16016  efi4p  16019  efival  16034  sinadd  16046  cosadd  16047  sinmul  16054  cos2tsin  16061  ef01bndlem  16066  cos01bnd  16068  cos1bnd  16069  cos2bnd  16070  cos01gt0  16073  sin02gt0  16074  sin4lt0  16077  odd2np1lem  16222  odd2np1  16223  opoe  16245  omoe  16246  opeo  16247  omeo  16248  nno  16264  nn0o  16265  flodddiv4  16295  bits0  16308  bitsfzolem  16314  0bits  16319  bitsinv1  16322  sadcadd  16338  smumullem  16372  6gcd4e2  16419  3lcm2e6woprm  16491  6lcm4e12  16492  pythagtriplem1  16688  pythagtriplem12  16698  pythagtriplem14  16700  pythagtriplem15  16701  pythagtriplem16  16702  pythagtriplem17  16703  iserodd  16707  prmreclem5  16792  prmreclem6  16793  4sqlem11  16827  4sqlem12  16828  prmo2  16912  prmo3  16913  dec5dvds  16936  dec2nprm  16939  decexp2  16947  2exp5  16958  2exp6  16959  2exp7  16960  2exp8  16961  2exp11  16962  2exp16  16963  7prm  16983  11prm  16987  13prm  16988  37prm  16993  43prm  16994  83prm  16995  139prm  16996  163prm  16997  317prm  16998  631prm  16999  1259lem1  17003  1259lem2  17004  1259lem3  17005  1259lem4  17006  1259lem5  17007  1259prm  17008  2503lem1  17009  2503lem2  17010  2503lem3  17011  4001lem1  17013  4001lem2  17014  4001lem3  17015  4001lem4  17016  4001prm  17017  psgnunilem2  19277  efgtlen  19508  efgredleme  19525  frgpnabllem1  19651  lt6abl  19672  htpycc  24343  pcoval2  24379  pcocn  24380  pcohtpylem  24382  pcopt  24385  pcopt2  24386  pcoass  24387  pcorevlem  24389  csbren  24763  minveclem2  24790  ovolunlem1a  24860  ovolunlem1  24861  vitalilem4  24975  mbfi1fseqlem5  25084  dvmptre  25333  dvsincos  25345  aaliou3lem2  25703  aaliou3lem3  25704  aaliou3lem8  25705  coscn  25804  sinhalfpilem  25820  cospi  25829  ef2pi  25834  ef2kpi  25835  efper  25836  sinperlem  25837  sin2kpi  25840  cos2kpi  25841  sin2pim  25842  cos2pim  25843  sincosq3sgn  25857  sincosq4sgn  25858  tangtx  25862  sinq12gt0  25864  sincosq1eq  25869  sincos4thpi  25870  sincos6thpi  25872  sincos3rdpi  25873  pige3ALT  25876  abssinper  25877  coskpi  25879  sineq0  25880  coseq1  25881  efeq1  25884  efif1olem4  25901  eflogeq  25957  tanarg  25974  cxpsqrtlem  26057  cxpsqrt  26058  logsqrt  26059  2irrexpq  26085  root1eq1  26108  cxpeq  26110  2logb9irrALT  26148  sqrt2cxp2logb9e3  26149  ang180lem2  26160  ang180lem3  26161  quad2  26189  1cubrlem  26191  1cubr  26192  dcubic2  26194  dcubic1  26195  dcubic  26196  mcubic  26197  cubic2  26198  cubic  26199  dquartlem1  26201  dquartlem2  26202  dquart  26203  quart1lem  26205  quart1  26206  quartlem1  26207  quartlem2  26208  quartlem3  26209  quart  26211  sinasin  26239  asinsin  26242  atancj  26260  efiatan  26262  efiatan2  26267  2efiatan  26268  tanatan  26269  atantan  26273  atanbndlem  26275  atans2  26281  dvatan  26285  atantayl2  26288  leibpilem2  26291  log2cnv  26294  log2tlbnd  26295  log2ublem2  26297  log2ublem3  26298  log2ub  26299  birthday  26304  zetacvg  26364  basellem1  26430  basellem3  26432  basellem8  26437  basellem9  26438  cht3  26522  1sgm2ppw  26548  ppiub  26552  chtublem  26559  chtub  26560  perfect1  26576  perfectlem1  26577  perfectlem2  26578  perfect  26579  bcmax  26626  bcp1ctr  26627  bclbnd  26628  bpos1lem  26630  bpos1  26631  bposlem1  26632  bposlem2  26633  bposlem4  26635  bposlem5  26636  bposlem6  26637  bposlem8  26639  bposlem9  26640  lgsdir2lem2  26674  gausslemma2dlem6  26720  lgsquadlem1  26728  lgsquadlem2  26729  lgsquad2lem2  26733  m1lgs  26736  2lgslem3a  26744  2lgslem3b  26745  2lgslem3c  26746  2lgslem3d  26747  2lgsoddprmlem2  26757  2lgsoddprmlem3c  26760  2lgsoddprmlem3d  26761  addsqnreup  26791  addsq2nreurex  26792  rplogsumlem1  26832  dchrisum0fno1  26859  dchrisum0lem1  26864  dchrisum0lem2  26866  logdivsum  26881  mulog2sumlem3  26884  log2sumbnd  26892  selberglem1  26893  selberglem2  26894  selberg2  26899  selberg4lem1  26908  selberg3r  26917  pntpbnd1a  26933  pntpbnd2  26935  pntibndlem2  26939  pntlemk  26954  ax5seglem7  27884  axlowdimlem13  27903  elwspths2spth  28912  clwlkclwwlklem2a4  28941  clwwlknonex2  29053  2clwwlk2  29292  numclwlk1lem1  29313  ex-fl  29391  ex-ceil  29392  ex-exp  29394  ex-fac  29395  ex-abs  29399  ex-ind-dvds  29405  ipidsq  29652  cncph  29761  ip0i  29767  ip1ilem  29768  ipdirilem  29771  minvecolem2  29817  hvsubcan2i  30006  norm-ii-i  30079  norm3lem  30091  normpar2i  30098  polid2i  30099  hhph  30120  mayete3i  30670  nmcexi  30968  opsqrlem6  31087  addltmulALT  31388  omssubadd  32900  oddpwdc  32954  fib5  33005  ballotlem2  33088  ballotth  33137  efmul2picn  33209  itgexpif  33219  vtscl  33251  circlemeth  33253  hgt750lemd  33261  logdivsqrle  33263  hgt750lem  33264  hgt750lem2  33265  problem4  34256  problem5  34257  quad3  34258  cnndvlem1  35000  sin2h  36068  cos2h  36069  tan2h  36070  poimirlem29  36107  mblfinlem1  36115  mblfinlem2  36116  mblfinlem3  36117  itg2addnclem3  36131  dvasin  36162  areacirc  36171  heiborlem6  36275  12gcd5e1  40460  12lcm5e60  40465  60lcm7e420  40467  420lcm8e840  40468  3exp7  40510  3lexlogpow5ineq1  40511  3lexlogpow2ineq2  40516  3lexlogpow5ineq5  40517  aks4d1p1p5  40532  aks4d1p1  40533  facp2  40551  fac2xp3  40612  2xp3dxp2ge1d  40614  sqn5i  40785  235t711  40791  ex-decpmul  40792  fltne  40968  flt4lem5e  40980  3cubeslem3l  40995  3cubeslem3r  40996  rmxluc  41246  rmyluc  41247  jm2.17a  41270  jm2.18  41298  jm2.23  41306  jm3.1lem1  41327  proot1ex  41514  areaquad  41536  sqrtcval  41903  resqrtvalex  41907  lhe4.4ex1a  42599  sineq0ALT  43209  coskpi2  44097  cosnegpi  44098  cosknegpi  44100  stoweidlem26  44257  wallispilem4  44299  wallispi  44301  wallispi2lem1  44302  stirlinglem8  44312  dirkerper  44327  dirkertrigeqlem3  44331  dirkertrigeq  44332  dirkeritg  44333  dirkercncflem1  44334  dirkercncflem2  44335  fourierdlem57  44394  fourierdlem58  44395  fourierdlem62  44399  fourierdlem76  44413  fourierdlem103  44440  fourierdlem104  44441  sqwvfourb  44460  fourierswlem  44461  fmtnoge3  45712  fmtnorec1  45719  fmtno0  45722  fmtno1  45723  fmtnorec3  45730  fmtnorec4  45731  fmtno5lem2  45736  fmtno5lem4  45738  257prm  45743  fmtnoprmfac2lem1  45748  fmtno4prmfac  45754  fmtno5faclem2  45762  fmtno5faclem3  45763  fmtno5fac  45764  139prmALT  45778  31prm  45779  127prm  45781  mod42tp1mod8  45784  lighneallem2  45788  lighneallem3  45789  lighneallem4a  45790  3exp4mod41  45798  41prothprmlem1  45799  41prothprmlem2  45800  41prothprm  45801  bits0ALTV  45861  0evenALTV  45870  6even  45893  8even  45895  perfectALTVlem1  45903  perfectALTVlem2  45904  perfectALTV  45905  2exp340mod341  45915  8exp8mod9  45918  mogoldbb  45967  nnsum3primes4  45970  bgoldbtbndlem1  45987  0nodd  46094  0even  46219  2even  46221  2zrngamgm  46227  2t6m3t4e0  46414  linevalexample  46466  zlmodzxzequap  46570  pw2m1lepw2m1  46591  nnlog2ge0lt1  46642  logbpw2m1  46643  nnpw2blen  46656  nnpw2pmod  46659  blen1  46660  blen2  46661  blennnt2  46665  nnolog2flm1  46666  0dig2nn0e  46688  0dig2nn0o  46689  nn0sumshdiglemA  46695  nn0sumshdiglemB  46696  nn0sumshdiglem1  46697  nn0sumshdiglem2  46698  ackval1012  46766  ackval2012  46767  ackval3012  46768  ackval42  46772  sinhpcosh  47175