Theorem 2cn 12283

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7404  ℂcc 11104  1c1 11107   + caddc 11109  2c2 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12271

This theorem is referenced by:  2ex  12285  2cnd  12286  3cn  12289  2m1e1  12334  3m1e2  12336  2p2e4  12343  times2  12345  2div2e1  12349  1p2e3ALT  12352  3p3e6  12360  4p3e7  12362  5p3e8  12365  6p3e9  12368  2t1e2  12371  2t2e4  12372  3t3e9  12375  2t0e0  12377  4d2e2  12378  2cnne0  12418  halfcn  12423  1mhlfehlf  12427  8th4div3  12428  halfpm6th  12429  2mulicn  12431  2muline0  12432  halfcl  12433  half0  12435  2halves  12436  halfaddsub  12441  div4p1lem1div2  12463  3halfnz  12637  zneo  12641  nneo  12642  zeo  12644  7p3e10  12748  4t4e16  12772  6t3e18  12778  7t7e49  12787  8t5e40  12791  9t9e81  12802  decbin0  12813  decbin2  12814  halfthird  12816  fztpval  13559  fz0tp  13598  fz0to4untppr  13600  fzo0to3tp  13714  fzo1to4tp  13716  expubnd  14138  sq2  14157  sq4e2t8  14159  cu2  14160  subsq2  14171  binom2sub  14179  binom3  14183  zesq  14185  fac2  14235  fac3  14236  faclbnd2  14247  faclbnd4lem1  14249  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd5  14254  bcn2  14275  4bc2eq6  14285  swrd2lsw  14899  crre  15057  addcj  15091  imval2  15094  01sqrexlem7  15191  absmax  15272  rddif  15283  sqreulem  15302  amgm2  15312  abs3lemi  15353  iseraltlem2  15625  ackbijnn  15770  climcndslem1  15791  climcndslem2  15792  arisum  15802  arisum2  15803  geo2sum2  15816  geo2lim  15817  geoihalfsum  15824  bpoly2  15997  bpoly3  15998  bpoly4  15999  fsumcube  16000  efcllem  16017  ege2le3  16029  efgt0  16042  tanval2  16072  tanval3  16073  efi4p  16076  efival  16091  sinadd  16103  cosadd  16104  sinmul  16111  cos2tsin  16118  ef01bndlem  16123  cos01bnd  16125  cos1bnd  16126  cos2bnd  16127  cos01gt0  16130  sin02gt0  16131  sin4lt0  16134  odd2np1lem  16279  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  nno  16321  nn0o  16322  flodddiv4  16352  bits0  16365  bitsfzolem  16371  0bits  16376  bitsinv1  16379  sadcadd  16395  smumullem  16429  6gcd4e2  16476  3lcm2e6woprm  16548  6lcm4e12  16549  pythagtriplem1  16745  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem15  16758  pythagtriplem16  16759  pythagtriplem17  16760  iserodd  16764  prmreclem5  16849  prmreclem6  16850  4sqlem11  16884  4sqlem12  16885  prmo2  16969  prmo3  16970  dec5dvds  16993  dec2nprm  16996  decexp2  17004  2exp5  17015  2exp6  17016  2exp7  17017  2exp8  17018  2exp11  17019  2exp16  17020  7prm  17040  11prm  17044  13prm  17045  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  psgnunilem2  19356  efgtlen  19587  efgredleme  19604  frgpnabllem1  19733  lt6abl  19755  htpycc  24478  pcoval2  24514  pcocn  24515  pcohtpylem  24517  pcopt  24520  pcopt2  24521  pcoass  24522  pcorevlem  24524  csbren  24898  minveclem2  24925  ovolunlem1a  24995  ovolunlem1  24996  vitalilem4  25110  mbfi1fseqlem5  25219  dvmptre  25468  dvsincos  25480  aaliou3lem2  25838  aaliou3lem3  25839  aaliou3lem8  25840  coscn  25939  sinhalfpilem  25955  cospi  25964  ef2pi  25969  ef2kpi  25970  efper  25971  sinperlem  25972  sin2kpi  25975  cos2kpi  25976  sin2pim  25977  cos2pim  25978  sincosq3sgn  25992  sincosq4sgn  25993  tangtx  25997  sinq12gt0  25999  sincosq1eq  26004  sincos4thpi  26005  sincos6thpi  26007  sincos3rdpi  26008  pige3ALT  26011  abssinper  26012  coskpi  26014  sineq0  26015  coseq1  26016  efeq1  26019  efif1olem4  26036  eflogeq  26092  tanarg  26109  cxpsqrtlem  26192  cxpsqrt  26193  logsqrt  26194  2irrexpq  26220  root1eq1  26243  cxpeq  26245  2logb9irrALT  26283  sqrt2cxp2logb9e3  26284  ang180lem2  26295  ang180lem3  26296  quad2  26324  1cubrlem  26326  1cubr  26327  dcubic2  26329  dcubic1  26330  dcubic  26331  mcubic  26332  cubic2  26333  cubic  26334  dquartlem1  26336  dquartlem2  26337  dquart  26338  quart1lem  26340  quart1  26341  quartlem1  26342  quartlem2  26343  quartlem3  26344  quart  26346  sinasin  26374  asinsin  26377  atancj  26395  efiatan  26397  efiatan2  26402  2efiatan  26403  tanatan  26404  atantan  26408  atanbndlem  26410  atans2  26416  dvatan  26420  atantayl2  26423  leibpilem2  26426  log2cnv  26429  log2tlbnd  26430  log2ublem2  26432  log2ublem3  26433  log2ub  26434  birthday  26439  zetacvg  26499  basellem1  26565  basellem3  26567  basellem8  26572  basellem9  26573  cht3  26657  1sgm2ppw  26683  ppiub  26687  chtublem  26694  chtub  26695  perfect1  26711  perfectlem1  26712  perfectlem2  26713  perfect  26714  bcmax  26761  bcp1ctr  26762  bclbnd  26763  bpos1lem  26765  bpos1  26766  bposlem1  26767  bposlem2  26768  bposlem4  26770  bposlem5  26771  bposlem6  26772  bposlem8  26774  bposlem9  26775  lgsdir2lem2  26809  gausslemma2dlem6  26855  lgsquadlem1  26863  lgsquadlem2  26864  lgsquad2lem2  26868  m1lgs  26871  2lgslem3a  26879  2lgslem3b  26880  2lgslem3c  26881  2lgslem3d  26882  2lgsoddprmlem2  26892  2lgsoddprmlem3c  26895  2lgsoddprmlem3d  26896  addsqnreup  26926  addsq2nreurex  26927  rplogsumlem1  26967  dchrisum0fno1  26994  dchrisum0lem1  26999  dchrisum0lem2  27001  logdivsum  27016  mulog2sumlem3  27019  log2sumbnd  27027  selberglem1  27028  selberglem2  27029  selberg2  27034  selberg4lem1  27043  selberg3r  27052  pntpbnd1a  27068  pntpbnd2  27070  pntibndlem2  27074  pntlemk  27089  ax5seglem7  28173  axlowdimlem13  28192  elwspths2spth  29201  clwlkclwwlklem2a4  29230  clwwlknonex2  29342  2clwwlk2  29581  numclwlk1lem1  29602  ex-fl  29680  ex-ceil  29681  ex-exp  29683  ex-fac  29684  ex-abs  29688  ex-ind-dvds  29694  ipidsq  29941  cncph  30050  ip0i  30056  ip1ilem  30057  ipdirilem  30060  minvecolem2  30106  hvsubcan2i  30295  norm-ii-i  30368  norm3lem  30380  normpar2i  30387  polid2i  30388  hhph  30409  mayete3i  30959  nmcexi  31257  opsqrlem6  31376  addltmulALT  31677  omssubadd  33237  oddpwdc  33291  fib5  33342  ballotlem2  33425  ballotth  33474  efmul2picn  33546  itgexpif  33556  vtscl  33588  circlemeth  33590  hgt750lemd  33598  logdivsqrle  33600  hgt750lem  33601  hgt750lem2  33602  problem4  34591  problem5  34592  quad3  34593  cnndvlem1  35351  sin2h  36416  cos2h  36417  tan2h  36418  poimirlem29  36455  mblfinlem1  36463  mblfinlem2  36464  mblfinlem3  36465  itg2addnclem3  36479  dvasin  36510  areacirc  36519  heiborlem6  36622  12gcd5e1  40806  12lcm5e60  40811  60lcm7e420  40813  420lcm8e840  40814  3exp7  40856  3lexlogpow5ineq1  40857  3lexlogpow2ineq2  40862  3lexlogpow5ineq5  40863  aks4d1p1p5  40878  aks4d1p1  40879  facp2  40897  fac2xp3  40958  2xp3dxp2ge1d  40960  sqn5i  41147  235t711  41153  ex-decpmul  41154  fltne  41330  flt4lem5e  41342  3cubeslem3l  41357  3cubeslem3r  41358  rmxluc  41608  rmyluc  41609  jm2.17a  41632  jm2.18  41660  jm2.23  41668  jm3.1lem1  41689  proot1ex  41876  areaquad  41898  sqrtcval  42325  resqrtvalex  42329  lhe4.4ex1a  43021  sineq0ALT  43631  coskpi2  44517  cosnegpi  44518  cosknegpi  44520  stoweidlem26  44677  wallispilem4  44719  wallispi  44721  wallispi2lem1  44722  stirlinglem8  44732  dirkerper  44747  dirkertrigeqlem3  44751  dirkertrigeq  44752  dirkeritg  44753  dirkercncflem1  44754  dirkercncflem2  44755  fourierdlem57  44814  fourierdlem58  44815  fourierdlem62  44819  fourierdlem76  44833  fourierdlem103  44860  fourierdlem104  44861  sqwvfourb  44880  fourierswlem  44881  fmtnoge3  46133  fmtnorec1  46140  fmtno0  46143  fmtno1  46144  fmtnorec3  46151  fmtnorec4  46152  fmtno5lem2  46157  fmtno5lem4  46159  257prm  46164  fmtnoprmfac2lem1  46169  fmtno4prmfac  46175  fmtno5faclem2  46183  fmtno5faclem3  46184  fmtno5fac  46185  139prmALT  46199  31prm  46200  127prm  46202  mod42tp1mod8  46205  lighneallem2  46209  lighneallem3  46210  lighneallem4a  46211  3exp4mod41  46219  41prothprmlem1  46220  41prothprmlem2  46221  41prothprm  46222  bits0ALTV  46282  0evenALTV  46291  6even  46314  8even  46316  perfectALTVlem1  46324  perfectALTVlem2  46325  perfectALTV  46326  2exp340mod341  46336  8exp8mod9  46339  mogoldbb  46388  nnsum3primes4  46391  bgoldbtbndlem1  46408  0nodd  46515  0even  46731  2even  46733  2zrngamgm  46739  2t6m3t4e0  46926  linevalexample  46978  zlmodzxzequap  47082  pw2m1lepw2m1  47103  nnlog2ge0lt1  47154  logbpw2m1  47155  nnpw2blen  47168  nnpw2pmod  47171  blen1  47172  blen2  47173  blennnt2  47177  nnolog2flm1  47178  0dig2nn0e  47200  0dig2nn0o  47201  nn0sumshdiglemA  47207  nn0sumshdiglemB  47208  nn0sumshdiglem1  47209  nn0sumshdiglem2  47210  ackval1012  47278  ackval2012  47279  ackval3012  47280  ackval42  47284  sinhpcosh  47687