Theorem 2cn 12341

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 12329	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11267	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2837	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158  2c2 12321

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 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329

This theorem is referenced by:  2ex  12343  2cnd  12344  3cn  12347  2m1e1  12392  3m1e2  12394  2p2e4  12401  times2  12403  2div2e1  12407  1p2e3ALT  12410  3p3e6  12418  4p3e7  12420  5p3e8  12423  6p3e9  12426  2t1e2  12429  2t2e4  12430  3t3e9  12433  2t0e0  12435  4d2e2  12436  2cnne0  12476  halfcn  12481  1mhlfehlf  12485  8th4div3  12486  halfpm6th  12487  2mulicn  12489  2muline0  12490  halfcl  12491  half0  12493  2halves  12494  halfaddsub  12499  div4p1lem1div2  12521  3halfnz  12697  zneo  12701  nneo  12702  zeo  12704  7p3e10  12808  4t4e16  12832  6t3e18  12838  7t7e49  12847  8t5e40  12851  9t9e81  12862  decbin0  12873  decbin2  12874  halfthird  12876  fztpval  13626  fz0tp  13668  fzo0to3tp  13791  fzo1to4tp  13793  expubnd  14217  sq2  14236  sq4e2t8  14238  cu2  14239  subsq2  14250  binom2sub  14259  binom3  14263  zesq  14265  fac2  14318  fac3  14319  faclbnd2  14330  faclbnd4lem1  14332  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd5  14337  bcn2  14358  4bc2eq6  14368  swrd2lsw  14991  crre  15153  addcj  15187  imval2  15190  01sqrexlem7  15287  absmax  15368  rddif  15379  sqreulem  15398  amgm2  15408  abs3lemi  15449  iseraltlem2  15719  ackbijnn  15864  climcndslem1  15885  climcndslem2  15886  arisum  15896  arisum2  15897  geo2sum2  15910  geo2lim  15911  geoihalfsum  15918  bpoly2  16093  bpoly3  16094  bpoly4  16095  fsumcube  16096  efcllem  16113  ege2le3  16126  efgt0  16139  tanval2  16169  tanval3  16170  efi4p  16173  efival  16188  sinadd  16200  cosadd  16201  sinmul  16208  cos2tsin  16215  ef01bndlem  16220  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  cos01gt0  16227  sin02gt0  16228  sin4lt0  16231  odd2np1lem  16377  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  nno  16419  nn0o  16420  flodddiv4  16452  bits0  16465  bitsfzolem  16471  0bits  16476  bitsinv1  16479  sadcadd  16495  smumullem  16529  6gcd4e2  16575  3lcm2e6woprm  16652  6lcm4e12  16653  pythagtriplem1  16854  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem15  16867  pythagtriplem16  16868  pythagtriplem17  16869  iserodd  16873  prmreclem5  16958  prmreclem6  16959  4sqlem11  16993  4sqlem12  16994  prmo2  17078  prmo3  17079  dec5dvds  17102  dec2nprm  17105  2exp5  17123  2exp6  17124  2exp7  17125  2exp8  17126  2exp11  17127  2exp16  17128  7prm  17148  11prm  17152  13prm  17153  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  psgnunilem2  19513  efgtlen  19744  efgredleme  19761  frgpnabllem1  19891  lt6abl  19913  htpycc  25012  pcoval2  25049  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  csbren  25433  minveclem2  25460  ovolunlem1a  25531  ovolunlem1  25532  vitalilem4  25646  mbfi1fseqlem5  25754  dvmptre  26007  dvsincos  26019  aaliou3lem2  26385  aaliou3lem3  26386  aaliou3lem8  26387  coscn  26489  sinhalfpilem  26505  cospi  26514  ef2pi  26519  ef2kpi  26520  efper  26521  sinperlem  26522  sin2kpi  26525  cos2kpi  26526  sin2pim  26527  cos2pim  26528  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sinq12gt0  26549  sincosq1eq  26554  sincos4thpi  26555  sincos6thpi  26558  sincos3rdpi  26559  pige3ALT  26562  abssinper  26563  coskpi  26565  sineq0  26566  coseq1  26567  efeq1  26570  efif1olem4  26587  eflogeq  26644  tanarg  26661  cxpsqrtlem  26744  cxpsqrt  26745  logsqrt  26746  2irrexpq  26773  root1eq1  26798  cxpeq  26800  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  ang180lem2  26853  ang180lem3  26854  quad2  26882  1cubrlem  26884  1cubr  26885  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem2  26901  quartlem3  26902  quart  26904  sinasin  26932  asinsin  26935  atancj  26953  efiatan  26955  efiatan2  26960  2efiatan  26961  tanatan  26962  atantan  26966  atanbndlem  26968  atans2  26974  dvatan  26978  atantayl2  26981  leibpilem2  26984  log2cnv  26987  log2tlbnd  26988  log2ublem2  26990  log2ublem3  26991  log2ub  26992  birthday  26997  zetacvg  27058  basellem1  27124  basellem3  27126  basellem8  27131  basellem9  27132  cht3  27216  1sgm2ppw  27244  ppiub  27248  chtublem  27255  chtub  27256  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  bcmax  27322  bcp1ctr  27323  bclbnd  27324  bpos1lem  27326  bpos1  27327  bposlem1  27328  bposlem2  27329  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem8  27335  bposlem9  27336  lgsdir2lem2  27370  gausslemma2dlem6  27416  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem2  27429  m1lgs  27432  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgsoddprmlem2  27453  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  addsqnreup  27487  addsq2nreurex  27488  rplogsumlem1  27528  dchrisum0fno1  27555  dchrisum0lem1  27560  dchrisum0lem2  27562  logdivsum  27577  mulog2sumlem3  27580  log2sumbnd  27588  selberglem1  27589  selberglem2  27590  selberg2  27595  selberg4lem1  27604  selberg3r  27613  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem2  27635  pntlemk  27650  ax5seglem7  28950  axlowdimlem13  28969  elwspths2spth  29987  clwlkclwwlklem2a4  30016  clwwlknonex2  30128  2clwwlk2  30367  numclwlk1lem1  30388  ex-fl  30466  ex-ceil  30467  ex-exp  30469  ex-fac  30470  ex-abs  30474  ex-ind-dvds  30480  ipidsq  30729  cncph  30838  ip0i  30844  ip1ilem  30845  ipdirilem  30848  minvecolem2  30894  hvsubcan2i  31083  norm-ii-i  31156  norm3lem  31168  normpar2i  31175  polid2i  31176  hhph  31197  mayete3i  31747  nmcexi  32045  opsqrlem6  32164  addltmulALT  32465  ply1dg3rt0irred  33607  fldext2chn  33769  constrelextdg2  33788  2sqr3minply  33791  omssubadd  34302  oddpwdc  34356  fib5  34407  ballotlem2  34491  ballotth  34540  efmul2picn  34611  itgexpif  34621  vtscl  34653  circlemeth  34655  hgt750lemd  34663  logdivsqrle  34665  hgt750lem  34666  hgt750lem2  34667  problem4  35673  problem5  35674  quad3  35675  cnndvlem1  36538  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem29  37656  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  itg2addnclem3  37680  dvasin  37711  areacirc  37720  heiborlem6  37823  12gcd5e1  42004  12lcm5e60  42009  60lcm7e420  42011  420lcm8e840  42012  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1p5  42076  aks4d1p1  42077  posbezout  42101  facp2  42144  fac2xp3  42240  2xp3dxp2ge1d  42242  sqn5i  42320  235t711  42339  ex-decpmul  42340  cxp112d  42377  cxp111d  42378  cxpi11d  42379  tanhalfpim  42385  fltne  42654  flt4lem5e  42666  sum9cubes  42682  3cubeslem3l  42697  3cubeslem3r  42698  rmxluc  42948  rmyluc  42949  jm2.17a  42972  jm2.18  43000  jm2.23  43008  jm3.1lem1  43029  proot1ex  43208  areaquad  43228  sqrtcval  43654  resqrtvalex  43658  lhe4.4ex1a  44348  sineq0ALT  44957  coskpi2  45881  cosnegpi  45882  cosknegpi  45884  stoweidlem26  46041  wallispilem4  46083  wallispi  46085  wallispi2lem1  46086  stirlinglem8  46096  dirkerper  46111  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkeritg  46117  dirkercncflem1  46118  dirkercncflem2  46119  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem76  46197  fourierdlem103  46224  fourierdlem104  46225  sqwvfourb  46244  fourierswlem  46245  ceil5half3  47342  fmtnoge3  47517  fmtnorec1  47524  fmtno0  47527  fmtno1  47528  fmtnorec3  47535  fmtnorec4  47536  fmtno5lem2  47541  fmtno5lem4  47543  257prm  47548  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  fmtno5faclem2  47567  fmtno5faclem3  47568  fmtno5fac  47569  139prmALT  47583  31prm  47584  127prm  47586  mod42tp1mod8  47589  lighneallem2  47593  lighneallem3  47594  lighneallem4a  47595  3exp4mod41  47603  41prothprmlem1  47604  41prothprmlem2  47605  41prothprm  47606  bits0ALTV  47666  0evenALTV  47675  6even  47698  8even  47700  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  2exp340mod341  47720  8exp8mod9  47723  mogoldbb  47772  nnsum3primes4  47775  bgoldbtbndlem1  47792  gpg5order  48014  0nodd  48086  0even  48153  2even  48155  2zrngamgm  48161  2t6m3t4e0  48264  linevalexample  48312  zlmodzxzequap  48416  pw2m1lepw2m1  48437  nnlog2ge0lt1  48487  logbpw2m1  48488  nnpw2blen  48501  nnpw2pmod  48504  blen1  48505  blen2  48506  blennnt2  48510  nnolog2flm1  48511  0dig2nn0e  48533  0dig2nn0o  48534  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdiglem2  48543  ackval1012  48611  ackval2012  48612  ackval3012  48613  ackval42  48617  sinhpcosh  49259