Theorem 2cn 12421

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 12408	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11261	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11318	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2856	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  1c1 11204   + caddc 11206  2c2 12400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-addcl 11263

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-2 12408

This theorem is used by:  2ex  12423  2cnd  12424  3cn  12427  2thalfe1  12453  2m1e1OLD  12471  3m1e2  12473  2p2e4  12480  times2  12482  2div2e1  12486  1p2e3ALT  12489  3p3e6  12497  4p3e7  12499  5p3e8  12502  6p3e9  12505  2t1e2  12508  2t2e4  12509  2t3e6  12512  3t3e9  12513  2t4e8  12515  2t0e0  12516  4div2e2  12517  2cnne0  12558  halfcn  12563  2halves  12567  8th4div3  12569  halfthird  12570  halfpm6th  12571  2mulicn  12573  2muline0  12574  halfcl  12575  half0  12577  halfaddsub  12582  div4p1lem1div2  12604  3halfnz  12781  zneo  12785  nneo  12786  zeo  12788  7p3e10  12897  4t4e16  12921  6t3e18  12927  7t7e49  12936  8t5e40  12940  9t9e81  12951  decbin0  12964  decbin2  12965  fztpval  13723  fz0tp  13765  fzo0to3tp  13890  fzo1to4tp  13892  expubnd  14324  sq2  14343  sq4e2t8  14345  cu2  14346  subsq2  14358  binom2sub  14367  binom3  14371  zesq  14373  fac2  14426  faclbnd2  14438  faclbnd4lem1  14440  faclbnd4lem3  14442  faclbnd4lem4  14443  faclbnd5  14445  bcn2  14466  4bc2eq6  14476  swrd2lsw  15110  crre  15286  addcj  15320  imval2  15323  01sqrexlem7  15420  absmax  15502  sqreulem  15532  amgm2  15542  abs3lemi  15583  iseraltlem2  15855  ackbijnn  16002  climcndslem1  16023  climcndslem2  16024  arisum  16034  arisum2  16035  geo2sum2  16048  geo2lim  16049  geoihalfsum  16056  bpoly2  16228  bpoly3  16229  bpoly4  16230  fsumcube  16231  efcllem  16248  ege2le3  16261  efgt0  16276  tanval2  16306  tanval3  16307  efi4p  16310  efival  16325  sinadd  16337  cosadd  16338  sinmul  16345  cos2tsin  16352  ef01bndlem  16357  cos01bnd  16359  cos1bnd  16360  cos2bnd  16361  cos01gt0  16364  sin02gt0  16365  sin4lt0  16368  odd2np1lem  16515  odd2np1  16516  opoe  16538  omoe  16539  opeo  16540  omeo  16541  nno  16557  nn0o  16558  flodddiv4  16590  bits0  16603  bitsfzolem  16609  0bits  16614  bitsinv1  16617  sadcadd  16633  smumullem  16667  6gcd4e2  16716  3lcm2e6woprm  16795  6lcm4e12  16796  pythagtriplem1  16999  pythagtriplem12  17009  pythagtriplem14  17011  pythagtriplem15  17012  pythagtriplem16  17013  pythagtriplem17  17014  iserodd  17018  prmreclem5  17103  prmreclem6  17104  4sqlem11  17138  4sqlem12  17139  prmo2  17223  dec5dvds  17247  dec2nprm  17250  2exp5  17268  2exp7  17270  2exp11  17272  2exp16  17273  10nprm  17296  11prm  17298  13prm  17299  37prm  17304  43prm  17305  83prm  17306  139prm  17307  163prm  17308  317prm  17309  631prm  17310  1259lem1  17314  1259lem2  17315  1259lem3  17316  1259lem4  17317  1259lem5  17318  1259prm  17319  2503lem1  17320  2503lem2  17321  2503lem3  17322  4001lem1  17324  4001lem2  17325  4001lem3  17326  4001lem4  17327  4001prm  17328  psgnunilem2  19714  efgtlen  19945  efgredleme  19962  frgpnabllem1  20092  lt6abl  20114  pcoass  25350  pcorevlem  25352  csbren  25725  minveclem2  25752  ovolunlem1a  25822  ovolunlem1  25823  vitalilem4  25937  mbfi1fseqlem5  26045  dvmptre  26294  dvsincos  26306  aaliou3lem2  26675  aaliou3lem3  26676  aaliou3lem8  26677  coscn  26777  2picn  26791  sinhalfpilem  26797  cospi  26806  ef2pi  26811  ef2kpi  26812  efper  26813  sinperlem  26814  sin2kpi  26817  cos2kpi  26818  sin2pim  26819  cos2pim  26820  sincosq3sgn  26834  sincosq4sgn  26835  tangtx  26839  sinq12gt0  26841  sincosq1eq  26846  sincos4thpi  26847  sincos6thpi  26849  sincos3rdpi  26850  pige3ALT  26853  abssinper  26854  coskpi  26856  sineq0  26857  coseq1  26858  efeq1  26861  efif1olem4  26878  eflogeq  26935  tanarg  26952  cxpsqrtlem  27035  cxpsqrt  27036  logsqrt  27037  2irrexpq  27064  root1eq1  27088  cxpeq  27090  2logb9irrALT  27131  sqrt2cxp2logb9e3  27132  ang180lem2  27143  ang180lem3  27144  quad2  27172  1cubrlem  27174  1cubr  27175  dcubic2  27177  dcubic1  27178  dcubic  27179  mcubic  27180  cubic2  27181  cubic  27182  dquartlem1  27184  dquartlem2  27185  dquart  27186  quart1lem  27188  quart1  27189  quartlem1  27190  quartlem2  27191  quartlem3  27192  quart  27194  sinasin  27222  asinsin  27225  atancj  27243  efiatan  27245  efiatan2  27250  2efiatan  27251  tanatan  27252  atantan  27256  atanbndlem  27258  atans2  27264  dvatan  27268  atantayl2  27271  leibpilem2  27274  log2cnv  27277  log2tlbnd  27278  log2ublem2  27280  log2ublem3  27281  log2ub  27282  birthday  27287  zetacvg  27347  basellem1  27413  basellem3  27415  basellem8  27420  basellem9  27421  1sgm2ppw  27532  ppiub  27536  chtublem  27543  chtub  27544  perfect1  27560  perfectlem1  27561  perfectlem2  27562  perfect  27563  bcmax  27610  bcp1ctr  27611  bclbnd  27612  bpos1lem  27614  bpos1  27615  bposlem1  27616  bposlem2  27617  bposlem4  27619  bposlem5  27620  bposlem6  27621  bposlem8  27623  bposlem9  27624  lgsdir2lem2  27658  gausslemma2dlem6  27704  lgsquadlem1  27712  lgsquadlem2  27713  lgsquad2lem2  27717  m1lgs  27720  2lgslem3a  27728  2lgslem3b  27729  2lgslem3c  27730  2lgslem3d  27731  2lgsoddprmlem2  27741  2lgsoddprmlem3c  27744  2lgsoddprmlem3d  27745  addsqnreup  27775  addsq2nreurex  27776  rplogsumlem1  27816  dchrisum0fno1  27843  dchrisum0lem1  27848  dchrisum0lem2  27850  logdivsum  27865  mulog2sumlem3  27868  log2sumbnd  27876  selberglem1  27877  selberglem2  27878  selberg2  27883  selberg4lem1  27892  selberg3r  27901  pntpbnd1a  27917  pntpbnd2  27919  pntibndlem2  27923  pntlemk  27938  fltne  27980  flt4lem5e  27991  fltoprmlem2  27999  ax5seglem7  29518  axlowdimlem13  29537  elwspths2spth  30564  clwlkclwwlklem2a4  30593  clwwlknonex2  30705  2clwwlk2  30954  numclwlk1lem1  30975  ex-fl  31053  ex-ceil  31054  ex-exp  31056  ex-fac  31057  ex-abs  31061  ex-ind-dvds  31067  ipidsq  31317  cncph  31426  ip0i  31432  ip1ilem  31433  ipdirilem  31436  minvecolem2  31482  hvsubcan2i  31671  norm-ii-i  31744  norm3lem  31756  normpar2i  31763  polid2i  31764  hhph  31785  mayete3i  32335  nmcexi  32633  opsqrlem6  32752  addltmulALT  33095  ply1dg3rt0irred  34162  fldext2chn  34406  constrelextdg2  34425  2sqr3minply  34458  cos9thpiminplylem4  34463  cos9thpiminplylem5  34464  oddpwdc  35032  fib5  35083  ballotlem2  35167  ballotth  35216  efmul2picn  35271  itgexpif  35281  vtscl  35313  circlemeth  35315  hgt750lemd  35323  logdivsqrle  35325  hgt750lem  35326  hgt750lem2  35327  problem4  36519  problem5  36520  quad3  36521  cnndvlem1  37495  sin2h  38626  cos2h  38627  tan2h  38628  poimirlem29  38660  mblfinlem1  38668  mblfinlem2  38669  mblfinlem3  38670  itg2addnclem3  38684  dvasin  38715  areacirc  38724  heiborlem6  38843  12gcd5e1  43146  12lcm5e60  43151  60lcm7e420  43153  3exp7  43196  3lexlogpow5ineq1  43197  3lexlogpow5ineq5  43203  aks4d1p1p5  43218  aks4d1p1  43219  posbezout  43243  facp2  43286  25or6to4  43349  4p4e8ALT  43402  1p3e4  43403  2p3e5  43409  2p4e6  43410  2p5e7  43411  2p6e8  43412  2p7e9  43413  3p4e7  43414  3p5e8  43415  sqn5i  43435  235t711  43455  ex-decpmul  43456  cxp112d  43485  cxp111d  43486  cxpi11d  43487  tanhalfpim  43493  sum9cubes  43776  3cubeslem3r  43790  rmxluc  44036  rmyluc  44037  jm2.17a  44060  jm2.18  44088  jm2.23  44096  jm3.1lem1  44117  proot1ex  44291  areaquad  44311  sqrtcval  44734  resqrtvalex  44738  lhe4.4ex1a  45406  sineq0ALT  46012  coskpi2  46969  cosnegpi  46970  cosknegpi  46972  stoweidlem26  47129  wallispilem4  47171  wallispi  47173  wallispi2lem1  47174  stirlinglem8  47184  dirkerper  47199  dirkertrigeqlem3  47203  dirkertrigeq  47204  dirkeritg  47205  dirkercncflem1  47206  fourierdlem57  47266  fourierdlem58  47267  fourierdlem62  47271  fourierdlem76  47285  fourierdlem103  47312  fourierdlem104  47313  sqwvfourb  47332  fourierswlem  47333  sin5tlem1  48012  sin5tlem5  48016  cos5t  48018  goldpolyfactor  48020  goldrasin  48022  goldracos5teq  48025  goldratmolem2  48026  goldratmolem3  48027  goldratmolem4  48028  rehalfge1  48502  ceil5half3  48509  modm2nep1  48535  modm1nep2  48537  modm1nem2  48538  fmtnoge3  48708  fmtnorec1  48715  fmtno0  48718  fmtno1  48719  fmtnorec3  48726  fmtnorec4  48727  fmtno5lem2  48732  fmtno5lem4  48734  257prm  48739  fmtnoprmfac2lem1  48744  fmtno4prmfac  48750  fmtno5faclem2  48758  fmtno5faclem3  48759  fmtno5fac  48760  139prmALT  48774  31prm  48775  127prm  48777  lighneallem2  48784  lighneallem3  48785  lighneallem4a  48786  3exp4mod41  48794  41prothprmlem1  48795  41prothprmlem2  48796  41prothprm  48797  bits0ALTV  48870  0evenALTV  48879  6even  48902  8even  48904  perfectALTVlem1  48912  perfectALTVlem2  48913  perfectALTV  48914  2exp340mod341  48924  mogoldbb  48976  nnsum3primes4  48979  bgoldbtbndlem1  48996  gpg5order  49251  gpg5edgnedg  49321  0nodd  49360  0even  49427  2even  49429  2zrngamgm  49435  2t6m3t4e0  49553  linevalexample  49600  zlmodzxzequap  49704  pw2m1lepw2m1  49725  nnlog2ge0lt1  49771  logbpw2m1  49772  nnpw2blen  49785  nnpw2pmod  49788  blen1  49789  blen2  49790  blennnt2  49794  nnolog2flm1  49795  0dig2nn0e  49817  0dig2nn0o  49818  nn0sumshdiglemA  49824  nn0sumshdiglemB  49825  nn0sumshdiglem1  49826  nn0sumshdiglem2  49827  ackval1012  49895  ackval2012  49896  ackval3012  49897  ackval42  49901  sinhpcosh  51001