Theorem 2cn 12247

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  1c1 11030   + caddc 11032  2c2 12227

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 11087  ax-addcl 11089

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

This theorem is referenced by:  2ex  12249  2cnd  12250  3cn  12253  2m1e1  12293  3m1e2  12295  2p2e4  12302  times2  12304  2div2e1  12308  1p2e3ALT  12311  3p3e6  12319  4p3e7  12321  5p3e8  12324  6p3e9  12327  2t1e2  12330  2t2e4  12331  3t3e9  12334  2t0e0  12336  4div2e2  12337  2cnne0  12377  halfcn  12382  2halves  12386  8th4div3  12388  halfthird  12389  halfpm6th  12390  2mulicn  12392  2muline0  12393  halfcl  12394  half0  12396  halfaddsub  12401  div4p1lem1div2  12423  3halfnz  12599  zneo  12603  nneo  12604  zeo  12606  7p3e10  12710  4t4e16  12734  6t3e18  12740  7t7e49  12749  8t5e40  12753  9t9e81  12764  decbin0  12775  decbin2  12776  fztpval  13531  fz0tp  13573  fzo0to3tp  13698  fzo1to4tp  13700  expubnd  14131  sq2  14150  sq4e2t8  14152  cu2  14153  subsq2  14164  binom2sub  14173  binom3  14177  zesq  14179  fac2  14232  fac3  14233  faclbnd2  14244  faclbnd4lem1  14246  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd5  14251  bcn2  14272  4bc2eq6  14282  swrd2lsw  14905  crre  15067  addcj  15101  imval2  15104  01sqrexlem7  15201  absmax  15283  rddif  15294  sqreulem  15313  amgm2  15323  abs3lemi  15364  iseraltlem2  15636  ackbijnn  15784  climcndslem1  15805  climcndslem2  15806  arisum  15816  arisum2  15817  geo2sum2  15830  geo2lim  15831  geoihalfsum  15838  bpoly2  16013  bpoly3  16014  bpoly4  16015  fsumcube  16016  efcllem  16033  ege2le3  16046  efgt0  16061  tanval2  16091  tanval3  16092  efi4p  16095  efival  16110  sinadd  16122  cosadd  16123  sinmul  16130  cos2tsin  16137  ef01bndlem  16142  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  cos01gt0  16149  sin02gt0  16150  sin4lt0  16153  odd2np1lem  16300  odd2np1  16301  opoe  16323  omoe  16324  opeo  16325  omeo  16326  nno  16342  nn0o  16343  flodddiv4  16375  bits0  16388  bitsfzolem  16394  0bits  16399  bitsinv1  16402  sadcadd  16418  smumullem  16452  6gcd4e2  16498  3lcm2e6woprm  16575  6lcm4e12  16576  pythagtriplem1  16778  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem15  16791  pythagtriplem16  16792  pythagtriplem17  16793  iserodd  16797  prmreclem5  16882  prmreclem6  16883  4sqlem11  16917  4sqlem12  16918  prmo2  17002  prmo3  17003  dec5dvds  17026  dec2nprm  17029  2exp5  17047  2exp6  17048  2exp7  17049  2exp8  17050  2exp11  17051  2exp16  17052  7prm  17072  11prm  17076  13prm  17077  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  psgnunilem2  19461  efgtlen  19692  efgredleme  19709  frgpnabllem1  19839  lt6abl  19861  htpycc  24957  pcoval2  24993  pcocn  24994  pcohtpylem  24996  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  csbren  25376  minveclem2  25403  ovolunlem1a  25473  ovolunlem1  25474  vitalilem4  25588  mbfi1fseqlem5  25696  dvmptre  25946  dvsincos  25958  aaliou3lem2  26320  aaliou3lem3  26321  aaliou3lem8  26322  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  26732  cxpeq  26734  2logb9irrALT  26775  sqrt2cxp2logb9e3  26776  ang180lem2  26787  ang180lem3  26788  quad2  26816  1cubrlem  26818  1cubr  26819  dcubic2  26821  dcubic1  26822  dcubic  26823  mcubic  26824  cubic2  26825  cubic  26826  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  quartlem3  26836  quart  26838  sinasin  26866  asinsin  26869  atancj  26887  efiatan  26889  efiatan2  26894  2efiatan  26895  tanatan  26896  atantan  26900  atanbndlem  26902  atans2  26908  dvatan  26912  atantayl2  26915  leibpilem2  26918  log2cnv  26921  log2tlbnd  26922  log2ublem2  26924  log2ublem3  26925  log2ub  26926  birthday  26931  zetacvg  26992  basellem1  27058  basellem3  27060  basellem8  27065  basellem9  27066  cht3  27150  1sgm2ppw  27177  ppiub  27181  chtublem  27188  chtub  27189  perfect1  27205  perfectlem1  27206  perfectlem2  27207  perfect  27208  bcmax  27255  bcp1ctr  27256  bclbnd  27257  bpos1lem  27259  bpos1  27260  bposlem1  27261  bposlem2  27262  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem8  27268  bposlem9  27269  lgsdir2lem2  27303  gausslemma2dlem6  27349  lgsquadlem1  27357  lgsquadlem2  27358  lgsquad2lem2  27362  m1lgs  27365  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgsoddprmlem2  27386  2lgsoddprmlem3c  27389  2lgsoddprmlem3d  27390  addsqnreup  27420  addsq2nreurex  27421  rplogsumlem1  27461  dchrisum0fno1  27488  dchrisum0lem1  27493  dchrisum0lem2  27495  logdivsum  27510  mulog2sumlem3  27513  log2sumbnd  27521  selberglem1  27522  selberglem2  27523  selberg2  27528  selberg4lem1  27537  selberg3r  27546  pntpbnd1a  27562  pntpbnd2  27564  pntibndlem2  27568  pntlemk  27583  ax5seglem7  29018  axlowdimlem13  29037  elwspths2spth  30053  clwlkclwwlklem2a4  30082  clwwlknonex2  30194  2clwwlk2  30433  numclwlk1lem1  30454  ex-fl  30532  ex-ceil  30533  ex-exp  30535  ex-fac  30536  ex-abs  30540  ex-ind-dvds  30546  ipidsq  30796  cncph  30905  ip0i  30911  ip1ilem  30912  ipdirilem  30915  minvecolem2  30961  hvsubcan2i  31150  norm-ii-i  31223  norm3lem  31235  normpar2i  31242  polid2i  31243  hhph  31264  mayete3i  31814  nmcexi  32112  opsqrlem6  32231  addltmulALT  32532  ply1dg3rt0irred  33659  fldext2chn  33888  constrelextdg2  33907  2sqr3minply  33940  cos9thpiminplylem4  33945  cos9thpiminplylem5  33946  omssubadd  34460  oddpwdc  34514  fib5  34565  ballotlem2  34649  ballotth  34698  efmul2picn  34756  itgexpif  34766  vtscl  34798  circlemeth  34800  hgt750lemd  34808  logdivsqrle  34810  hgt750lem  34811  hgt750lem2  34812  problem4  35866  problem5  35867  quad3  35868  cnndvlem1  36813  sin2h  37945  cos2h  37946  tan2h  37947  poimirlem29  37984  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  itg2addnclem3  38008  dvasin  38039  areacirc  38048  heiborlem6  38151  12gcd5e1  42456  12lcm5e60  42461  60lcm7e420  42463  420lcm8e840  42464  3exp7  42506  3lexlogpow5ineq1  42507  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1p1p5  42528  aks4d1p1  42529  posbezout  42553  facp2  42596  1p3e4  42711  sqn5i  42731  235t711  42751  ex-decpmul  42752  cxp112d  42787  cxp111d  42788  cxpi11d  42789  tanhalfpim  42795  fltne  43091  flt4lem5e  43103  sum9cubes  43119  3cubeslem3l  43132  3cubeslem3r  43133  rmxluc  43382  rmyluc  43383  jm2.17a  43406  jm2.18  43434  jm2.23  43442  jm3.1lem1  43463  proot1ex  43642  areaquad  43662  sqrtcval  44086  resqrtvalex  44090  lhe4.4ex1a  44774  sineq0ALT  45381  coskpi2  46312  cosnegpi  46313  cosknegpi  46315  stoweidlem26  46472  wallispilem4  46514  wallispi  46516  wallispi2lem1  46517  stirlinglem8  46527  dirkerper  46542  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem76  46628  fourierdlem103  46655  fourierdlem104  46656  sqwvfourb  46675  fourierswlem  46676  nthrucw  47332  sin5tlem1  47337  sin5tlem5  47341  goldrasin  47344  rehalfge1  47799  ceil5half3  47806  modm2nep1  47832  modm1nep2  47834  modm1nem2  47835  fmtnoge3  48005  fmtnorec1  48012  fmtno0  48015  fmtno1  48016  fmtnorec3  48023  fmtnorec4  48024  fmtno5lem2  48029  fmtno5lem4  48031  257prm  48036  fmtnoprmfac2lem1  48041  fmtno4prmfac  48047  fmtno5faclem2  48055  fmtno5faclem3  48056  fmtno5fac  48057  139prmALT  48071  31prm  48072  127prm  48074  mod42tp1mod8  48077  lighneallem2  48081  lighneallem3  48082  lighneallem4a  48083  3exp4mod41  48091  41prothprmlem1  48092  41prothprmlem2  48093  41prothprm  48094  bits0ALTV  48167  0evenALTV  48176  6even  48199  8even  48201  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  2exp340mod341  48221  8exp8mod9  48224  mogoldbb  48273  nnsum3primes4  48276  bgoldbtbndlem1  48293  gpg5order  48548  gpg5edgnedg  48618  0nodd  48658  0even  48725  2even  48727  2zrngamgm  48733  2t6m3t4e0  48836  linevalexample  48883  zlmodzxzequap  48987  pw2m1lepw2m1  49008  nnlog2ge0lt1  49054  logbpw2m1  49055  nnpw2blen  49068  nnpw2pmod  49071  blen1  49072  blen2  49073  blennnt2  49077  nnolog2flm1  49078  0dig2nn0e  49100  0dig2nn0o  49101  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109  nn0sumshdiglem2  49110  ackval1012  49178  ackval2012  49179  ackval3012  49180  ackval42  49184  sinhpcosh  50227