Theorem 2cn 12368

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356

This theorem is referenced by:  2ex  12370  2cnd  12371  3cn  12374  2m1e1  12419  3m1e2  12421  2p2e4  12428  times2  12430  2div2e1  12434  1p2e3ALT  12437  3p3e6  12445  4p3e7  12447  5p3e8  12450  6p3e9  12453  2t1e2  12456  2t2e4  12457  3t3e9  12460  2t0e0  12462  4d2e2  12463  2cnne0  12503  halfcn  12508  1mhlfehlf  12512  8th4div3  12513  halfpm6th  12514  2mulicn  12516  2muline0  12517  halfcl  12518  half0  12520  2halves  12521  halfaddsub  12526  div4p1lem1div2  12548  3halfnz  12722  zneo  12726  nneo  12727  zeo  12729  7p3e10  12833  4t4e16  12857  6t3e18  12863  7t7e49  12872  8t5e40  12876  9t9e81  12887  decbin0  12898  decbin2  12899  halfthird  12901  fztpval  13646  fz0tp  13685  fzo0to3tp  13802  fzo1to4tp  13804  expubnd  14227  sq2  14246  sq4e2t8  14248  cu2  14249  subsq2  14260  binom2sub  14269  binom3  14273  zesq  14275  fac2  14328  fac3  14329  faclbnd2  14340  faclbnd4lem1  14342  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd5  14347  bcn2  14368  4bc2eq6  14378  swrd2lsw  15001  crre  15163  addcj  15197  imval2  15200  01sqrexlem7  15297  absmax  15378  rddif  15389  sqreulem  15408  amgm2  15418  abs3lemi  15459  iseraltlem2  15731  ackbijnn  15876  climcndslem1  15897  climcndslem2  15898  arisum  15908  arisum2  15909  geo2sum2  15922  geo2lim  15923  geoihalfsum  15930  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  efcllem  16125  ege2le3  16138  efgt0  16151  tanval2  16181  tanval3  16182  efi4p  16185  efival  16200  sinadd  16212  cosadd  16213  sinmul  16220  cos2tsin  16227  ef01bndlem  16232  cos01bnd  16234  cos1bnd  16235  cos2bnd  16236  cos01gt0  16239  sin02gt0  16240  sin4lt0  16243  odd2np1lem  16388  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  nno  16430  nn0o  16431  flodddiv4  16461  bits0  16474  bitsfzolem  16480  0bits  16485  bitsinv1  16488  sadcadd  16504  smumullem  16538  6gcd4e2  16585  3lcm2e6woprm  16662  6lcm4e12  16663  pythagtriplem1  16863  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem15  16876  pythagtriplem16  16877  pythagtriplem17  16878  iserodd  16882  prmreclem5  16967  prmreclem6  16968  4sqlem11  17002  4sqlem12  17003  prmo2  17087  prmo3  17088  dec5dvds  17111  dec2nprm  17114  decexp2  17122  2exp5  17133  2exp6  17134  2exp7  17135  2exp8  17136  2exp11  17137  2exp16  17138  7prm  17158  11prm  17162  13prm  17163  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  psgnunilem2  19537  efgtlen  19768  efgredleme  19785  frgpnabllem1  19915  lt6abl  19937  htpycc  25031  pcoval2  25068  pcocn  25069  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  csbren  25452  minveclem2  25479  ovolunlem1a  25550  ovolunlem1  25551  vitalilem4  25665  mbfi1fseqlem5  25774  dvmptre  26027  dvsincos  26039  aaliou3lem2  26403  aaliou3lem3  26404  aaliou3lem8  26405  coscn  26507  sinhalfpilem  26523  cospi  26532  ef2pi  26537  ef2kpi  26538  efper  26539  sinperlem  26540  sin2kpi  26543  cos2kpi  26544  sin2pim  26545  cos2pim  26546  sincosq3sgn  26560  sincosq4sgn  26561  tangtx  26565  sinq12gt0  26567  sincosq1eq  26572  sincos4thpi  26573  sincos6thpi  26576  sincos3rdpi  26577  pige3ALT  26580  abssinper  26581  coskpi  26583  sineq0  26584  coseq1  26585  efeq1  26588  efif1olem4  26605  eflogeq  26662  tanarg  26679  cxpsqrtlem  26762  cxpsqrt  26763  logsqrt  26764  2irrexpq  26791  root1eq1  26816  cxpeq  26818  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  ang180lem2  26871  ang180lem3  26872  quad2  26900  1cubrlem  26902  1cubr  26903  dcubic2  26905  dcubic1  26906  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  quartlem3  26920  quart  26922  sinasin  26950  asinsin  26953  atancj  26971  efiatan  26973  efiatan2  26978  2efiatan  26979  tanatan  26980  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl2  26999  leibpilem2  27002  log2cnv  27005  log2tlbnd  27006  log2ublem2  27008  log2ublem3  27009  log2ub  27010  birthday  27015  zetacvg  27076  basellem1  27142  basellem3  27144  basellem8  27149  basellem9  27150  cht3  27234  1sgm2ppw  27262  ppiub  27266  chtublem  27273  chtub  27274  perfect1  27290  perfectlem1  27291  perfectlem2  27292  perfect  27293  bcmax  27340  bcp1ctr  27341  bclbnd  27342  bpos1lem  27344  bpos1  27345  bposlem1  27346  bposlem2  27347  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsdir2lem2  27388  gausslemma2dlem6  27434  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem2  27447  m1lgs  27450  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgsoddprmlem2  27471  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  addsqnreup  27505  addsq2nreurex  27506  rplogsumlem1  27546  dchrisum0fno1  27573  dchrisum0lem1  27578  dchrisum0lem2  27580  logdivsum  27595  mulog2sumlem3  27598  log2sumbnd  27606  selberglem1  27607  selberglem2  27608  selberg2  27613  selberg4lem1  27622  selberg3r  27631  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2  27653  pntlemk  27668  ax5seglem7  28968  axlowdimlem13  28987  elwspths2spth  30000  clwlkclwwlklem2a4  30029  clwwlknonex2  30141  2clwwlk2  30380  numclwlk1lem1  30401  ex-fl  30479  ex-ceil  30480  ex-exp  30482  ex-fac  30483  ex-abs  30487  ex-ind-dvds  30493  ipidsq  30742  cncph  30851  ip0i  30857  ip1ilem  30858  ipdirilem  30861  minvecolem2  30907  hvsubcan2i  31096  norm-ii-i  31169  norm3lem  31181  normpar2i  31188  polid2i  31189  hhph  31210  mayete3i  31760  nmcexi  32058  opsqrlem6  32177  addltmulALT  32478  ply1dg3rt0irred  33572  fldext2chn  33719  constrelextdg2  33737  2sqr3minply  33738  omssubadd  34265  oddpwdc  34319  fib5  34370  ballotlem2  34453  ballotth  34502  efmul2picn  34573  itgexpif  34583  vtscl  34615  circlemeth  34617  hgt750lemd  34625  logdivsqrle  34627  hgt750lem  34628  hgt750lem2  34629  problem4  35636  problem5  35637  quad3  35638  cnndvlem1  36503  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem29  37609  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  itg2addnclem3  37633  dvasin  37664  areacirc  37673  heiborlem6  37776  12gcd5e1  41960  12lcm5e60  41965  60lcm7e420  41967  420lcm8e840  41968  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1p1p5  42032  aks4d1p1  42033  posbezout  42057  facp2  42100  fac2xp3  42196  2xp3dxp2ge1d  42198  sqn5i  42274  235t711  42293  ex-decpmul  42294  cxp112d  42329  cxp111d  42330  cxpi11d  42331  tanhalfpim  42337  fltne  42599  flt4lem5e  42611  sum9cubes  42627  3cubeslem3l  42642  3cubeslem3r  42643  rmxluc  42893  rmyluc  42894  jm2.17a  42917  jm2.18  42945  jm2.23  42953  jm3.1lem1  42974  proot1ex  43157  areaquad  43177  sqrtcval  43603  resqrtvalex  43607  lhe4.4ex1a  44298  sineq0ALT  44908  coskpi2  45787  cosnegpi  45788  cosknegpi  45790  stoweidlem26  45947  wallispilem4  45989  wallispi  45991  wallispi2lem1  45992  stirlinglem8  46002  dirkerper  46017  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem2  46025  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem76  46103  fourierdlem103  46130  fourierdlem104  46131  sqwvfourb  46150  fourierswlem  46151  fmtnoge3  47404  fmtnorec1  47411  fmtno0  47414  fmtno1  47415  fmtnorec3  47422  fmtnorec4  47423  fmtno5lem2  47428  fmtno5lem4  47430  257prm  47435  fmtnoprmfac2lem1  47440  fmtno4prmfac  47446  fmtno5faclem2  47454  fmtno5faclem3  47455  fmtno5fac  47456  139prmALT  47470  31prm  47471  127prm  47473  mod42tp1mod8  47476  lighneallem2  47480  lighneallem3  47481  lighneallem4a  47482  3exp4mod41  47490  41prothprmlem1  47491  41prothprmlem2  47492  41prothprm  47493  bits0ALTV  47553  0evenALTV  47562  6even  47585  8even  47587  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  2exp340mod341  47607  8exp8mod9  47610  mogoldbb  47659  nnsum3primes4  47662  bgoldbtbndlem1  47679  0nodd  47893  0even  47960  2even  47962  2zrngamgm  47968  2t6m3t4e0  48073  linevalexample  48124  zlmodzxzequap  48228  pw2m1lepw2m1  48249  nnlog2ge0lt1  48300  logbpw2m1  48301  nnpw2blen  48314  nnpw2pmod  48317  blen1  48318  blen2  48319  blennnt2  48323  nnolog2flm1  48324  0dig2nn0e  48346  0dig2nn0o  48347  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  nn0sumshdiglem2  48356  ackval1012  48424  ackval2012  48425  ackval3012  48426  ackval42  48430  sinhpcosh  48832