Theorem 2cn 12294

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 12282	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11174	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11227	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2828	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7412  ℂcc 11114  1c1 11117   + caddc 11119  2c2 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-1cn 11174  ax-addcl 11176

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809  df-2 12282

This theorem is referenced by:  2ex  12296  2cnd  12297  3cn  12300  2m1e1  12345  3m1e2  12347  2p2e4  12354  times2  12356  2div2e1  12360  1p2e3ALT  12363  3p3e6  12371  4p3e7  12373  5p3e8  12376  6p3e9  12379  2t1e2  12382  2t2e4  12383  3t3e9  12386  2t0e0  12388  4d2e2  12389  2cnne0  12429  halfcn  12434  1mhlfehlf  12438  8th4div3  12439  halfpm6th  12440  2mulicn  12442  2muline0  12443  halfcl  12444  half0  12446  2halves  12447  halfaddsub  12452  div4p1lem1div2  12474  3halfnz  12648  zneo  12652  nneo  12653  zeo  12655  7p3e10  12759  4t4e16  12783  6t3e18  12789  7t7e49  12798  8t5e40  12802  9t9e81  12813  decbin0  12824  decbin2  12825  halfthird  12827  fztpval  13570  fz0tp  13609  fz0to4untppr  13611  fzo0to3tp  13725  fzo1to4tp  13727  expubnd  14149  sq2  14168  sq4e2t8  14170  cu2  14171  subsq2  14182  binom2sub  14190  binom3  14194  zesq  14196  fac2  14246  fac3  14247  faclbnd2  14258  faclbnd4lem1  14260  faclbnd4lem3  14262  faclbnd4lem4  14263  faclbnd5  14265  bcn2  14286  4bc2eq6  14296  swrd2lsw  14910  crre  15068  addcj  15102  imval2  15105  01sqrexlem7  15202  absmax  15283  rddif  15294  sqreulem  15313  amgm2  15323  abs3lemi  15364  iseraltlem2  15636  ackbijnn  15781  climcndslem1  15802  climcndslem2  15803  arisum  15813  arisum2  15814  geo2sum2  15827  geo2lim  15828  geoihalfsum  15835  bpoly2  16008  bpoly3  16009  bpoly4  16010  fsumcube  16011  efcllem  16028  ege2le3  16040  efgt0  16053  tanval2  16083  tanval3  16084  efi4p  16087  efival  16102  sinadd  16114  cosadd  16115  sinmul  16122  cos2tsin  16129  ef01bndlem  16134  cos01bnd  16136  cos1bnd  16137  cos2bnd  16138  cos01gt0  16141  sin02gt0  16142  sin4lt0  16145  odd2np1lem  16290  odd2np1  16291  opoe  16313  omoe  16314  opeo  16315  omeo  16316  nno  16332  nn0o  16333  flodddiv4  16363  bits0  16376  bitsfzolem  16382  0bits  16387  bitsinv1  16390  sadcadd  16406  smumullem  16440  6gcd4e2  16487  3lcm2e6woprm  16559  6lcm4e12  16560  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  decexp2  17015  2exp5  17026  2exp6  17027  2exp7  17028  2exp8  17029  2exp11  17030  2exp16  17031  7prm  17051  11prm  17055  13prm  17056  37prm  17061  43prm  17062  83prm  17063  139prm  17064  163prm  17065  317prm  17066  631prm  17067  1259lem1  17071  1259lem2  17072  1259lem3  17073  1259lem4  17074  1259lem5  17075  1259prm  17076  2503lem1  17077  2503lem2  17078  2503lem3  17079  4001lem1  17081  4001lem2  17082  4001lem3  17083  4001lem4  17084  4001prm  17085  psgnunilem2  19408  efgtlen  19639  efgredleme  19656  frgpnabllem1  19786  lt6abl  19808  htpycc  24739  pcoval2  24776  pcocn  24777  pcohtpylem  24779  pcopt  24782  pcopt2  24783  pcoass  24784  pcorevlem  24786  csbren  25160  minveclem2  25187  ovolunlem1a  25258  ovolunlem1  25259  vitalilem4  25373  mbfi1fseqlem5  25482  dvmptre  25734  dvsincos  25746  aaliou3lem2  26106  aaliou3lem3  26107  aaliou3lem8  26108  coscn  26208  sinhalfpilem  26224  cospi  26233  ef2pi  26238  ef2kpi  26239  efper  26240  sinperlem  26241  sin2kpi  26244  cos2kpi  26245  sin2pim  26246  cos2pim  26247  sincosq3sgn  26261  sincosq4sgn  26262  tangtx  26266  sinq12gt0  26268  sincosq1eq  26273  sincos4thpi  26274  sincos6thpi  26276  sincos3rdpi  26277  pige3ALT  26280  abssinper  26281  coskpi  26283  sineq0  26284  coseq1  26285  efeq1  26288  efif1olem4  26305  eflogeq  26361  tanarg  26378  cxpsqrtlem  26461  cxpsqrt  26462  logsqrt  26463  2irrexpq  26490  root1eq1  26514  cxpeq  26516  2logb9irrALT  26554  sqrt2cxp2logb9e3  26555  ang180lem2  26566  ang180lem3  26567  quad2  26595  1cubrlem  26597  1cubr  26598  dcubic2  26600  dcubic1  26601  dcubic  26602  mcubic  26603  cubic2  26604  cubic  26605  dquartlem1  26607  dquartlem2  26608  dquart  26609  quart1lem  26611  quart1  26612  quartlem1  26613  quartlem2  26614  quartlem3  26615  quart  26617  sinasin  26645  asinsin  26648  atancj  26666  efiatan  26668  efiatan2  26673  2efiatan  26674  tanatan  26675  atantan  26679  atanbndlem  26681  atans2  26687  dvatan  26691  atantayl2  26694  leibpilem2  26697  log2cnv  26700  log2tlbnd  26701  log2ublem2  26703  log2ublem3  26704  log2ub  26705  birthday  26710  zetacvg  26770  basellem1  26836  basellem3  26838  basellem8  26843  basellem9  26844  cht3  26928  1sgm2ppw  26954  ppiub  26958  chtublem  26965  chtub  26966  perfect1  26982  perfectlem1  26983  perfectlem2  26984  perfect  26985  bcmax  27032  bcp1ctr  27033  bclbnd  27034  bpos1lem  27036  bpos1  27037  bposlem1  27038  bposlem2  27039  bposlem4  27041  bposlem5  27042  bposlem6  27043  bposlem8  27045  bposlem9  27046  lgsdir2lem2  27080  gausslemma2dlem6  27126  lgsquadlem1  27134  lgsquadlem2  27135  lgsquad2lem2  27139  m1lgs  27142  2lgslem3a  27150  2lgslem3b  27151  2lgslem3c  27152  2lgslem3d  27153  2lgsoddprmlem2  27163  2lgsoddprmlem3c  27166  2lgsoddprmlem3d  27167  addsqnreup  27197  addsq2nreurex  27198  rplogsumlem1  27238  dchrisum0fno1  27265  dchrisum0lem1  27270  dchrisum0lem2  27272  logdivsum  27287  mulog2sumlem3  27290  log2sumbnd  27298  selberglem1  27299  selberglem2  27300  selberg2  27305  selberg4lem1  27314  selberg3r  27323  pntpbnd1a  27339  pntpbnd2  27341  pntibndlem2  27345  pntlemk  27360  ax5seglem7  28475  axlowdimlem13  28494  elwspths2spth  29503  clwlkclwwlklem2a4  29532  clwwlknonex2  29644  2clwwlk2  29883  numclwlk1lem1  29904  ex-fl  29982  ex-ceil  29983  ex-exp  29985  ex-fac  29986  ex-abs  29990  ex-ind-dvds  29996  ipidsq  30245  cncph  30354  ip0i  30360  ip1ilem  30361  ipdirilem  30364  minvecolem2  30410  hvsubcan2i  30599  norm-ii-i  30672  norm3lem  30684  normpar2i  30691  polid2i  30692  hhph  30713  mayete3i  31263  nmcexi  31561  opsqrlem6  31680  addltmulALT  31981  omssubadd  33612  oddpwdc  33666  fib5  33717  ballotlem2  33800  ballotth  33849  efmul2picn  33921  itgexpif  33931  vtscl  33963  circlemeth  33965  hgt750lemd  33973  logdivsqrle  33975  hgt750lem  33976  hgt750lem2  33977  problem4  34966  problem5  34967  quad3  34968  cnndvlem1  35729  sin2h  36794  cos2h  36795  tan2h  36796  poimirlem29  36833  mblfinlem1  36841  mblfinlem2  36842  mblfinlem3  36843  itg2addnclem3  36857  dvasin  36888  areacirc  36897  heiborlem6  37000  12gcd5e1  41187  12lcm5e60  41192  60lcm7e420  41194  420lcm8e840  41195  3exp7  41237  3lexlogpow5ineq1  41238  3lexlogpow2ineq2  41243  3lexlogpow5ineq5  41244  aks4d1p1p5  41259  aks4d1p1  41260  facp2  41278  fac2xp3  41339  2xp3dxp2ge1d  41341  sqn5i  41512  235t711  41520  ex-decpmul  41521  fltne  41701  flt4lem5e  41713  sum9cubes  41729  3cubeslem3l  41739  3cubeslem3r  41740  rmxluc  41990  rmyluc  41991  jm2.17a  42014  jm2.18  42042  jm2.23  42050  jm3.1lem1  42071  proot1ex  42258  areaquad  42280  sqrtcval  42707  resqrtvalex  42711  lhe4.4ex1a  43403  sineq0ALT  44013  coskpi2  44893  cosnegpi  44894  cosknegpi  44896  stoweidlem26  45053  wallispilem4  45095  wallispi  45097  wallispi2lem1  45098  stirlinglem8  45108  dirkerper  45123  dirkertrigeqlem3  45127  dirkertrigeq  45128  dirkeritg  45129  dirkercncflem1  45130  dirkercncflem2  45131  fourierdlem57  45190  fourierdlem58  45191  fourierdlem62  45195  fourierdlem76  45209  fourierdlem103  45236  fourierdlem104  45237  sqwvfourb  45256  fourierswlem  45257  fmtnoge3  46509  fmtnorec1  46516  fmtno0  46519  fmtno1  46520  fmtnorec3  46527  fmtnorec4  46528  fmtno5lem2  46533  fmtno5lem4  46535  257prm  46540  fmtnoprmfac2lem1  46545  fmtno4prmfac  46551  fmtno5faclem2  46559  fmtno5faclem3  46560  fmtno5fac  46561  139prmALT  46575  31prm  46576  127prm  46578  mod42tp1mod8  46581  lighneallem2  46585  lighneallem3  46586  lighneallem4a  46587  3exp4mod41  46595  41prothprmlem1  46596  41prothprmlem2  46597  41prothprm  46598  bits0ALTV  46658  0evenALTV  46667  6even  46690  8even  46692  perfectALTVlem1  46700  perfectALTVlem2  46701  perfectALTV  46702  2exp340mod341  46712  8exp8mod9  46715  mogoldbb  46764  nnsum3primes4  46767  bgoldbtbndlem1  46784  0nodd  46859  0even  46930  2even  46932  2zrngamgm  46938  2t6m3t4e0  47125  linevalexample  47176  zlmodzxzequap  47280  pw2m1lepw2m1  47301  nnlog2ge0lt1  47352  logbpw2m1  47353  nnpw2blen  47366  nnpw2pmod  47369  blen1  47370  blen2  47371  blennnt2  47375  nnolog2flm1  47376  0dig2nn0e  47398  0dig2nn0o  47399  nn0sumshdiglemA  47405  nn0sumshdiglemB  47406  nn0sumshdiglem1  47407  nn0sumshdiglem2  47408  ackval1012  47476  ackval2012  47477  ackval3012  47478  ackval42  47482  sinhpcosh  47885