Theorem 2cn 12220

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 12208	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11138	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2832	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208

This theorem is referenced by:  2ex  12222  2cnd  12223  3cn  12226  2m1e1  12266  3m1e2  12268  2p2e4  12275  times2  12277  2div2e1  12281  1p2e3ALT  12284  3p3e6  12292  4p3e7  12294  5p3e8  12297  6p3e9  12300  2t1e2  12303  2t2e4  12304  3t3e9  12307  2t0e0  12309  4div2e2  12310  2cnne0  12350  halfcn  12355  2halves  12359  8th4div3  12361  halfthird  12362  halfpm6th  12363  2mulicn  12365  2muline0  12366  halfcl  12367  half0  12369  halfaddsub  12374  div4p1lem1div2  12396  3halfnz  12571  zneo  12575  nneo  12576  zeo  12578  7p3e10  12682  4t4e16  12706  6t3e18  12712  7t7e49  12721  8t5e40  12725  9t9e81  12736  decbin0  12747  decbin2  12748  fztpval  13502  fz0tp  13544  fzo0to3tp  13668  fzo1to4tp  13670  expubnd  14101  sq2  14120  sq4e2t8  14122  cu2  14123  subsq2  14134  binom2sub  14143  binom3  14147  zesq  14149  fac2  14202  fac3  14203  faclbnd2  14214  faclbnd4lem1  14216  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd5  14221  bcn2  14242  4bc2eq6  14252  swrd2lsw  14875  crre  15037  addcj  15071  imval2  15074  01sqrexlem7  15171  absmax  15253  rddif  15264  sqreulem  15283  amgm2  15293  abs3lemi  15334  iseraltlem2  15606  ackbijnn  15751  climcndslem1  15772  climcndslem2  15773  arisum  15783  arisum2  15784  geo2sum2  15797  geo2lim  15798  geoihalfsum  15805  bpoly2  15980  bpoly3  15981  bpoly4  15982  fsumcube  15983  efcllem  16000  ege2le3  16013  efgt0  16028  tanval2  16058  tanval3  16059  efi4p  16062  efival  16077  sinadd  16089  cosadd  16090  sinmul  16097  cos2tsin  16104  ef01bndlem  16109  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  cos01gt0  16116  sin02gt0  16117  sin4lt0  16120  odd2np1lem  16267  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  nno  16309  nn0o  16310  flodddiv4  16342  bits0  16355  bitsfzolem  16361  0bits  16366  bitsinv1  16369  sadcadd  16385  smumullem  16419  6gcd4e2  16465  3lcm2e6woprm  16542  6lcm4e12  16543  pythagtriplem1  16744  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem15  16757  pythagtriplem16  16758  pythagtriplem17  16759  iserodd  16763  prmreclem5  16848  prmreclem6  16849  4sqlem11  16883  4sqlem12  16884  prmo2  16968  prmo3  16969  dec5dvds  16992  dec2nprm  16995  2exp5  17013  2exp6  17014  2exp7  17015  2exp8  17016  2exp11  17017  2exp16  17018  7prm  17038  11prm  17042  13prm  17043  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  psgnunilem2  19424  efgtlen  19655  efgredleme  19672  frgpnabllem1  19802  lt6abl  19824  htpycc  24935  pcoval2  24972  pcocn  24973  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  csbren  25355  minveclem2  25382  ovolunlem1a  25453  ovolunlem1  25454  vitalilem4  25568  mbfi1fseqlem5  25676  dvmptre  25929  dvsincos  25941  aaliou3lem2  26307  aaliou3lem3  26308  aaliou3lem8  26309  coscn  26411  sinhalfpilem  26428  cospi  26437  ef2pi  26442  ef2kpi  26443  efper  26444  sinperlem  26445  sin2kpi  26448  cos2kpi  26449  sin2pim  26450  cos2pim  26451  sincosq3sgn  26465  sincosq4sgn  26466  tangtx  26470  sinq12gt0  26472  sincosq1eq  26477  sincos4thpi  26478  sincos6thpi  26481  sincos3rdpi  26482  pige3ALT  26485  abssinper  26486  coskpi  26488  sineq0  26489  coseq1  26490  efeq1  26493  efif1olem4  26510  eflogeq  26567  tanarg  26584  cxpsqrtlem  26667  cxpsqrt  26668  logsqrt  26669  2irrexpq  26696  root1eq1  26721  cxpeq  26723  2logb9irrALT  26764  sqrt2cxp2logb9e3  26765  ang180lem2  26776  ang180lem3  26777  quad2  26805  1cubrlem  26807  1cubr  26808  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem2  26824  quartlem3  26825  quart  26827  sinasin  26855  asinsin  26858  atancj  26876  efiatan  26878  efiatan2  26883  2efiatan  26884  tanatan  26885  atantan  26889  atanbndlem  26891  atans2  26897  dvatan  26901  atantayl2  26904  leibpilem2  26907  log2cnv  26910  log2tlbnd  26911  log2ublem2  26913  log2ublem3  26914  log2ub  26915  birthday  26920  zetacvg  26981  basellem1  27047  basellem3  27049  basellem8  27054  basellem9  27055  cht3  27139  1sgm2ppw  27167  ppiub  27171  chtublem  27178  chtub  27179  perfect1  27195  perfectlem1  27196  perfectlem2  27197  perfect  27198  bcmax  27245  bcp1ctr  27246  bclbnd  27247  bpos1lem  27249  bpos1  27250  bposlem1  27251  bposlem2  27252  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem2  27293  gausslemma2dlem6  27339  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem2  27352  m1lgs  27355  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgsoddprmlem2  27376  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  addsqnreup  27410  addsq2nreurex  27411  rplogsumlem1  27451  dchrisum0fno1  27478  dchrisum0lem1  27483  dchrisum0lem2  27485  logdivsum  27500  mulog2sumlem3  27503  log2sumbnd  27511  selberglem1  27512  selberglem2  27513  selberg2  27518  selberg4lem1  27527  selberg3r  27536  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem2  27558  pntlemk  27573  ax5seglem7  29008  axlowdimlem13  29027  elwspths2spth  30043  clwlkclwwlklem2a4  30072  clwwlknonex2  30184  2clwwlk2  30423  numclwlk1lem1  30444  ex-fl  30522  ex-ceil  30523  ex-exp  30525  ex-fac  30526  ex-abs  30530  ex-ind-dvds  30536  ipidsq  30785  cncph  30894  ip0i  30900  ip1ilem  30901  ipdirilem  30904  minvecolem2  30950  hvsubcan2i  31139  norm-ii-i  31212  norm3lem  31224  normpar2i  31231  polid2i  31232  hhph  31253  mayete3i  31803  nmcexi  32101  opsqrlem6  32220  addltmulALT  32521  ply1dg3rt0irred  33665  fldext2chn  33885  constrelextdg2  33904  2sqr3minply  33937  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  omssubadd  34457  oddpwdc  34511  fib5  34562  ballotlem2  34646  ballotth  34695  efmul2picn  34753  itgexpif  34763  vtscl  34795  circlemeth  34797  hgt750lemd  34805  logdivsqrle  34807  hgt750lem  34808  hgt750lem2  34809  problem4  35862  problem5  35863  quad3  35864  cnndvlem1  36737  sin2h  37807  cos2h  37808  tan2h  37809  poimirlem29  37846  mblfinlem1  37854  mblfinlem2  37855  mblfinlem3  37856  itg2addnclem3  37870  dvasin  37901  areacirc  37910  heiborlem6  38013  12gcd5e1  42253  12lcm5e60  42258  60lcm7e420  42260  420lcm8e840  42261  3exp7  42303  3lexlogpow5ineq1  42304  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1p1p5  42325  aks4d1p1  42326  posbezout  42350  facp2  42393  1p3e4  42510  sqn5i  42536  235t711  42556  ex-decpmul  42557  cxp112d  42592  cxp111d  42593  cxpi11d  42594  tanhalfpim  42600  fltne  42883  flt4lem5e  42895  sum9cubes  42911  3cubeslem3l  42924  3cubeslem3r  42925  rmxluc  43174  rmyluc  43175  jm2.17a  43198  jm2.18  43226  jm2.23  43234  jm3.1lem1  43255  proot1ex  43434  areaquad  43454  sqrtcval  43878  resqrtvalex  43882  lhe4.4ex1a  44566  sineq0ALT  45173  coskpi2  46106  cosnegpi  46107  cosknegpi  46109  stoweidlem26  46266  wallispilem4  46308  wallispi  46310  wallispi2lem1  46311  stirlinglem8  46321  dirkerper  46336  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkeritg  46342  dirkercncflem1  46343  dirkercncflem2  46344  fourierdlem57  46403  fourierdlem58  46404  fourierdlem62  46408  fourierdlem76  46422  fourierdlem103  46449  fourierdlem104  46450  sqwvfourb  46469  fourierswlem  46470  nthrucw  47126  rehalfge1  47577  ceil5half3  47582  modm2nep1  47608  modm1nep2  47610  modm1nem2  47611  fmtnoge3  47772  fmtnorec1  47779  fmtno0  47782  fmtno1  47783  fmtnorec3  47790  fmtnorec4  47791  fmtno5lem2  47796  fmtno5lem4  47798  257prm  47803  fmtnoprmfac2lem1  47808  fmtno4prmfac  47814  fmtno5faclem2  47822  fmtno5faclem3  47823  fmtno5fac  47824  139prmALT  47838  31prm  47839  127prm  47841  mod42tp1mod8  47844  lighneallem2  47848  lighneallem3  47849  lighneallem4a  47850  3exp4mod41  47858  41prothprmlem1  47859  41prothprmlem2  47860  41prothprm  47861  bits0ALTV  47921  0evenALTV  47930  6even  47953  8even  47955  perfectALTVlem1  47963  perfectALTVlem2  47964  perfectALTV  47965  2exp340mod341  47975  8exp8mod9  47978  mogoldbb  48027  nnsum3primes4  48030  bgoldbtbndlem1  48047  gpg5order  48302  gpg5edgnedg  48372  0nodd  48412  0even  48479  2even  48481  2zrngamgm  48487  2t6m3t4e0  48590  linevalexample  48637  zlmodzxzequap  48741  pw2m1lepw2m1  48762  nnlog2ge0lt1  48808  logbpw2m1  48809  nnpw2blen  48822  nnpw2pmod  48825  blen1  48826  blen2  48827  blennnt2  48831  nnolog2flm1  48832  0dig2nn0e  48854  0dig2nn0o  48855  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  nn0sumshdiglem1  48863  nn0sumshdiglem2  48864  ackval1012  48932  ackval2012  48933  ackval3012  48934  ackval42  48938  sinhpcosh  49981