Theorem 2cn 12268

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 12256	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11187	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2825	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  2c2 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256

This theorem is referenced by:  2ex  12270  2cnd  12271  3cn  12274  2m1e1  12314  3m1e2  12316  2p2e4  12323  times2  12325  2div2e1  12329  1p2e3ALT  12332  3p3e6  12340  4p3e7  12342  5p3e8  12345  6p3e9  12348  2t1e2  12351  2t2e4  12352  3t3e9  12355  2t0e0  12357  4d2e2  12358  2cnne0  12398  halfcn  12403  2halves  12407  8th4div3  12409  halfthird  12410  halfpm6th  12411  2mulicn  12413  2muline0  12414  halfcl  12415  half0  12417  halfaddsub  12422  div4p1lem1div2  12444  3halfnz  12620  zneo  12624  nneo  12625  zeo  12627  7p3e10  12731  4t4e16  12755  6t3e18  12761  7t7e49  12770  8t5e40  12774  9t9e81  12785  decbin0  12796  decbin2  12797  fztpval  13554  fz0tp  13596  fzo0to3tp  13720  fzo1to4tp  13722  expubnd  14150  sq2  14169  sq4e2t8  14171  cu2  14172  subsq2  14183  binom2sub  14192  binom3  14196  zesq  14198  fac2  14251  fac3  14252  faclbnd2  14263  faclbnd4lem1  14265  faclbnd4lem3  14267  faclbnd4lem4  14268  faclbnd5  14270  bcn2  14291  4bc2eq6  14301  swrd2lsw  14925  crre  15087  addcj  15121  imval2  15124  01sqrexlem7  15221  absmax  15303  rddif  15314  sqreulem  15333  amgm2  15343  abs3lemi  15384  iseraltlem2  15656  ackbijnn  15801  climcndslem1  15822  climcndslem2  15823  arisum  15833  arisum2  15834  geo2sum2  15847  geo2lim  15848  geoihalfsum  15855  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  efcllem  16050  ege2le3  16063  efgt0  16078  tanval2  16108  tanval3  16109  efi4p  16112  efival  16127  sinadd  16139  cosadd  16140  sinmul  16147  cos2tsin  16154  ef01bndlem  16159  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  cos01gt0  16166  sin02gt0  16167  sin4lt0  16170  odd2np1lem  16317  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  nno  16359  nn0o  16360  flodddiv4  16392  bits0  16405  bitsfzolem  16411  0bits  16416  bitsinv1  16419  sadcadd  16435  smumullem  16469  6gcd4e2  16515  3lcm2e6woprm  16592  6lcm4e12  16593  pythagtriplem1  16794  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem15  16807  pythagtriplem16  16808  pythagtriplem17  16809  iserodd  16813  prmreclem5  16898  prmreclem6  16899  4sqlem11  16933  4sqlem12  16934  prmo2  17018  prmo3  17019  dec5dvds  17042  dec2nprm  17045  2exp5  17063  2exp6  17064  2exp7  17065  2exp8  17066  2exp11  17067  2exp16  17068  7prm  17088  11prm  17092  13prm  17093  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  psgnunilem2  19432  efgtlen  19663  efgredleme  19680  frgpnabllem1  19810  lt6abl  19832  htpycc  24886  pcoval2  24923  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  csbren  25306  minveclem2  25333  ovolunlem1a  25404  ovolunlem1  25405  vitalilem4  25519  mbfi1fseqlem5  25627  dvmptre  25880  dvsincos  25892  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem8  26260  coscn  26362  sinhalfpilem  26379  cospi  26388  ef2pi  26393  ef2kpi  26394  efper  26395  sinperlem  26396  sin2kpi  26399  cos2kpi  26400  sin2pim  26401  cos2pim  26402  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sinq12gt0  26423  sincosq1eq  26428  sincos4thpi  26429  sincos6thpi  26432  sincos3rdpi  26433  pige3ALT  26436  abssinper  26437  coskpi  26439  sineq0  26440  coseq1  26441  efeq1  26444  efif1olem4  26461  eflogeq  26518  tanarg  26535  cxpsqrtlem  26618  cxpsqrt  26619  logsqrt  26620  2irrexpq  26647  root1eq1  26672  cxpeq  26674  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  ang180lem2  26727  ang180lem3  26728  quad2  26756  1cubrlem  26758  1cubr  26759  dcubic2  26761  dcubic1  26762  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  quartlem3  26776  quart  26778  sinasin  26806  asinsin  26809  atancj  26827  efiatan  26829  efiatan2  26834  2efiatan  26835  tanatan  26836  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl2  26855  leibpilem2  26858  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  log2ublem3  26865  log2ub  26866  birthday  26871  zetacvg  26932  basellem1  26998  basellem3  27000  basellem8  27005  basellem9  27006  cht3  27090  1sgm2ppw  27118  ppiub  27122  chtublem  27129  chtub  27130  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  bcmax  27196  bcp1ctr  27197  bclbnd  27198  bpos1lem  27200  bpos1  27201  bposlem1  27202  bposlem2  27203  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem2  27244  gausslemma2dlem6  27290  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem2  27303  m1lgs  27306  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgsoddprmlem2  27327  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  addsqnreup  27361  addsq2nreurex  27362  rplogsumlem1  27402  dchrisum0fno1  27429  dchrisum0lem1  27434  dchrisum0lem2  27436  logdivsum  27451  mulog2sumlem3  27454  log2sumbnd  27462  selberglem1  27463  selberglem2  27464  selberg2  27469  selberg4lem1  27478  selberg3r  27487  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2  27509  pntlemk  27524  ax5seglem7  28869  axlowdimlem13  28888  elwspths2spth  29904  clwlkclwwlklem2a4  29933  clwwlknonex2  30045  2clwwlk2  30284  numclwlk1lem1  30305  ex-fl  30383  ex-ceil  30384  ex-exp  30386  ex-fac  30387  ex-abs  30391  ex-ind-dvds  30397  ipidsq  30646  cncph  30755  ip0i  30761  ip1ilem  30762  ipdirilem  30765  minvecolem2  30811  hvsubcan2i  31000  norm-ii-i  31073  norm3lem  31085  normpar2i  31092  polid2i  31093  hhph  31114  mayete3i  31664  nmcexi  31962  opsqrlem6  32081  addltmulALT  32382  ply1dg3rt0irred  33558  fldext2chn  33725  constrelextdg2  33744  2sqr3minply  33777  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  omssubadd  34298  oddpwdc  34352  fib5  34403  ballotlem2  34487  ballotth  34536  efmul2picn  34594  itgexpif  34604  vtscl  34636  circlemeth  34638  hgt750lemd  34646  logdivsqrle  34648  hgt750lem  34649  hgt750lem2  34650  problem4  35662  problem5  35663  quad3  35664  cnndvlem1  36532  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem29  37650  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  itg2addnclem3  37674  dvasin  37705  areacirc  37714  heiborlem6  37817  12gcd5e1  41998  12lcm5e60  42003  60lcm7e420  42005  420lcm8e840  42006  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1p1p5  42070  aks4d1p1  42071  posbezout  42095  facp2  42138  1p3e4  42254  sqn5i  42280  235t711  42300  ex-decpmul  42301  cxp112d  42336  cxp111d  42337  cxpi11d  42338  tanhalfpim  42344  fltne  42639  flt4lem5e  42651  sum9cubes  42667  3cubeslem3l  42681  3cubeslem3r  42682  rmxluc  42932  rmyluc  42933  jm2.17a  42956  jm2.18  42984  jm2.23  42992  jm3.1lem1  43013  proot1ex  43192  areaquad  43212  sqrtcval  43637  resqrtvalex  43641  lhe4.4ex1a  44325  sineq0ALT  44933  coskpi2  45871  cosnegpi  45872  cosknegpi  45874  stoweidlem26  46031  wallispilem4  46073  wallispi  46075  wallispi2lem1  46076  stirlinglem8  46086  dirkerper  46101  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkeritg  46107  dirkercncflem1  46108  dirkercncflem2  46109  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem76  46187  fourierdlem103  46214  fourierdlem104  46215  sqwvfourb  46234  fourierswlem  46235  rehalfge1  47340  ceil5half3  47345  modm2nep1  47371  modm1nep2  47373  modm1nem2  47374  fmtnoge3  47535  fmtnorec1  47542  fmtno0  47545  fmtno1  47546  fmtnorec3  47553  fmtnorec4  47554  fmtno5lem2  47559  fmtno5lem4  47561  257prm  47566  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  fmtno5faclem2  47585  fmtno5faclem3  47586  fmtno5fac  47587  139prmALT  47601  31prm  47602  127prm  47604  mod42tp1mod8  47607  lighneallem2  47611  lighneallem3  47612  lighneallem4a  47613  3exp4mod41  47621  41prothprmlem1  47622  41prothprmlem2  47623  41prothprm  47624  bits0ALTV  47684  0evenALTV  47693  6even  47716  8even  47718  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  2exp340mod341  47738  8exp8mod9  47741  mogoldbb  47790  nnsum3primes4  47793  bgoldbtbndlem1  47810  gpg5order  48055  0nodd  48162  0even  48229  2even  48231  2zrngamgm  48237  2t6m3t4e0  48340  linevalexample  48388  zlmodzxzequap  48492  pw2m1lepw2m1  48513  nnlog2ge0lt1  48559  logbpw2m1  48560  nnpw2blen  48573  nnpw2pmod  48576  blen1  48577  blen2  48578  blennnt2  48582  nnolog2flm1  48583  0dig2nn0e  48605  0dig2nn0o  48606  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  nn0sumshdiglem2  48615  ackval1012  48683  ackval2012  48684  ackval3012  48685  ackval42  48689  sinhpcosh  49733