Theorem 2cn 12287

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  2c2 12267

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 11168  ax-addcl 11170

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

This theorem is referenced by:  2ex  12289  2cnd  12290  3cn  12293  2m1e1  12338  3m1e2  12340  2p2e4  12347  times2  12349  2div2e1  12353  1p2e3ALT  12356  3p3e6  12364  4p3e7  12366  5p3e8  12369  6p3e9  12372  2t1e2  12375  2t2e4  12376  3t3e9  12379  2t0e0  12381  4d2e2  12382  2cnne0  12422  halfcn  12427  1mhlfehlf  12431  8th4div3  12432  halfpm6th  12433  2mulicn  12435  2muline0  12436  halfcl  12437  half0  12439  2halves  12440  halfaddsub  12445  div4p1lem1div2  12467  3halfnz  12641  zneo  12645  nneo  12646  zeo  12648  7p3e10  12752  4t4e16  12776  6t3e18  12782  7t7e49  12791  8t5e40  12795  9t9e81  12806  decbin0  12817  decbin2  12818  halfthird  12820  fztpval  13563  fz0tp  13602  fz0to4untppr  13604  fzo0to3tp  13718  fzo1to4tp  13720  expubnd  14142  sq2  14161  sq4e2t8  14163  cu2  14164  subsq2  14175  binom2sub  14183  binom3  14187  zesq  14189  fac2  14239  fac3  14240  faclbnd2  14251  faclbnd4lem1  14253  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd5  14258  bcn2  14279  4bc2eq6  14289  swrd2lsw  14903  crre  15061  addcj  15095  imval2  15098  01sqrexlem7  15195  absmax  15276  rddif  15287  sqreulem  15306  amgm2  15316  abs3lemi  15357  iseraltlem2  15629  ackbijnn  15774  climcndslem1  15795  climcndslem2  15796  arisum  15806  arisum2  15807  geo2sum2  15820  geo2lim  15821  geoihalfsum  15828  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  efcllem  16021  ege2le3  16033  efgt0  16046  tanval2  16076  tanval3  16077  efi4p  16080  efival  16095  sinadd  16107  cosadd  16108  sinmul  16115  cos2tsin  16122  ef01bndlem  16127  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  cos01gt0  16134  sin02gt0  16135  sin4lt0  16138  odd2np1lem  16283  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  nno  16325  nn0o  16326  flodddiv4  16356  bits0  16369  bitsfzolem  16375  0bits  16380  bitsinv1  16383  sadcadd  16399  smumullem  16433  6gcd4e2  16480  3lcm2e6woprm  16552  6lcm4e12  16553  pythagtriplem1  16749  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem15  16762  pythagtriplem16  16763  pythagtriplem17  16764  iserodd  16768  prmreclem5  16853  prmreclem6  16854  4sqlem11  16888  4sqlem12  16889  prmo2  16973  prmo3  16974  dec5dvds  16997  dec2nprm  17000  decexp2  17008  2exp5  17019  2exp6  17020  2exp7  17021  2exp8  17022  2exp11  17023  2exp16  17024  7prm  17044  11prm  17048  13prm  17049  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  psgnunilem2  19363  efgtlen  19594  efgredleme  19611  frgpnabllem1  19741  lt6abl  19763  htpycc  24496  pcoval2  24532  pcocn  24533  pcohtpylem  24535  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  csbren  24916  minveclem2  24943  ovolunlem1a  25013  ovolunlem1  25014  vitalilem4  25128  mbfi1fseqlem5  25237  dvmptre  25486  dvsincos  25498  aaliou3lem2  25856  aaliou3lem3  25857  aaliou3lem8  25858  coscn  25957  sinhalfpilem  25973  cospi  25982  ef2pi  25987  ef2kpi  25988  efper  25989  sinperlem  25990  sin2kpi  25993  cos2kpi  25994  sin2pim  25995  cos2pim  25996  sincosq3sgn  26010  sincosq4sgn  26011  tangtx  26015  sinq12gt0  26017  sincosq1eq  26022  sincos4thpi  26023  sincos6thpi  26025  sincos3rdpi  26026  pige3ALT  26029  abssinper  26030  coskpi  26032  sineq0  26033  coseq1  26034  efeq1  26037  efif1olem4  26054  eflogeq  26110  tanarg  26127  cxpsqrtlem  26210  cxpsqrt  26211  logsqrt  26212  2irrexpq  26239  root1eq1  26263  cxpeq  26265  2logb9irrALT  26303  sqrt2cxp2logb9e3  26304  ang180lem2  26315  ang180lem3  26316  quad2  26344  1cubrlem  26346  1cubr  26347  dcubic2  26349  dcubic1  26350  dcubic  26351  mcubic  26352  cubic2  26353  cubic  26354  dquartlem1  26356  dquartlem2  26357  dquart  26358  quart1lem  26360  quart1  26361  quartlem1  26362  quartlem2  26363  quartlem3  26364  quart  26366  sinasin  26394  asinsin  26397  atancj  26415  efiatan  26417  efiatan2  26422  2efiatan  26423  tanatan  26424  atantan  26428  atanbndlem  26430  atans2  26436  dvatan  26440  atantayl2  26443  leibpilem2  26446  log2cnv  26449  log2tlbnd  26450  log2ublem2  26452  log2ublem3  26453  log2ub  26454  birthday  26459  zetacvg  26519  basellem1  26585  basellem3  26587  basellem8  26592  basellem9  26593  cht3  26677  1sgm2ppw  26703  ppiub  26707  chtublem  26714  chtub  26715  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  bcmax  26781  bcp1ctr  26782  bclbnd  26783  bpos1lem  26785  bpos1  26786  bposlem1  26787  bposlem2  26788  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem8  26794  bposlem9  26795  lgsdir2lem2  26829  gausslemma2dlem6  26875  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem2  26888  m1lgs  26891  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgsoddprmlem2  26912  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  addsqnreup  26946  addsq2nreurex  26947  rplogsumlem1  26987  dchrisum0fno1  27014  dchrisum0lem1  27019  dchrisum0lem2  27021  logdivsum  27036  mulog2sumlem3  27039  log2sumbnd  27047  selberglem1  27048  selberglem2  27049  selberg2  27054  selberg4lem1  27063  selberg3r  27072  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemk  27109  ax5seglem7  28193  axlowdimlem13  28212  elwspths2spth  29221  clwlkclwwlklem2a4  29250  clwwlknonex2  29362  2clwwlk2  29601  numclwlk1lem1  29622  ex-fl  29700  ex-ceil  29701  ex-exp  29703  ex-fac  29704  ex-abs  29708  ex-ind-dvds  29714  ipidsq  29963  cncph  30072  ip0i  30078  ip1ilem  30079  ipdirilem  30082  minvecolem2  30128  hvsubcan2i  30317  norm-ii-i  30390  norm3lem  30402  normpar2i  30409  polid2i  30410  hhph  30431  mayete3i  30981  nmcexi  31279  opsqrlem6  31398  addltmulALT  31699  omssubadd  33299  oddpwdc  33353  fib5  33404  ballotlem2  33487  ballotth  33536  efmul2picn  33608  itgexpif  33618  vtscl  33650  circlemeth  33652  hgt750lemd  33660  logdivsqrle  33662  hgt750lem  33663  hgt750lem2  33664  problem4  34653  problem5  34654  quad3  34655  cnndvlem1  35413  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem29  36517  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  itg2addnclem3  36541  dvasin  36572  areacirc  36581  heiborlem6  36684  12gcd5e1  40868  12lcm5e60  40873  60lcm7e420  40875  420lcm8e840  40876  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1p1p5  40940  aks4d1p1  40941  facp2  40959  fac2xp3  41020  2xp3dxp2ge1d  41022  sqn5i  41197  235t711  41205  ex-decpmul  41206  fltne  41386  flt4lem5e  41398  sum9cubes  41414  3cubeslem3l  41424  3cubeslem3r  41425  rmxluc  41675  rmyluc  41676  jm2.17a  41699  jm2.18  41727  jm2.23  41735  jm3.1lem1  41756  proot1ex  41943  areaquad  41965  sqrtcval  42392  resqrtvalex  42396  lhe4.4ex1a  43088  sineq0ALT  43698  coskpi2  44582  cosnegpi  44583  cosknegpi  44585  stoweidlem26  44742  wallispilem4  44784  wallispi  44786  wallispi2lem1  44787  stirlinglem8  44797  dirkerper  44812  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkeritg  44818  dirkercncflem1  44819  dirkercncflem2  44820  fourierdlem57  44879  fourierdlem58  44880  fourierdlem62  44884  fourierdlem76  44898  fourierdlem103  44925  fourierdlem104  44926  sqwvfourb  44945  fourierswlem  44946  fmtnoge3  46198  fmtnorec1  46205  fmtno0  46208  fmtno1  46209  fmtnorec3  46216  fmtnorec4  46217  fmtno5lem2  46222  fmtno5lem4  46224  257prm  46229  fmtnoprmfac2lem1  46234  fmtno4prmfac  46240  fmtno5faclem2  46248  fmtno5faclem3  46249  fmtno5fac  46250  139prmALT  46264  31prm  46265  127prm  46267  mod42tp1mod8  46270  lighneallem2  46274  lighneallem3  46275  lighneallem4a  46276  3exp4mod41  46284  41prothprmlem1  46285  41prothprmlem2  46286  41prothprm  46287  bits0ALTV  46347  0evenALTV  46356  6even  46379  8even  46381  perfectALTVlem1  46389  perfectALTVlem2  46390  perfectALTV  46391  2exp340mod341  46401  8exp8mod9  46404  mogoldbb  46453  nnsum3primes4  46456  bgoldbtbndlem1  46473  0nodd  46580  0even  46829  2even  46831  2zrngamgm  46837  2t6m3t4e0  47024  linevalexample  47076  zlmodzxzequap  47180  pw2m1lepw2m1  47201  nnlog2ge0lt1  47252  logbpw2m1  47253  nnpw2blen  47266  nnpw2pmod  47269  blen1  47270  blen2  47271  blennnt2  47275  nnolog2flm1  47276  0dig2nn0e  47298  0dig2nn0o  47299  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  nn0sumshdiglem2  47308  ackval1012  47376  ackval2012  47377  ackval3012  47378  ackval42  47382  sinhpcosh  47785