Theorem 2cn 11953

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 11941	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 10835	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 10887	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2836	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775  1c1 10778   + caddc 10780  2c2 11933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10835  ax-addcl 10837

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-clel 2818  df-2 11941

This theorem is referenced by:  2ex  11955  2cnd  11956  3cn  11959  2m1e1  12004  3m1e2  12006  2p2e4  12013  times2  12015  2div2e1  12019  1p2e3ALT  12022  3p3e6  12030  4p3e7  12032  5p3e8  12035  6p3e9  12038  2t1e2  12041  2t2e4  12042  3t3e9  12045  2t0e0  12047  4d2e2  12048  2cnne0  12088  halfcn  12093  1mhlfehlf  12097  8th4div3  12098  halfpm6th  12099  2mulicn  12101  2muline0  12102  halfcl  12103  half0  12105  2halves  12106  halfaddsub  12111  div4p1lem1div2  12133  3halfnz  12304  zneo  12308  nneo  12309  zeo  12311  7p3e10  12416  4t4e16  12440  6t3e18  12446  7t7e49  12455  8t5e40  12459  9t9e81  12470  decbin0  12481  decbin2  12482  halfthird  12484  fztpval  13222  fz0tp  13261  fz0to4untppr  13263  fzo0to3tp  13376  fzo1to4tp  13378  expubnd  13798  sq2  13817  sq4e2t8  13819  cu2  13820  subsq2  13830  binom2sub  13838  binom3  13842  zesq  13844  fac2  13896  fac3  13897  faclbnd2  13908  faclbnd4lem1  13910  faclbnd4lem3  13912  faclbnd4lem4  13913  faclbnd5  13915  bcn2  13936  4bc2eq6  13946  swrd2lsw  14568  crre  14728  addcj  14762  imval2  14765  sqrlem7  14863  absmax  14944  rddif  14955  sqreulem  14974  amgm2  14984  abs3lemi  15025  iseraltlem2  15297  ackbijnn  15443  climcndslem1  15464  climcndslem2  15465  arisum  15475  arisum2  15476  geo2sum2  15489  geo2lim  15490  geoihalfsum  15497  bpoly2  15670  bpoly3  15671  bpoly4  15672  fsumcube  15673  efcllem  15690  ege2le3  15702  efgt0  15715  tanval2  15745  tanval3  15746  efi4p  15749  efival  15764  sinadd  15776  cosadd  15777  sinmul  15784  cos2tsin  15791  ef01bndlem  15796  cos01bnd  15798  cos1bnd  15799  cos2bnd  15800  cos01gt0  15803  sin02gt0  15804  sin4lt0  15807  odd2np1lem  15952  odd2np1  15953  opoe  15975  omoe  15976  opeo  15977  omeo  15978  nno  15994  nn0o  15995  flodddiv4  16025  bits0  16038  bitsfzolem  16044  0bits  16049  bitsinv1  16052  sadcadd  16068  smumullem  16102  6gcd4e2  16149  3lcm2e6woprm  16223  6lcm4e12  16224  pythagtriplem1  16420  pythagtriplem12  16430  pythagtriplem14  16432  pythagtriplem15  16433  pythagtriplem16  16434  pythagtriplem17  16435  iserodd  16439  prmreclem5  16524  prmreclem6  16525  4sqlem11  16559  4sqlem12  16560  prmo2  16644  prmo3  16645  dec5dvds  16668  dec2nprm  16671  decexp2  16679  2exp5  16690  2exp6  16691  2exp7  16692  2exp8  16693  2exp11  16694  2exp16  16695  7prm  16715  11prm  16719  13prm  16720  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  psgnunilem2  18993  efgtlen  19222  efgredleme  19239  frgpnabllem1  19364  lt6abl  19386  htpycc  24024  pcoval2  24060  pcocn  24061  pcohtpylem  24063  pcopt  24066  pcopt2  24067  pcoass  24068  pcorevlem  24070  csbren  24443  minveclem2  24470  ovolunlem1a  24540  ovolunlem1  24541  vitalilem4  24655  mbfi1fseqlem5  24764  dvmptre  25013  dvsincos  25025  aaliou3lem2  25383  aaliou3lem3  25384  aaliou3lem8  25385  coscn  25484  sinhalfpilem  25500  cospi  25509  ef2pi  25514  ef2kpi  25515  efper  25516  sinperlem  25517  sin2kpi  25520  cos2kpi  25521  sin2pim  25522  cos2pim  25523  sincosq3sgn  25537  sincosq4sgn  25538  tangtx  25542  sinq12gt0  25544  sincosq1eq  25549  sincos4thpi  25550  sincos6thpi  25552  sincos3rdpi  25553  pige3ALT  25556  abssinper  25557  coskpi  25559  sineq0  25560  coseq1  25561  efeq1  25564  efif1olem4  25581  eflogeq  25637  tanarg  25654  cxpsqrtlem  25737  cxpsqrt  25738  logsqrt  25739  2irrexpq  25765  root1eq1  25788  cxpeq  25790  2logb9irrALT  25828  sqrt2cxp2logb9e3  25829  ang180lem2  25840  ang180lem3  25841  quad2  25869  1cubrlem  25871  1cubr  25872  dcubic2  25874  dcubic1  25875  dcubic  25876  mcubic  25877  cubic2  25878  cubic  25879  dquartlem1  25881  dquartlem2  25882  dquart  25883  quart1lem  25885  quart1  25886  quartlem1  25887  quartlem2  25888  quartlem3  25889  quart  25891  sinasin  25919  asinsin  25922  atancj  25940  efiatan  25942  efiatan2  25947  2efiatan  25948  tanatan  25949  atantan  25953  atanbndlem  25955  atans2  25961  dvatan  25965  atantayl2  25968  leibpilem2  25971  log2cnv  25974  log2tlbnd  25975  log2ublem2  25977  log2ublem3  25978  log2ub  25979  birthday  25984  zetacvg  26044  basellem1  26110  basellem3  26112  basellem8  26117  basellem9  26118  cht3  26202  1sgm2ppw  26228  ppiub  26232  chtublem  26239  chtub  26240  perfect1  26256  perfectlem1  26257  perfectlem2  26258  perfect  26259  bcmax  26306  bcp1ctr  26307  bclbnd  26308  bpos1lem  26310  bpos1  26311  bposlem1  26312  bposlem2  26313  bposlem4  26315  bposlem5  26316  bposlem6  26317  bposlem8  26319  bposlem9  26320  lgsdir2lem2  26354  gausslemma2dlem6  26400  lgsquadlem1  26408  lgsquadlem2  26409  lgsquad2lem2  26413  m1lgs  26416  2lgslem3a  26424  2lgslem3b  26425  2lgslem3c  26426  2lgslem3d  26427  2lgsoddprmlem2  26437  2lgsoddprmlem3c  26440  2lgsoddprmlem3d  26441  addsqnreup  26471  addsq2nreurex  26472  rplogsumlem1  26512  dchrisum0fno1  26539  dchrisum0lem1  26544  dchrisum0lem2  26546  logdivsum  26561  mulog2sumlem3  26564  log2sumbnd  26572  selberglem1  26573  selberglem2  26574  selberg2  26579  selberg4lem1  26588  selberg3r  26597  pntpbnd1a  26613  pntpbnd2  26615  pntibndlem2  26619  pntlemk  26634  ax5seglem7  27181  axlowdimlem13  27200  elwspths2spth  28208  clwlkclwwlklem2a4  28237  clwwlknonex2  28349  2clwwlk2  28588  numclwlk1lem1  28609  ex-fl  28687  ex-ceil  28688  ex-exp  28690  ex-fac  28691  ex-abs  28695  ex-ind-dvds  28701  ipidsq  28948  cncph  29057  ip0i  29063  ip1ilem  29064  ipdirilem  29067  minvecolem2  29113  hvsubcan2i  29302  norm-ii-i  29375  norm3lem  29387  normpar2i  29394  polid2i  29395  hhph  29416  mayete3i  29966  nmcexi  30264  opsqrlem6  30383  addltmulALT  30684  omssubadd  32142  oddpwdc  32196  fib5  32247  ballotlem2  32330  ballotth  32379  efmul2picn  32451  itgexpif  32461  vtscl  32493  circlemeth  32495  hgt750lemd  32503  logdivsqrle  32505  hgt750lem  32506  hgt750lem2  32507  problem4  33501  problem5  33502  quad3  33503  cnndvlem1  34619  sin2h  35673  cos2h  35674  tan2h  35675  poimirlem29  35712  mblfinlem1  35720  mblfinlem2  35721  mblfinlem3  35722  itg2addnclem3  35736  dvasin  35767  areacirc  35776  heiborlem6  35880  12gcd5e1  39918  12lcm5e60  39923  60lcm7e420  39925  420lcm8e840  39926  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  aks4d1p1p5  39989  aks4d1p1  39990  facp2  39999  fac2xp3  40060  2xp3dxp2ge1d  40062  sqn5i  40206  235t711  40212  ex-decpmul  40213  fltne  40369  flt4lem5e  40381  3cubeslem3l  40396  3cubeslem3r  40397  rmxluc  40646  rmyluc  40647  jm2.17a  40670  jm2.18  40698  jm2.23  40706  jm3.1lem1  40727  proot1ex  40914  areaquad  40935  sqrtcval  41110  resqrtvalex  41114  lhe4.4ex1a  41809  sineq0ALT  42419  coskpi2  43270  cosnegpi  43271  cosknegpi  43273  stoweidlem26  43430  wallispilem4  43472  wallispi  43474  wallispi2lem1  43475  stirlinglem8  43485  dirkerper  43500  dirkertrigeqlem3  43504  dirkertrigeq  43505  dirkeritg  43506  dirkercncflem1  43507  dirkercncflem2  43508  fourierdlem57  43567  fourierdlem58  43568  fourierdlem62  43572  fourierdlem76  43586  fourierdlem103  43613  fourierdlem104  43614  sqwvfourb  43633  fourierswlem  43634  fmtnoge3  44843  fmtnorec1  44850  fmtno0  44853  fmtno1  44854  fmtnorec3  44861  fmtnorec4  44862  fmtno5lem2  44867  fmtno5lem4  44869  257prm  44874  fmtnoprmfac2lem1  44879  fmtno4prmfac  44885  fmtno5faclem2  44893  fmtno5faclem3  44894  fmtno5fac  44895  139prmALT  44909  31prm  44910  127prm  44912  mod42tp1mod8  44915  lighneallem2  44919  lighneallem3  44920  lighneallem4a  44921  3exp4mod41  44929  41prothprmlem1  44930  41prothprmlem2  44931  41prothprm  44932  bits0ALTV  44992  0evenALTV  45001  6even  45024  8even  45026  perfectALTVlem1  45034  perfectALTVlem2  45035  perfectALTV  45036  2exp340mod341  45046  8exp8mod9  45049  mogoldbb  45098  nnsum3primes4  45101  bgoldbtbndlem1  45118  0nodd  45225  0even  45350  2even  45352  2zrngamgm  45358  2t6m3t4e0  45545  linevalexample  45597  zlmodzxzequap  45701  pw2m1lepw2m1  45722  nnlog2ge0lt1  45773  logbpw2m1  45774  nnpw2blen  45787  nnpw2pmod  45790  blen1  45791  blen2  45792  blennnt2  45796  nnolog2flm1  45797  0dig2nn0e  45819  0dig2nn0o  45820  nn0sumshdiglemA  45826  nn0sumshdiglemB  45827  nn0sumshdiglem1  45828  nn0sumshdiglem2  45829  ackval1012  45897  ackval2012  45898  ackval3012  45899  ackval42  45903  sinhpcosh  46301