Theorem 2cn 12232

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 12220	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11150	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2833	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  2c2 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220

This theorem is referenced by:  2ex  12234  2cnd  12235  3cn  12238  2m1e1  12278  3m1e2  12280  2p2e4  12287  times2  12289  2div2e1  12293  1p2e3ALT  12296  3p3e6  12304  4p3e7  12306  5p3e8  12309  6p3e9  12312  2t1e2  12315  2t2e4  12316  3t3e9  12319  2t0e0  12321  4div2e2  12322  2cnne0  12362  halfcn  12367  2halves  12371  8th4div3  12373  halfthird  12374  halfpm6th  12375  2mulicn  12377  2muline0  12378  halfcl  12379  half0  12381  halfaddsub  12386  div4p1lem1div2  12408  3halfnz  12583  zneo  12587  nneo  12588  zeo  12590  7p3e10  12694  4t4e16  12718  6t3e18  12724  7t7e49  12733  8t5e40  12737  9t9e81  12748  decbin0  12759  decbin2  12760  fztpval  13514  fz0tp  13556  fzo0to3tp  13680  fzo1to4tp  13682  expubnd  14113  sq2  14132  sq4e2t8  14134  cu2  14135  subsq2  14146  binom2sub  14155  binom3  14159  zesq  14161  fac2  14214  fac3  14215  faclbnd2  14226  faclbnd4lem1  14228  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd5  14233  bcn2  14254  4bc2eq6  14264  swrd2lsw  14887  crre  15049  addcj  15083  imval2  15086  01sqrexlem7  15183  absmax  15265  rddif  15276  sqreulem  15295  amgm2  15305  abs3lemi  15346  iseraltlem2  15618  ackbijnn  15763  climcndslem1  15784  climcndslem2  15785  arisum  15795  arisum2  15796  geo2sum2  15809  geo2lim  15810  geoihalfsum  15817  bpoly2  15992  bpoly3  15993  bpoly4  15994  fsumcube  15995  efcllem  16012  ege2le3  16025  efgt0  16040  tanval2  16070  tanval3  16071  efi4p  16074  efival  16089  sinadd  16101  cosadd  16102  sinmul  16109  cos2tsin  16116  ef01bndlem  16121  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  cos01gt0  16128  sin02gt0  16129  sin4lt0  16132  odd2np1lem  16279  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  nno  16321  nn0o  16322  flodddiv4  16354  bits0  16367  bitsfzolem  16373  0bits  16378  bitsinv1  16381  sadcadd  16397  smumullem  16431  6gcd4e2  16477  3lcm2e6woprm  16554  6lcm4e12  16555  pythagtriplem1  16756  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem15  16769  pythagtriplem16  16770  pythagtriplem17  16771  iserodd  16775  prmreclem5  16860  prmreclem6  16861  4sqlem11  16895  4sqlem12  16896  prmo2  16980  prmo3  16981  dec5dvds  17004  dec2nprm  17007  2exp5  17025  2exp6  17026  2exp7  17027  2exp8  17028  2exp11  17029  2exp16  17030  7prm  17050  11prm  17054  13prm  17055  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  psgnunilem2  19436  efgtlen  19667  efgredleme  19684  frgpnabllem1  19814  lt6abl  19836  htpycc  24947  pcoval2  24984  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  csbren  25367  minveclem2  25394  ovolunlem1a  25465  ovolunlem1  25466  vitalilem4  25580  mbfi1fseqlem5  25688  dvmptre  25941  dvsincos  25953  aaliou3lem2  26319  aaliou3lem3  26320  aaliou3lem8  26321  coscn  26423  sinhalfpilem  26440  cospi  26449  ef2pi  26454  ef2kpi  26455  efper  26456  sinperlem  26457  sin2kpi  26460  cos2kpi  26461  sin2pim  26462  cos2pim  26463  sincosq3sgn  26477  sincosq4sgn  26478  tangtx  26482  sinq12gt0  26484  sincosq1eq  26489  sincos4thpi  26490  sincos6thpi  26493  sincos3rdpi  26494  pige3ALT  26497  abssinper  26498  coskpi  26500  sineq0  26501  coseq1  26502  efeq1  26505  efif1olem4  26522  eflogeq  26579  tanarg  26596  cxpsqrtlem  26679  cxpsqrt  26680  logsqrt  26681  2irrexpq  26708  root1eq1  26733  cxpeq  26735  2logb9irrALT  26776  sqrt2cxp2logb9e3  26777  ang180lem2  26788  ang180lem3  26789  quad2  26817  1cubrlem  26819  1cubr  26820  dcubic2  26822  dcubic1  26823  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  quartlem3  26837  quart  26839  sinasin  26867  asinsin  26870  atancj  26888  efiatan  26890  efiatan2  26895  2efiatan  26896  tanatan  26897  atantan  26901  atanbndlem  26903  atans2  26909  dvatan  26913  atantayl2  26916  leibpilem2  26919  log2cnv  26922  log2tlbnd  26923  log2ublem2  26925  log2ublem3  26926  log2ub  26927  birthday  26932  zetacvg  26993  basellem1  27059  basellem3  27061  basellem8  27066  basellem9  27067  cht3  27151  1sgm2ppw  27179  ppiub  27183  chtublem  27190  chtub  27191  perfect1  27207  perfectlem1  27208  perfectlem2  27209  perfect  27210  bcmax  27257  bcp1ctr  27258  bclbnd  27259  bpos1lem  27261  bpos1  27262  bposlem1  27263  bposlem2  27264  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem8  27270  bposlem9  27271  lgsdir2lem2  27305  gausslemma2dlem6  27351  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem2  27364  m1lgs  27367  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgsoddprmlem2  27388  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  addsqnreup  27422  addsq2nreurex  27423  rplogsumlem1  27463  dchrisum0fno1  27490  dchrisum0lem1  27495  dchrisum0lem2  27497  logdivsum  27512  mulog2sumlem3  27515  log2sumbnd  27523  selberglem1  27524  selberglem2  27525  selberg2  27530  selberg4lem1  27539  selberg3r  27548  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem2  27570  pntlemk  27585  ax5seglem7  29020  axlowdimlem13  29039  elwspths2spth  30055  clwlkclwwlklem2a4  30084  clwwlknonex2  30196  2clwwlk2  30435  numclwlk1lem1  30456  ex-fl  30534  ex-ceil  30535  ex-exp  30537  ex-fac  30538  ex-abs  30542  ex-ind-dvds  30548  ipidsq  30797  cncph  30906  ip0i  30912  ip1ilem  30913  ipdirilem  30916  minvecolem2  30962  hvsubcan2i  31151  norm-ii-i  31224  norm3lem  31236  normpar2i  31243  polid2i  31244  hhph  31265  mayete3i  31815  nmcexi  32113  opsqrlem6  32232  addltmulALT  32533  ply1dg3rt0irred  33676  fldext2chn  33905  constrelextdg2  33924  2sqr3minply  33957  cos9thpiminplylem4  33962  cos9thpiminplylem5  33963  omssubadd  34477  oddpwdc  34531  fib5  34582  ballotlem2  34666  ballotth  34715  efmul2picn  34773  itgexpif  34783  vtscl  34815  circlemeth  34817  hgt750lemd  34825  logdivsqrle  34827  hgt750lem  34828  hgt750lem2  34829  problem4  35881  problem5  35882  quad3  35883  cnndvlem1  36756  sin2h  37855  cos2h  37856  tan2h  37857  poimirlem29  37894  mblfinlem1  37902  mblfinlem2  37903  mblfinlem3  37904  itg2addnclem3  37918  dvasin  37949  areacirc  37958  heiborlem6  38061  12gcd5e1  42367  12lcm5e60  42372  60lcm7e420  42374  420lcm8e840  42375  3exp7  42417  3lexlogpow5ineq1  42418  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1p1p5  42439  aks4d1p1  42440  posbezout  42464  facp2  42507  1p3e4  42623  sqn5i  42649  235t711  42669  ex-decpmul  42670  cxp112d  42705  cxp111d  42706  cxpi11d  42707  tanhalfpim  42713  fltne  42996  flt4lem5e  43008  sum9cubes  43024  3cubeslem3l  43037  3cubeslem3r  43038  rmxluc  43287  rmyluc  43288  jm2.17a  43311  jm2.18  43339  jm2.23  43347  jm3.1lem1  43368  proot1ex  43547  areaquad  43567  sqrtcval  43991  resqrtvalex  43995  lhe4.4ex1a  44679  sineq0ALT  45286  coskpi2  46218  cosnegpi  46219  cosknegpi  46221  stoweidlem26  46378  wallispilem4  46420  wallispi  46422  wallispi2lem1  46423  stirlinglem8  46433  dirkerper  46448  dirkertrigeqlem3  46452  dirkertrigeq  46453  dirkeritg  46454  dirkercncflem1  46455  dirkercncflem2  46456  fourierdlem57  46515  fourierdlem58  46516  fourierdlem62  46520  fourierdlem76  46534  fourierdlem103  46561  fourierdlem104  46562  sqwvfourb  46581  fourierswlem  46582  nthrucw  47238  rehalfge1  47689  ceil5half3  47694  modm2nep1  47720  modm1nep2  47722  modm1nem2  47723  fmtnoge3  47884  fmtnorec1  47891  fmtno0  47894  fmtno1  47895  fmtnorec3  47902  fmtnorec4  47903  fmtno5lem2  47908  fmtno5lem4  47910  257prm  47915  fmtnoprmfac2lem1  47920  fmtno4prmfac  47926  fmtno5faclem2  47934  fmtno5faclem3  47935  fmtno5fac  47936  139prmALT  47950  31prm  47951  127prm  47953  mod42tp1mod8  47956  lighneallem2  47960  lighneallem3  47961  lighneallem4a  47962  3exp4mod41  47970  41prothprmlem1  47971  41prothprmlem2  47972  41prothprm  47973  bits0ALTV  48033  0evenALTV  48042  6even  48065  8even  48067  perfectALTVlem1  48075  perfectALTVlem2  48076  perfectALTV  48077  2exp340mod341  48087  8exp8mod9  48090  mogoldbb  48139  nnsum3primes4  48142  bgoldbtbndlem1  48159  gpg5order  48414  gpg5edgnedg  48484  0nodd  48524  0even  48591  2even  48593  2zrngamgm  48599  2t6m3t4e0  48702  linevalexample  48749  zlmodzxzequap  48853  pw2m1lepw2m1  48874  nnlog2ge0lt1  48920  logbpw2m1  48921  nnpw2blen  48934  nnpw2pmod  48937  blen1  48938  blen2  48939  blennnt2  48943  nnolog2flm1  48944  0dig2nn0e  48966  0dig2nn0o  48967  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974  nn0sumshdiglem1  48975  nn0sumshdiglem2  48976  ackval1012  49044  ackval2012  49045  ackval3012  49046  ackval42  49050  sinhpcosh  50093