Theorem 2cn 12399

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 12386	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11239	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11296	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2857	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179  1c1 11182   + caddc 11184  2c2 12378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11239  ax-addcl 11241

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12386

This theorem is used by:  2ex  12401  2cnd  12402  3cn  12405  2thalfe1  12431  2m1e1OLD  12449  3m1e2  12451  2p2e4  12458  times2  12460  2div2e1  12464  1p2e3ALT  12467  3p3e6  12475  4p3e7  12477  5p3e8  12480  6p3e9  12483  2t1e2  12486  2t2e4  12487  2t3e6  12490  3t3e9  12491  2t4e8  12493  2t0e0  12494  4div2e2  12495  2cnne0  12536  halfcn  12541  2halves  12545  8th4div3  12547  halfthird  12548  halfpm6th  12549  2mulicn  12551  2muline0  12552  halfcl  12553  half0  12555  halfaddsub  12560  div4p1lem1div2  12582  3halfnz  12759  zneo  12763  nneo  12764  zeo  12766  7p3e10  12875  4t4e16  12899  6t3e18  12905  7t7e49  12914  8t5e40  12918  9t9e81  12929  decbin0  12942  decbin2  12943  fztpval  13700  fz0tp  13742  fzo0to3tp  13867  fzo1to4tp  13869  expubnd  14301  sq2  14320  sq4e2t8  14322  cu2  14323  subsq2  14335  binom2sub  14344  binom3  14348  zesq  14350  fac2  14403  faclbnd2  14415  faclbnd4lem1  14417  faclbnd4lem3  14419  faclbnd4lem4  14420  faclbnd5  14422  bcn2  14443  4bc2eq6  14453  swrd2lsw  15085  crre  15261  addcj  15295  imval2  15298  01sqrexlem7  15395  absmax  15477  sqreulem  15507  amgm2  15517  abs3lemi  15558  iseraltlem2  15830  ackbijnn  15977  climcndslem1  15998  climcndslem2  15999  arisum  16009  arisum2  16010  geo2sum2  16023  geo2lim  16024  geoihalfsum  16031  bpoly2  16203  bpoly3  16204  bpoly4  16205  fsumcube  16206  efcllem  16223  ege2le3  16236  efgt0  16251  tanval2  16281  tanval3  16282  efi4p  16285  efival  16300  sinadd  16312  cosadd  16313  sinmul  16320  cos2tsin  16327  ef01bndlem  16332  cos01bnd  16334  cos1bnd  16335  cos2bnd  16336  cos01gt0  16339  sin02gt0  16340  sin4lt0  16343  odd2np1lem  16490  odd2np1  16491  opoe  16513  omoe  16514  opeo  16515  omeo  16516  nno  16532  nn0o  16533  flodddiv4  16565  bits0  16578  bitsfzolem  16584  0bits  16589  bitsinv1  16592  sadcadd  16608  smumullem  16642  6gcd4e2  16691  3lcm2e6woprm  16770  6lcm4e12  16771  pythagtriplem1  16974  pythagtriplem12  16984  pythagtriplem14  16986  pythagtriplem15  16987  pythagtriplem16  16988  pythagtriplem17  16989  iserodd  16993  prmreclem5  17078  prmreclem6  17079  4sqlem11  17113  4sqlem12  17114  prmo2  17198  dec5dvds  17222  dec2nprm  17225  2exp5  17243  2exp7  17245  2exp11  17247  2exp16  17248  10nprm  17271  11prm  17273  13prm  17274  37prm  17279  43prm  17280  83prm  17281  139prm  17282  163prm  17283  317prm  17284  631prm  17285  1259lem1  17289  1259lem2  17290  1259lem3  17291  1259lem4  17292  1259lem5  17293  1259prm  17294  2503lem1  17295  2503lem2  17296  2503lem3  17297  4001lem1  17299  4001lem2  17300  4001lem3  17301  4001lem4  17302  4001prm  17303  psgnunilem2  19689  efgtlen  19920  efgredleme  19937  frgpnabllem1  20067  lt6abl  20089  pcoass  25325  pcorevlem  25327  csbren  25700  minveclem2  25727  ovolunlem1a  25797  ovolunlem1  25798  vitalilem4  25912  mbfi1fseqlem5  26020  dvmptre  26269  dvsincos  26281  aaliou3lem2  26652  aaliou3lem3  26653  aaliou3lem8  26654  coscn  26754  2picn  26768  sinhalfpilem  26774  cospi  26783  ef2pi  26788  ef2kpi  26789  efper  26790  sinperlem  26791  sin2kpi  26794  cos2kpi  26795  sin2pim  26796  cos2pim  26797  sincosq3sgn  26811  sincosq4sgn  26812  tangtx  26816  sinq12gt0  26818  sincosq1eq  26823  sincos4thpi  26824  sincos6thpi  26826  sincos3rdpi  26827  pige3ALT  26830  abssinper  26831  coskpi  26833  sineq0  26834  coseq1  26835  efeq1  26838  efif1olem4  26855  eflogeq  26912  tanarg  26929  cxpsqrtlem  27012  cxpsqrt  27013  logsqrt  27014  2irrexpq  27041  root1eq1  27065  cxpeq  27067  2logb9irrALT  27108  sqrt2cxp2logb9e3  27109  ang180lem2  27120  ang180lem3  27121  quad2  27149  1cubrlem  27151  1cubr  27152  dcubic2  27154  dcubic1  27155  dcubic  27156  mcubic  27157  cubic2  27158  cubic  27159  dquartlem1  27161  dquartlem2  27162  dquart  27163  quart1lem  27165  quart1  27166  quartlem1  27167  quartlem2  27168  quartlem3  27169  quart  27171  sinasin  27199  asinsin  27202  atancj  27220  efiatan  27222  efiatan2  27227  2efiatan  27228  tanatan  27229  atantan  27233  atanbndlem  27235  atans2  27241  dvatan  27245  atantayl2  27248  leibpilem2  27251  log2cnv  27254  log2tlbnd  27255  log2ublem2  27257  log2ublem3  27258  log2ub  27259  birthday  27264  zetacvg  27324  basellem1  27390  basellem3  27392  basellem8  27397  basellem9  27398  1sgm2ppw  27509  ppiub  27513  chtublem  27520  chtub  27521  perfect1  27537  perfectlem1  27538  perfectlem2  27539  perfect  27540  bcmax  27587  bcp1ctr  27588  bclbnd  27589  bpos1lem  27591  bpos1  27592  bposlem1  27593  bposlem2  27594  bposlem4  27596  bposlem5  27597  bposlem6  27598  bposlem8  27600  bposlem9  27601  lgsdir2lem2  27635  gausslemma2dlem6  27681  lgsquadlem1  27689  lgsquadlem2  27690  lgsquad2lem2  27694  m1lgs  27697  2lgslem3a  27705  2lgslem3b  27706  2lgslem3c  27707  2lgslem3d  27708  2lgsoddprmlem2  27718  2lgsoddprmlem3c  27721  2lgsoddprmlem3d  27722  addsqnreup  27752  addsq2nreurex  27753  rplogsumlem1  27793  dchrisum0fno1  27820  dchrisum0lem1  27825  dchrisum0lem2  27827  logdivsum  27842  mulog2sumlem3  27845  log2sumbnd  27853  selberglem1  27854  selberglem2  27855  selberg2  27860  selberg4lem1  27869  selberg3r  27878  pntpbnd1a  27894  pntpbnd2  27896  pntibndlem2  27900  pntlemk  27915  fltne  27957  flt4lem5e  27968  fltoprmlem2  27976  ax5seglem7  29495  axlowdimlem13  29514  elwspths2spth  30541  clwlkclwwlklem2a4  30570  clwwlknonex2  30682  2clwwlk2  30931  numclwlk1lem1  30952  ex-fl  31030  ex-ceil  31031  ex-exp  31033  ex-fac  31034  ex-abs  31038  ex-ind-dvds  31044  ipidsq  31294  cncph  31403  ip0i  31409  ip1ilem  31410  ipdirilem  31413  minvecolem2  31459  hvsubcan2i  31648  norm-ii-i  31721  norm3lem  31733  normpar2i  31740  polid2i  31741  hhph  31762  mayete3i  32312  nmcexi  32610  opsqrlem6  32729  addltmulALT  33030  ply1dg3rt0irred  34098  fldext2chn  34342  constrelextdg2  34361  2sqr3minply  34394  cos9thpiminplylem4  34399  cos9thpiminplylem5  34400  omssubadd  34915  oddpwdc  34969  fib5  35020  ballotlem2  35104  ballotth  35153  efmul2picn  35208  itgexpif  35218  vtscl  35250  circlemeth  35252  hgt750lemd  35260  logdivsqrle  35262  hgt750lem  35263  hgt750lem2  35264  problem4  36402  problem5  36403  quad3  36404  cnndvlem1  37373  sin2h  38501  cos2h  38502  tan2h  38503  poimirlem29  38535  mblfinlem1  38543  mblfinlem2  38544  mblfinlem3  38545  itg2addnclem3  38559  dvasin  38590  areacirc  38599  heiborlem6  38718  12gcd5e1  43021  12lcm5e60  43026  60lcm7e420  43028  3exp7  43071  3lexlogpow5ineq1  43072  3lexlogpow5ineq5  43078  aks4d1p1p5  43093  aks4d1p1  43094  posbezout  43118  facp2  43161  25or6to4  43224  4p4e8ALT  43277  1p3e4  43278  2p3e5  43284  2p4e6  43285  2p5e7  43286  2p6e8  43287  2p7e9  43288  3p4e7  43289  3p5e8  43290  sqn5i  43310  235t711  43330  ex-decpmul  43331  cxp112d  43360  cxp111d  43361  cxpi11d  43362  tanhalfpim  43368  sum9cubes  43637  3cubeslem3r  43651  rmxluc  43896  rmyluc  43897  jm2.17a  43920  jm2.18  43948  jm2.23  43956  jm3.1lem1  43977  proot1ex  44156  areaquad  44176  sqrtcval  44600  resqrtvalex  44604  lhe4.4ex1a  45272  sineq0ALT  45878  coskpi2  46820  cosnegpi  46821  cosknegpi  46823  stoweidlem26  46980  wallispilem4  47022  wallispi  47024  wallispi2lem1  47025  stirlinglem8  47035  dirkerper  47050  dirkertrigeqlem3  47054  dirkertrigeq  47055  dirkeritg  47056  dirkercncflem1  47057  fourierdlem57  47117  fourierdlem58  47118  fourierdlem62  47122  fourierdlem76  47136  fourierdlem103  47163  fourierdlem104  47164  sqwvfourb  47183  fourierswlem  47184  sin5tlem1  47863  sin5tlem5  47867  cos5t  47869  goldpolyfactor  47871  goldrasin  47873  goldracos5teq  47876  goldratmolem2  47877  goldratmolem3  47878  goldratmolem4  47879  rehalfge1  48353  ceil5half3  48360  modm2nep1  48386  modm1nep2  48388  modm1nem2  48389  fmtnoge3  48559  fmtnorec1  48566  fmtno0  48569  fmtno1  48570  fmtnorec3  48577  fmtnorec4  48578  fmtno5lem2  48583  fmtno5lem4  48585  257prm  48590  fmtnoprmfac2lem1  48595  fmtno4prmfac  48601  fmtno5faclem2  48609  fmtno5faclem3  48610  fmtno5fac  48611  139prmALT  48625  31prm  48626  127prm  48628  lighneallem2  48635  lighneallem3  48636  lighneallem4a  48637  3exp4mod41  48645  41prothprmlem1  48646  41prothprmlem2  48647  41prothprm  48648  bits0ALTV  48721  0evenALTV  48730  6even  48753  8even  48755  perfectALTVlem1  48763  perfectALTVlem2  48764  perfectALTV  48765  2exp340mod341  48775  mogoldbb  48827  nnsum3primes4  48830  bgoldbtbndlem1  48847  gpg5order  49102  gpg5edgnedg  49172  0nodd  49211  0even  49278  2even  49280  2zrngamgm  49286  2t6m3t4e0  49404  linevalexample  49451  zlmodzxzequap  49555  pw2m1lepw2m1  49576  nnlog2ge0lt1  49622  logbpw2m1  49623  nnpw2blen  49636  nnpw2pmod  49639  blen1  49640  blen2  49641  blennnt2  49645  nnolog2flm1  49646  0dig2nn0e  49668  0dig2nn0o  49669  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  nn0sumshdiglem1  49677  nn0sumshdiglem2  49678  ackval1012  49746  ackval2012  49747  ackval3012  49748  ackval42  49752  sinhpcosh  50777