Theorem 2cn 12344

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 12331	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11186	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11243	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2858	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   + caddc 11131  2c2 12323

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 2734  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-2 12331

This theorem is used by:  2ex  12346  2cnd  12347  3cn  12350  2thalfe1  12376  2m1e1OLD  12394  3m1e2  12396  2p2e4  12403  times2  12405  2div2e1  12409  1p2e3ALT  12412  3p3e6  12420  4p3e7  12422  5p3e8  12425  6p3e9  12428  2t1e2  12431  2t2e4  12432  2t3e6  12435  3t3e9  12436  2t4e8  12438  2t0e0  12439  4div2e2  12440  2cnne0  12481  halfcn  12486  2halves  12490  8th4div3  12492  halfthird  12493  halfpm6th  12494  2mulicn  12496  2muline0  12497  halfcl  12498  half0  12500  halfaddsub  12505  div4p1lem1div2  12527  3halfnz  12704  zneo  12708  nneo  12709  zeo  12711  7p3e10  12820  4t4e16  12844  6t3e18  12850  7t7e49  12859  8t5e40  12863  9t9e81  12874  decbin0  12887  decbin2  12888  fztpval  13645  fz0tp  13687  fzo0to3tp  13812  fzo1to4tp  13814  expubnd  14246  sq2  14265  sq4e2t8  14267  cu2  14268  subsq2  14279  binom2sub  14288  binom3  14292  zesq  14294  fac2  14347  faclbnd2  14359  faclbnd4lem1  14361  faclbnd4lem3  14363  faclbnd4lem4  14364  faclbnd5  14366  bcn2  14387  4bc2eq6  14397  swrd2lsw  15029  crre  15205  addcj  15239  imval2  15242  01sqrexlem7  15339  absmax  15421  sqreulem  15451  amgm2  15461  abs3lemi  15502  iseraltlem2  15774  ackbijnn  15921  climcndslem1  15942  climcndslem2  15943  arisum  15953  arisum2  15954  geo2sum2  15967  geo2lim  15968  geoihalfsum  15975  bpoly2  16149  bpoly3  16150  bpoly4  16151  fsumcube  16152  efcllem  16169  ege2le3  16182  efgt0  16197  tanval2  16227  tanval3  16228  efi4p  16231  efival  16246  sinadd  16258  cosadd  16259  sinmul  16266  cos2tsin  16273  ef01bndlem  16278  cos01bnd  16280  cos1bnd  16281  cos2bnd  16282  cos01gt0  16285  sin02gt0  16286  sin4lt0  16289  odd2np1lem  16436  odd2np1  16437  opoe  16459  omoe  16460  opeo  16461  omeo  16462  nno  16478  nn0o  16479  flodddiv4  16511  bits0  16524  bitsfzolem  16530  0bits  16535  bitsinv1  16538  sadcadd  16554  smumullem  16588  6gcd4e2  16634  3lcm2e6woprm  16711  6lcm4e12  16712  pythagtriplem1  16914  pythagtriplem12  16924  pythagtriplem14  16926  pythagtriplem15  16927  pythagtriplem16  16928  pythagtriplem17  16929  iserodd  16933  prmreclem5  17018  prmreclem6  17019  4sqlem11  17053  4sqlem12  17054  prmo2  17138  dec5dvds  17162  dec2nprm  17165  2exp5  17183  2exp7  17185  2exp11  17187  2exp16  17188  10nprm  17211  11prm  17213  13prm  17214  37prm  17219  43prm  17220  83prm  17221  139prm  17222  163prm  17223  317prm  17224  631prm  17225  1259lem1  17229  1259lem2  17230  1259lem3  17231  1259lem4  17232  1259lem5  17233  1259prm  17234  2503lem1  17235  2503lem2  17236  2503lem3  17237  4001lem1  17239  4001lem2  17240  4001lem3  17241  4001lem4  17242  4001prm  17243  psgnunilem2  19628  efgtlen  19859  efgredleme  19876  frgpnabllem1  20006  lt6abl  20028  pcoass  25258  pcorevlem  25260  csbren  25633  minveclem2  25660  ovolunlem1a  25730  ovolunlem1  25731  vitalilem4  25845  mbfi1fseqlem5  25953  dvmptre  26203  dvsincos  26215  aaliou3lem2  26586  aaliou3lem3  26587  aaliou3lem8  26588  coscn  26688  2picn  26702  sinhalfpilem  26708  cospi  26717  ef2pi  26722  ef2kpi  26723  efper  26724  sinperlem  26725  sin2kpi  26728  cos2kpi  26729  sin2pim  26730  cos2pim  26731  sincosq3sgn  26745  sincosq4sgn  26746  tangtx  26750  sinq12gt0  26752  sincosq1eq  26757  sincos4thpi  26758  sincos6thpi  26761  sincos3rdpi  26762  pige3ALT  26765  abssinper  26766  coskpi  26768  sineq0  26769  coseq1  26770  efeq1  26773  efif1olem4  26790  eflogeq  26847  tanarg  26864  cxpsqrtlem  26947  cxpsqrt  26948  logsqrt  26949  2irrexpq  26976  root1eq1  27000  cxpeq  27002  2logb9irrALT  27043  sqrt2cxp2logb9e3  27044  ang180lem2  27055  ang180lem3  27056  quad2  27084  1cubrlem  27086  1cubr  27087  dcubic2  27089  dcubic1  27090  dcubic  27091  mcubic  27092  cubic2  27093  cubic  27094  dquartlem1  27096  dquartlem2  27097  dquart  27098  quart1lem  27100  quart1  27101  quartlem1  27102  quartlem2  27103  quartlem3  27104  quart  27106  sinasin  27134  asinsin  27137  atancj  27155  efiatan  27157  efiatan2  27162  2efiatan  27163  tanatan  27164  atantan  27168  atanbndlem  27170  atans2  27176  dvatan  27180  atantayl2  27183  leibpilem2  27186  log2cnv  27189  log2tlbnd  27190  log2ublem2  27192  log2ublem3  27193  log2ub  27194  birthday  27199  zetacvg  27259  basellem1  27325  basellem3  27327  basellem8  27332  basellem9  27333  1sgm2ppw  27444  ppiub  27448  chtublem  27455  chtub  27456  perfect1  27472  perfectlem1  27473  perfectlem2  27474  perfect  27475  bcmax  27522  bcp1ctr  27523  bclbnd  27524  bpos1lem  27526  bpos1  27527  bposlem1  27528  bposlem2  27529  bposlem4  27531  bposlem5  27532  bposlem6  27533  bposlem8  27535  bposlem9  27536  lgsdir2lem2  27570  gausslemma2dlem6  27616  lgsquadlem1  27624  lgsquadlem2  27625  lgsquad2lem2  27629  m1lgs  27632  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2lgsoddprmlem2  27653  2lgsoddprmlem3c  27656  2lgsoddprmlem3d  27657  addsqnreup  27687  addsq2nreurex  27688  rplogsumlem1  27728  dchrisum0fno1  27755  dchrisum0lem1  27760  dchrisum0lem2  27762  logdivsum  27777  mulog2sumlem3  27780  log2sumbnd  27788  selberglem1  27789  selberglem2  27790  selberg2  27795  selberg4lem1  27804  selberg3r  27813  pntpbnd1a  27829  pntpbnd2  27831  pntibndlem2  27835  pntlemk  27850  ax5seglem7  29400  axlowdimlem13  29419  elwspths2spth  30446  clwlkclwwlklem2a4  30475  clwwlknonex2  30587  2clwwlk2  30836  numclwlk1lem1  30857  ex-fl  30935  ex-ceil  30936  ex-exp  30938  ex-fac  30939  ex-abs  30943  ex-ind-dvds  30949  ipidsq  31199  cncph  31308  ip0i  31314  ip1ilem  31315  ipdirilem  31318  minvecolem2  31364  hvsubcan2i  31553  norm-ii-i  31626  norm3lem  31638  normpar2i  31645  polid2i  31646  hhph  31667  mayete3i  32217  nmcexi  32515  opsqrlem6  32634  addltmulALT  32935  ply1dg3rt0irred  34002  fldext2chn  34246  constrelextdg2  34265  2sqr3minply  34298  cos9thpiminplylem4  34303  cos9thpiminplylem5  34304  omssubadd  34819  oddpwdc  34873  fib5  34924  ballotlem2  35008  ballotth  35057  efmul2picn  35112  itgexpif  35122  vtscl  35154  circlemeth  35156  hgt750lemd  35164  logdivsqrle  35166  hgt750lem  35167  hgt750lem2  35168  problem4  36255  problem5  36256  quad3  36257  cnndvlem1  37242  sin2h  38372  cos2h  38373  tan2h  38374  poimirlem29  38406  mblfinlem1  38414  mblfinlem2  38415  mblfinlem3  38416  itg2addnclem3  38430  dvasin  38461  areacirc  38470  heiborlem6  38574  12gcd5e1  42877  12lcm5e60  42882  60lcm7e420  42884  3exp7  42927  3lexlogpow5ineq1  42928  3lexlogpow5ineq5  42934  aks4d1p1p5  42949  aks4d1p1  42950  posbezout  42974  facp2  43017  25or6to4  43080  4p4e8ALT  43133  1p3e4  43134  2p3e5  43140  2p4e6  43141  2p5e7  43142  2p6e8  43143  2p7e9  43144  3p4e7  43145  3p5e8  43146  sqn5i  43168  235t711  43188  ex-decpmul  43189  cxp112d  43224  cxp111d  43225  cxpi11d  43226  tanhalfpim  43232  fltne  43498  flt4lem5e  43510  sum9cubes  43526  3cubeslem3r  43540  rmxluc  43785  rmyluc  43786  jm2.17a  43809  jm2.18  43837  jm2.23  43845  jm3.1lem1  43866  proot1ex  44045  areaquad  44065  sqrtcval  44489  resqrtvalex  44493  lhe4.4ex1a  45161  sineq0ALT  45767  coskpi2  46702  cosnegpi  46703  cosknegpi  46705  stoweidlem26  46862  wallispilem4  46904  wallispi  46906  wallispi2lem1  46907  stirlinglem8  46917  dirkerper  46932  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkeritg  46938  dirkercncflem1  46939  fourierdlem57  46999  fourierdlem58  47000  fourierdlem62  47004  fourierdlem76  47018  fourierdlem103  47045  fourierdlem104  47046  sqwvfourb  47065  fourierswlem  47066  sin5tlem1  47745  sin5tlem5  47749  cos5t  47751  goldpolyfactor  47753  goldrasin  47755  goldracos5teq  47758  goldratmolem2  47759  goldratmolem3  47760  goldratmolem4  47761  rehalfge1  48235  ceil5half3  48242  modm2nep1  48268  modm1nep2  48270  modm1nem2  48271  fmtnoge3  48441  fmtnorec1  48448  fmtno0  48451  fmtno1  48452  fmtnorec3  48459  fmtnorec4  48460  fmtno5lem2  48465  fmtno5lem4  48467  257prm  48472  fmtnoprmfac2lem1  48477  fmtno4prmfac  48483  fmtno5faclem2  48491  fmtno5faclem3  48492  fmtno5fac  48493  139prmALT  48507  31prm  48508  127prm  48510  lighneallem2  48517  lighneallem3  48518  lighneallem4a  48519  3exp4mod41  48527  41prothprmlem1  48528  41prothprmlem2  48529  41prothprm  48530  bits0ALTV  48603  0evenALTV  48612  6even  48635  8even  48637  perfectALTVlem1  48645  perfectALTVlem2  48646  perfectALTV  48647  2exp340mod341  48657  mogoldbb  48709  nnsum3primes4  48712  bgoldbtbndlem1  48729  gpg5order  48984  gpg5edgnedg  49054  0nodd  49093  0even  49160  2even  49162  2zrngamgm  49168  2t6m3t4e0  49286  linevalexample  49333  zlmodzxzequap  49437  pw2m1lepw2m1  49458  nnlog2ge0lt1  49504  logbpw2m1  49505  nnpw2blen  49518  nnpw2pmod  49521  blen1  49522  blen2  49523  blennnt2  49527  nnolog2flm1  49528  0dig2nn0e  49550  0dig2nn0o  49551  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559  nn0sumshdiglem2  49560  ackval1012  49628  ackval2012  49629  ackval3012  49630  ackval42  49634  sinhpcosh  50674