Theorem 2cn 12256

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  2c2 12236

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

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

This theorem is referenced by:  2ex  12258  2cnd  12259  3cn  12262  2m1e1  12302  3m1e2  12304  2p2e4  12311  times2  12313  2div2e1  12317  1p2e3ALT  12320  3p3e6  12328  4p3e7  12330  5p3e8  12333  6p3e9  12336  2t1e2  12339  2t2e4  12340  3t3e9  12343  2t0e0  12345  4div2e2  12346  2cnne0  12386  halfcn  12391  2halves  12395  8th4div3  12397  halfthird  12398  halfpm6th  12399  2mulicn  12401  2muline0  12402  halfcl  12403  half0  12405  halfaddsub  12410  div4p1lem1div2  12432  3halfnz  12608  zneo  12612  nneo  12613  zeo  12615  7p3e10  12719  4t4e16  12743  6t3e18  12749  7t7e49  12758  8t5e40  12762  9t9e81  12773  decbin0  12784  decbin2  12785  fztpval  13540  fz0tp  13582  fzo0to3tp  13707  fzo1to4tp  13709  expubnd  14140  sq2  14159  sq4e2t8  14161  cu2  14162  subsq2  14173  binom2sub  14182  binom3  14186  zesq  14188  fac2  14241  fac3  14242  faclbnd2  14253  faclbnd4lem1  14255  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd5  14260  bcn2  14281  4bc2eq6  14291  swrd2lsw  14914  crre  15076  addcj  15110  imval2  15113  01sqrexlem7  15210  absmax  15292  rddif  15303  sqreulem  15322  amgm2  15332  abs3lemi  15373  iseraltlem2  15645  ackbijnn  15793  climcndslem1  15814  climcndslem2  15815  arisum  15825  arisum2  15826  geo2sum2  15839  geo2lim  15840  geoihalfsum  15847  bpoly2  16022  bpoly3  16023  bpoly4  16024  fsumcube  16025  efcllem  16042  ege2le3  16055  efgt0  16070  tanval2  16100  tanval3  16101  efi4p  16104  efival  16119  sinadd  16131  cosadd  16132  sinmul  16139  cos2tsin  16146  ef01bndlem  16151  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  cos01gt0  16158  sin02gt0  16159  sin4lt0  16162  odd2np1lem  16309  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  nno  16351  nn0o  16352  flodddiv4  16384  bits0  16397  bitsfzolem  16403  0bits  16408  bitsinv1  16411  sadcadd  16427  smumullem  16461  6gcd4e2  16507  3lcm2e6woprm  16584  6lcm4e12  16585  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  iserodd  16806  prmreclem5  16891  prmreclem6  16892  4sqlem11  16926  4sqlem12  16927  prmo2  17011  prmo3  17012  dec5dvds  17035  dec2nprm  17038  2exp5  17056  2exp6  17057  2exp7  17058  2exp8  17059  2exp11  17060  2exp16  17061  7prm  17081  11prm  17085  13prm  17086  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  psgnunilem2  19470  efgtlen  19701  efgredleme  19718  frgpnabllem1  19848  lt6abl  19870  htpycc  24947  pcoval2  24983  pcocn  24984  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  csbren  25366  minveclem2  25393  ovolunlem1a  25463  ovolunlem1  25464  vitalilem4  25578  mbfi1fseqlem5  25686  dvmptre  25936  dvsincos  25948  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem8  26311  coscn  26410  sinhalfpilem  26427  cospi  26436  ef2pi  26441  ef2kpi  26442  efper  26443  sinperlem  26444  sin2kpi  26447  cos2kpi  26448  sin2pim  26449  cos2pim  26450  sincosq3sgn  26464  sincosq4sgn  26465  tangtx  26469  sinq12gt0  26471  sincosq1eq  26476  sincos4thpi  26477  sincos6thpi  26480  sincos3rdpi  26481  pige3ALT  26484  abssinper  26485  coskpi  26487  sineq0  26488  coseq1  26489  efeq1  26492  efif1olem4  26509  eflogeq  26566  tanarg  26583  cxpsqrtlem  26666  cxpsqrt  26667  logsqrt  26668  2irrexpq  26695  root1eq1  26719  cxpeq  26721  2logb9irrALT  26762  sqrt2cxp2logb9e3  26763  ang180lem2  26774  ang180lem3  26775  quad2  26803  1cubrlem  26805  1cubr  26806  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quartlem3  26823  quart  26825  sinasin  26853  asinsin  26856  atancj  26874  efiatan  26876  efiatan2  26881  2efiatan  26882  tanatan  26883  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl2  26902  leibpilem2  26905  log2cnv  26908  log2tlbnd  26909  log2ublem2  26911  log2ublem3  26912  log2ub  26913  birthday  26918  zetacvg  26978  basellem1  27044  basellem3  27046  basellem8  27051  basellem9  27052  cht3  27136  1sgm2ppw  27163  ppiub  27167  chtublem  27174  chtub  27175  perfect1  27191  perfectlem1  27192  perfectlem2  27193  perfect  27194  bcmax  27241  bcp1ctr  27242  bclbnd  27243  bpos1lem  27245  bpos1  27246  bposlem1  27247  bposlem2  27248  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem2  27289  gausslemma2dlem6  27335  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem2  27348  m1lgs  27351  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgsoddprmlem2  27372  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  addsqnreup  27406  addsq2nreurex  27407  rplogsumlem1  27447  dchrisum0fno1  27474  dchrisum0lem1  27479  dchrisum0lem2  27481  logdivsum  27496  mulog2sumlem3  27499  log2sumbnd  27507  selberglem1  27508  selberglem2  27509  selberg2  27514  selberg4lem1  27523  selberg3r  27532  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem2  27554  pntlemk  27569  ax5seglem7  29004  axlowdimlem13  29023  elwspths2spth  30038  clwlkclwwlklem2a4  30067  clwwlknonex2  30179  2clwwlk2  30418  numclwlk1lem1  30439  ex-fl  30517  ex-ceil  30518  ex-exp  30520  ex-fac  30521  ex-abs  30525  ex-ind-dvds  30531  ipidsq  30781  cncph  30890  ip0i  30896  ip1ilem  30897  ipdirilem  30900  minvecolem2  30946  hvsubcan2i  31135  norm-ii-i  31208  norm3lem  31220  normpar2i  31227  polid2i  31228  hhph  31249  mayete3i  31799  nmcexi  32097  opsqrlem6  32216  addltmulALT  32517  ply1dg3rt0irred  33644  fldext2chn  33872  constrelextdg2  33891  2sqr3minply  33924  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  omssubadd  34444  oddpwdc  34498  fib5  34549  ballotlem2  34633  ballotth  34682  efmul2picn  34740  itgexpif  34750  vtscl  34782  circlemeth  34784  hgt750lemd  34792  logdivsqrle  34794  hgt750lem  34795  hgt750lem2  34796  problem4  35850  problem5  35851  quad3  35852  cnndvlem1  36797  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem29  37970  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  itg2addnclem3  37994  dvasin  38025  areacirc  38034  heiborlem6  38137  12gcd5e1  42442  12lcm5e60  42447  60lcm7e420  42449  420lcm8e840  42450  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1p5  42514  aks4d1p1  42515  posbezout  42539  facp2  42582  1p3e4  42697  sqn5i  42717  235t711  42737  ex-decpmul  42738  cxp112d  42773  cxp111d  42774  cxpi11d  42775  tanhalfpim  42781  fltne  43077  flt4lem5e  43089  sum9cubes  43105  3cubeslem3l  43118  3cubeslem3r  43119  rmxluc  43364  rmyluc  43365  jm2.17a  43388  jm2.18  43416  jm2.23  43424  jm3.1lem1  43445  proot1ex  43624  areaquad  43644  sqrtcval  44068  resqrtvalex  44072  lhe4.4ex1a  44756  sineq0ALT  45363  coskpi2  46294  cosnegpi  46295  cosknegpi  46297  stoweidlem26  46454  wallispilem4  46496  wallispi  46498  wallispi2lem1  46499  stirlinglem8  46509  dirkerper  46524  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem2  46532  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem76  46610  fourierdlem103  46637  fourierdlem104  46638  sqwvfourb  46657  fourierswlem  46658  nthrucw  47316  sin5tlem1  47321  sin5tlem5  47325  cos5t  47327  goldrasin  47330  goldracos5teq  47333  goldratmolem2  47334  rehalfge1  47787  ceil5half3  47794  modm2nep1  47820  modm1nep2  47822  modm1nem2  47823  fmtnoge3  47993  fmtnorec1  48000  fmtno0  48003  fmtno1  48004  fmtnorec3  48011  fmtnorec4  48012  fmtno5lem2  48017  fmtno5lem4  48019  257prm  48024  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  fmtno5faclem2  48043  fmtno5faclem3  48044  fmtno5fac  48045  139prmALT  48059  31prm  48060  127prm  48062  mod42tp1mod8  48065  lighneallem2  48069  lighneallem3  48070  lighneallem4a  48071  3exp4mod41  48079  41prothprmlem1  48080  41prothprmlem2  48081  41prothprm  48082  bits0ALTV  48155  0evenALTV  48164  6even  48187  8even  48189  perfectALTVlem1  48197  perfectALTVlem2  48198  perfectALTV  48199  2exp340mod341  48209  8exp8mod9  48212  mogoldbb  48261  nnsum3primes4  48264  bgoldbtbndlem1  48281  gpg5order  48536  gpg5edgnedg  48606  0nodd  48646  0even  48713  2even  48715  2zrngamgm  48721  2t6m3t4e0  48824  linevalexample  48871  zlmodzxzequap  48975  pw2m1lepw2m1  48996  nnlog2ge0lt1  49042  logbpw2m1  49043  nnpw2blen  49056  nnpw2pmod  49059  blen1  49060  blen2  49061  blennnt2  49065  nnolog2flm1  49066  0dig2nn0e  49088  0dig2nn0o  49089  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  nn0sumshdiglem2  49098  ackval1012  49166  ackval2012  49167  ackval3012  49168  ackval42  49172  sinhpcosh  50215