Theorem 2cn 12313

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 12301	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11239	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2830	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   + caddc 11130  2c2 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-2 12301

This theorem is referenced by:  2ex  12315  2cnd  12316  3cn  12319  2m1e1  12364  3m1e2  12366  2p2e4  12373  times2  12375  2div2e1  12379  1p2e3ALT  12382  3p3e6  12390  4p3e7  12392  5p3e8  12395  6p3e9  12398  2t1e2  12401  2t2e4  12402  3t3e9  12405  2t0e0  12407  4d2e2  12408  2cnne0  12448  halfcn  12453  2halves  12457  8th4div3  12459  halfthird  12460  halfpm6th  12461  2mulicn  12463  2muline0  12464  halfcl  12465  half0  12467  halfaddsub  12472  div4p1lem1div2  12494  3halfnz  12670  zneo  12674  nneo  12675  zeo  12677  7p3e10  12781  4t4e16  12805  6t3e18  12811  7t7e49  12820  8t5e40  12824  9t9e81  12835  decbin0  12846  decbin2  12847  fztpval  13601  fz0tp  13643  fzo0to3tp  13766  fzo1to4tp  13768  expubnd  14194  sq2  14213  sq4e2t8  14215  cu2  14216  subsq2  14227  binom2sub  14236  binom3  14240  zesq  14242  fac2  14295  fac3  14296  faclbnd2  14307  faclbnd4lem1  14309  faclbnd4lem3  14311  faclbnd4lem4  14312  faclbnd5  14314  bcn2  14335  4bc2eq6  14345  swrd2lsw  14969  crre  15131  addcj  15165  imval2  15168  01sqrexlem7  15265  absmax  15346  rddif  15357  sqreulem  15376  amgm2  15386  abs3lemi  15427  iseraltlem2  15697  ackbijnn  15842  climcndslem1  15863  climcndslem2  15864  arisum  15874  arisum2  15875  geo2sum2  15888  geo2lim  15889  geoihalfsum  15896  bpoly2  16071  bpoly3  16072  bpoly4  16073  fsumcube  16074  efcllem  16091  ege2le3  16104  efgt0  16119  tanval2  16149  tanval3  16150  efi4p  16153  efival  16168  sinadd  16180  cosadd  16181  sinmul  16188  cos2tsin  16195  ef01bndlem  16200  cos01bnd  16202  cos1bnd  16203  cos2bnd  16204  cos01gt0  16207  sin02gt0  16208  sin4lt0  16211  odd2np1lem  16357  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  nno  16399  nn0o  16400  flodddiv4  16432  bits0  16445  bitsfzolem  16451  0bits  16456  bitsinv1  16459  sadcadd  16475  smumullem  16509  6gcd4e2  16555  3lcm2e6woprm  16632  6lcm4e12  16633  pythagtriplem1  16834  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem15  16847  pythagtriplem16  16848  pythagtriplem17  16849  iserodd  16853  prmreclem5  16938  prmreclem6  16939  4sqlem11  16973  4sqlem12  16974  prmo2  17058  prmo3  17059  dec5dvds  17082  dec2nprm  17085  2exp5  17103  2exp6  17104  2exp7  17105  2exp8  17106  2exp11  17107  2exp16  17108  7prm  17128  11prm  17132  13prm  17133  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  psgnunilem2  19474  efgtlen  19705  efgredleme  19722  frgpnabllem1  19852  lt6abl  19874  htpycc  24928  pcoval2  24965  pcocn  24966  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  csbren  25349  minveclem2  25376  ovolunlem1a  25447  ovolunlem1  25448  vitalilem4  25562  mbfi1fseqlem5  25670  dvmptre  25923  dvsincos  25935  aaliou3lem2  26301  aaliou3lem3  26302  aaliou3lem8  26303  coscn  26405  sinhalfpilem  26422  cospi  26431  ef2pi  26436  ef2kpi  26437  efper  26438  sinperlem  26439  sin2kpi  26442  cos2kpi  26443  sin2pim  26444  cos2pim  26445  sincosq3sgn  26459  sincosq4sgn  26460  tangtx  26464  sinq12gt0  26466  sincosq1eq  26471  sincos4thpi  26472  sincos6thpi  26475  sincos3rdpi  26476  pige3ALT  26479  abssinper  26480  coskpi  26482  sineq0  26483  coseq1  26484  efeq1  26487  efif1olem4  26504  eflogeq  26561  tanarg  26578  cxpsqrtlem  26661  cxpsqrt  26662  logsqrt  26663  2irrexpq  26690  root1eq1  26715  cxpeq  26717  2logb9irrALT  26758  sqrt2cxp2logb9e3  26759  ang180lem2  26770  ang180lem3  26771  quad2  26799  1cubrlem  26801  1cubr  26802  dcubic2  26804  dcubic1  26805  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1lem  26815  quart1  26816  quartlem1  26817  quartlem2  26818  quartlem3  26819  quart  26821  sinasin  26849  asinsin  26852  atancj  26870  efiatan  26872  efiatan2  26877  2efiatan  26878  tanatan  26879  atantan  26883  atanbndlem  26885  atans2  26891  dvatan  26895  atantayl2  26898  leibpilem2  26901  log2cnv  26904  log2tlbnd  26905  log2ublem2  26907  log2ublem3  26908  log2ub  26909  birthday  26914  zetacvg  26975  basellem1  27041  basellem3  27043  basellem8  27048  basellem9  27049  cht3  27133  1sgm2ppw  27161  ppiub  27165  chtublem  27172  chtub  27173  perfect1  27189  perfectlem1  27190  perfectlem2  27191  perfect  27192  bcmax  27239  bcp1ctr  27240  bclbnd  27241  bpos1lem  27243  bpos1  27244  bposlem1  27245  bposlem2  27246  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem8  27252  bposlem9  27253  lgsdir2lem2  27287  gausslemma2dlem6  27333  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem2  27346  m1lgs  27349  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgsoddprmlem2  27370  2lgsoddprmlem3c  27373  2lgsoddprmlem3d  27374  addsqnreup  27404  addsq2nreurex  27405  rplogsumlem1  27445  dchrisum0fno1  27472  dchrisum0lem1  27477  dchrisum0lem2  27479  logdivsum  27494  mulog2sumlem3  27497  log2sumbnd  27505  selberglem1  27506  selberglem2  27507  selberg2  27512  selberg4lem1  27521  selberg3r  27530  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2  27552  pntlemk  27567  ax5seglem7  28860  axlowdimlem13  28879  elwspths2spth  29895  clwlkclwwlklem2a4  29924  clwwlknonex2  30036  2clwwlk2  30275  numclwlk1lem1  30296  ex-fl  30374  ex-ceil  30375  ex-exp  30377  ex-fac  30378  ex-abs  30382  ex-ind-dvds  30388  ipidsq  30637  cncph  30746  ip0i  30752  ip1ilem  30753  ipdirilem  30756  minvecolem2  30802  hvsubcan2i  30991  norm-ii-i  31064  norm3lem  31076  normpar2i  31083  polid2i  31084  hhph  31105  mayete3i  31655  nmcexi  31953  opsqrlem6  32072  addltmulALT  32373  ply1dg3rt0irred  33541  fldext2chn  33708  constrelextdg2  33727  2sqr3minply  33760  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  omssubadd  34278  oddpwdc  34332  fib5  34383  ballotlem2  34467  ballotth  34516  efmul2picn  34574  itgexpif  34584  vtscl  34616  circlemeth  34618  hgt750lemd  34626  logdivsqrle  34628  hgt750lem  34629  hgt750lem2  34630  problem4  35636  problem5  35637  quad3  35638  cnndvlem1  36501  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem29  37619  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  itg2addnclem3  37643  dvasin  37674  areacirc  37683  heiborlem6  37786  12gcd5e1  41962  12lcm5e60  41967  60lcm7e420  41969  420lcm8e840  41970  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1p5  42034  aks4d1p1  42035  posbezout  42059  facp2  42102  fac2xp3  42198  2xp3dxp2ge1d  42200  sqn5i  42282  235t711  42301  ex-decpmul  42302  cxp112d  42337  cxp111d  42338  cxpi11d  42339  tanhalfpim  42345  fltne  42614  flt4lem5e  42626  sum9cubes  42642  3cubeslem3l  42656  3cubeslem3r  42657  rmxluc  42907  rmyluc  42908  jm2.17a  42931  jm2.18  42959  jm2.23  42967  jm3.1lem1  42988  proot1ex  43167  areaquad  43187  sqrtcval  43612  resqrtvalex  43616  lhe4.4ex1a  44301  sineq0ALT  44909  coskpi2  45843  cosnegpi  45844  cosknegpi  45846  stoweidlem26  46003  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  stirlinglem8  46058  dirkerper  46073  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkeritg  46079  dirkercncflem1  46080  dirkercncflem2  46081  fourierdlem57  46140  fourierdlem58  46141  fourierdlem62  46145  fourierdlem76  46159  fourierdlem103  46186  fourierdlem104  46187  sqwvfourb  46206  fourierswlem  46207  rehalfge1  47312  ceil5half3  47317  fmtnoge3  47492  fmtnorec1  47499  fmtno0  47502  fmtno1  47503  fmtnorec3  47510  fmtnorec4  47511  fmtno5lem2  47516  fmtno5lem4  47518  257prm  47523  fmtnoprmfac2lem1  47528  fmtno4prmfac  47534  fmtno5faclem2  47542  fmtno5faclem3  47543  fmtno5fac  47544  139prmALT  47558  31prm  47559  127prm  47561  mod42tp1mod8  47564  lighneallem2  47568  lighneallem3  47569  lighneallem4a  47570  3exp4mod41  47578  41prothprmlem1  47579  41prothprmlem2  47580  41prothprm  47581  bits0ALTV  47641  0evenALTV  47650  6even  47673  8even  47675  perfectALTVlem1  47683  perfectALTVlem2  47684  perfectALTV  47685  2exp340mod341  47695  8exp8mod9  47698  mogoldbb  47747  nnsum3primes4  47750  bgoldbtbndlem1  47767  gpg5order  48012  0nodd  48093  0even  48160  2even  48162  2zrngamgm  48168  2t6m3t4e0  48271  linevalexample  48319  zlmodzxzequap  48423  pw2m1lepw2m1  48444  nnlog2ge0lt1  48494  logbpw2m1  48495  nnpw2blen  48508  nnpw2pmod  48511  blen1  48512  blen2  48513  blennnt2  48517  nnolog2flm1  48518  0dig2nn0e  48540  0dig2nn0o  48541  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  nn0sumshdiglem2  48550  ackval1012  48618  ackval2012  48619  ackval3012  48620  ackval42  48624  sinhpcosh  49552