Theorem 2cn 11791

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 11779	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 10673	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 10725	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2829	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7170  ℂcc 10613  1c1 10616   + caddc 10618  2c2 11771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-1cn 10673  ax-addcl 10675

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811  df-2 11779

This theorem is referenced by:  2ex  11793  2cnd  11794  3cn  11797  2m1e1  11842  3m1e2  11844  2p2e4  11851  times2  11853  2div2e1  11857  1p2e3ALT  11860  3p3e6  11868  4p3e7  11870  5p3e8  11873  6p3e9  11876  2t1e2  11879  2t2e4  11880  3t3e9  11883  2t0e0  11885  4d2e2  11886  2cnne0  11926  halfcn  11931  1mhlfehlf  11935  8th4div3  11936  halfpm6th  11937  2mulicn  11939  2muline0  11940  halfcl  11941  half0  11943  2halves  11944  halfaddsub  11949  div4p1lem1div2  11971  3halfnz  12142  zneo  12146  nneo  12147  zeo  12149  7p3e10  12254  4t4e16  12278  6t3e18  12284  7t7e49  12293  8t5e40  12297  9t9e81  12308  decbin0  12319  decbin2  12320  halfthird  12322  fztpval  13060  fz0tp  13099  fz0to4untppr  13101  fzo0to3tp  13214  fzo1to4tp  13216  expubnd  13633  sq2  13652  sq4e2t8  13654  cu2  13655  subsq2  13665  binom2sub  13673  binom3  13677  zesq  13679  fac2  13731  fac3  13732  faclbnd2  13743  faclbnd4lem1  13745  faclbnd4lem3  13747  faclbnd4lem4  13748  faclbnd5  13750  bcn2  13771  4bc2eq6  13781  swrd2lsw  14403  crre  14563  addcj  14597  imval2  14600  sqrlem7  14698  absmax  14779  rddif  14790  sqreulem  14809  amgm2  14819  abs3lemi  14860  iseraltlem2  15132  ackbijnn  15276  climcndslem1  15297  climcndslem2  15298  arisum  15308  arisum2  15309  geo2sum2  15322  geo2lim  15323  geoihalfsum  15330  bpoly2  15503  bpoly3  15504  bpoly4  15505  fsumcube  15506  efcllem  15523  ege2le3  15535  efgt0  15548  tanval2  15578  tanval3  15579  efi4p  15582  efival  15597  sinadd  15609  cosadd  15610  sinmul  15617  cos2tsin  15624  ef01bndlem  15629  cos01bnd  15631  cos1bnd  15632  cos2bnd  15633  cos01gt0  15636  sin02gt0  15637  sin4lt0  15640  odd2np1lem  15785  odd2np1  15786  opoe  15808  omoe  15809  opeo  15810  omeo  15811  nno  15827  nn0o  15828  flodddiv4  15858  bits0  15871  bitsfzolem  15877  0bits  15882  bitsinv1  15885  sadcadd  15901  smumullem  15935  6gcd4e2  15982  3lcm2e6woprm  16056  6lcm4e12  16057  pythagtriplem1  16253  pythagtriplem12  16263  pythagtriplem14  16265  pythagtriplem15  16266  pythagtriplem16  16267  pythagtriplem17  16268  iserodd  16272  prmreclem5  16356  prmreclem6  16357  4sqlem11  16391  4sqlem12  16392  prmo2  16476  prmo3  16477  dec5dvds  16500  dec2nprm  16503  decexp2  16511  2exp5  16522  2exp6  16523  2exp7  16524  2exp8  16525  2exp11  16526  2exp16  16527  7prm  16547  11prm  16551  13prm  16552  37prm  16557  43prm  16558  83prm  16559  139prm  16560  163prm  16561  317prm  16562  631prm  16563  1259lem1  16567  1259lem2  16568  1259lem3  16569  1259lem4  16570  1259lem5  16571  1259prm  16572  2503lem1  16573  2503lem2  16574  2503lem3  16575  4001lem1  16577  4001lem2  16578  4001lem3  16579  4001lem4  16580  4001prm  16581  psgnunilem2  18741  efgtlen  18970  efgredleme  18987  frgpnabllem1  19112  lt6abl  19134  htpycc  23732  pcoval2  23768  pcocn  23769  pcohtpylem  23771  pcopt  23774  pcopt2  23775  pcoass  23776  pcorevlem  23778  csbren  24151  minveclem2  24178  ovolunlem1a  24248  ovolunlem1  24249  vitalilem4  24363  mbfi1fseqlem5  24472  dvmptre  24721  dvsincos  24733  aaliou3lem2  25091  aaliou3lem3  25092  aaliou3lem8  25093  coscn  25192  sinhalfpilem  25208  cospi  25217  ef2pi  25222  ef2kpi  25223  efper  25224  sinperlem  25225  sin2kpi  25228  cos2kpi  25229  sin2pim  25230  cos2pim  25231  sincosq3sgn  25245  sincosq4sgn  25246  tangtx  25250  sinq12gt0  25252  sincosq1eq  25257  sincos4thpi  25258  sincos6thpi  25260  sincos3rdpi  25261  pige3ALT  25264  abssinper  25265  coskpi  25267  sineq0  25268  coseq1  25269  efeq1  25272  efif1olem4  25289  eflogeq  25345  tanarg  25362  cxpsqrtlem  25445  cxpsqrt  25446  logsqrt  25447  2irrexpq  25473  root1eq1  25496  cxpeq  25498  2logb9irrALT  25536  sqrt2cxp2logb9e3  25537  ang180lem2  25548  ang180lem3  25549  quad2  25577  1cubrlem  25579  1cubr  25580  dcubic2  25582  dcubic1  25583  dcubic  25584  mcubic  25585  cubic2  25586  cubic  25587  dquartlem1  25589  dquartlem2  25590  dquart  25591  quart1lem  25593  quart1  25594  quartlem1  25595  quartlem2  25596  quartlem3  25597  quart  25599  sinasin  25627  asinsin  25630  atancj  25648  efiatan  25650  efiatan2  25655  2efiatan  25656  tanatan  25657  atantan  25661  atanbndlem  25663  atans2  25669  dvatan  25673  atantayl2  25676  leibpilem2  25679  log2cnv  25682  log2tlbnd  25683  log2ublem2  25685  log2ublem3  25686  log2ub  25687  birthday  25692  zetacvg  25752  basellem1  25818  basellem3  25820  basellem8  25825  basellem9  25826  cht3  25910  1sgm2ppw  25936  ppiub  25940  chtublem  25947  chtub  25948  perfect1  25964  perfectlem1  25965  perfectlem2  25966  perfect  25967  bcmax  26014  bcp1ctr  26015  bclbnd  26016  bpos1lem  26018  bpos1  26019  bposlem1  26020  bposlem2  26021  bposlem4  26023  bposlem5  26024  bposlem6  26025  bposlem8  26027  bposlem9  26028  lgsdir2lem2  26062  gausslemma2dlem6  26108  lgsquadlem1  26116  lgsquadlem2  26117  lgsquad2lem2  26121  m1lgs  26124  2lgslem3a  26132  2lgslem3b  26133  2lgslem3c  26134  2lgslem3d  26135  2lgsoddprmlem2  26145  2lgsoddprmlem3c  26148  2lgsoddprmlem3d  26149  addsqnreup  26179  addsq2nreurex  26180  rplogsumlem1  26220  dchrisum0fno1  26247  dchrisum0lem1  26252  dchrisum0lem2  26254  logdivsum  26269  mulog2sumlem3  26272  log2sumbnd  26280  selberglem1  26281  selberglem2  26282  selberg2  26287  selberg4lem1  26296  selberg3r  26305  pntpbnd1a  26321  pntpbnd2  26323  pntibndlem2  26327  pntlemk  26342  ax5seglem7  26881  axlowdimlem13  26900  elwspths2spth  27905  clwlkclwwlklem2a4  27934  clwwlknonex2  28046  2clwwlk2  28285  numclwlk1lem1  28306  ex-fl  28384  ex-ceil  28385  ex-exp  28387  ex-fac  28388  ex-abs  28392  ex-ind-dvds  28398  ipidsq  28645  cncph  28754  ip0i  28760  ip1ilem  28761  ipdirilem  28764  minvecolem2  28810  hvsubcan2i  28999  norm-ii-i  29072  norm3lem  29084  normpar2i  29091  polid2i  29092  hhph  29113  mayete3i  29663  nmcexi  29961  opsqrlem6  30080  addltmulALT  30381  omssubadd  31837  oddpwdc  31891  fib5  31942  ballotlem2  32025  ballotth  32074  efmul2picn  32146  itgexpif  32156  vtscl  32188  circlemeth  32190  hgt750lemd  32198  logdivsqrle  32200  hgt750lem  32201  hgt750lem2  32202  problem4  33197  problem5  33198  quad3  33199  cnndvlem1  34355  sin2h  35390  cos2h  35391  tan2h  35392  poimirlem29  35429  mblfinlem1  35437  mblfinlem2  35438  mblfinlem3  35439  itg2addnclem3  35453  dvasin  35484  areacirc  35493  heiborlem6  35597  12gcd5e1  39631  12lcm5e60  39636  60lcm7e420  39638  420lcm8e840  39639  3exp7  39681  3lexlogpow5ineq1  39682  3lexlogpow2ineq2  39687  3lexlogpow5ineq5  39688  aks4d1p1p5  39702  aks4d1p1  39703  facp2  39705  fac2xp3  39751  2xp3dxp2ge1d  39753  sqn5i  39889  235t711  39895  ex-decpmul  39896  fltne  40053  flt4lem5e  40065  3cubeslem3l  40080  3cubeslem3r  40081  rmxluc  40330  rmyluc  40331  jm2.17a  40354  jm2.18  40382  jm2.23  40390  jm3.1lem1  40411  proot1ex  40598  areaquad  40619  sqrtcval  40794  resqrtvalex  40798  lhe4.4ex1a  41485  sineq0ALT  42095  coskpi2  42949  cosnegpi  42950  cosknegpi  42952  stoweidlem26  43109  wallispilem4  43151  wallispi  43153  wallispi2lem1  43154  stirlinglem8  43164  dirkerper  43179  dirkertrigeqlem3  43183  dirkertrigeq  43184  dirkeritg  43185  dirkercncflem1  43186  dirkercncflem2  43187  fourierdlem57  43246  fourierdlem58  43247  fourierdlem62  43251  fourierdlem76  43265  fourierdlem103  43292  fourierdlem104  43293  sqwvfourb  43312  fourierswlem  43313  fmtnoge3  44516  fmtnorec1  44523  fmtno0  44526  fmtno1  44527  fmtnorec3  44534  fmtnorec4  44535  fmtno5lem2  44540  fmtno5lem4  44542  257prm  44547  fmtnoprmfac2lem1  44552  fmtno4prmfac  44558  fmtno5faclem2  44566  fmtno5faclem3  44567  fmtno5fac  44568  139prmALT  44582  31prm  44583  127prm  44585  mod42tp1mod8  44588  lighneallem2  44592  lighneallem3  44593  lighneallem4a  44594  3exp4mod41  44602  41prothprmlem1  44603  41prothprmlem2  44604  41prothprm  44605  bits0ALTV  44665  0evenALTV  44674  6even  44697  8even  44699  perfectALTVlem1  44707  perfectALTVlem2  44708  perfectALTV  44709  2exp340mod341  44719  8exp8mod9  44722  mogoldbb  44771  nnsum3primes4  44774  bgoldbtbndlem1  44791  0nodd  44898  0even  45023  2even  45025  2zrngamgm  45031  2t6m3t4e0  45218  linevalexample  45270  zlmodzxzequap  45374  pw2m1lepw2m1  45395  nnlog2ge0lt1  45446  logbpw2m1  45447  nnpw2blen  45460  nnpw2pmod  45463  blen1  45464  blen2  45465  blennnt2  45469  nnolog2flm1  45470  0dig2nn0e  45492  0dig2nn0o  45493  nn0sumshdiglemA  45499  nn0sumshdiglemB  45500  nn0sumshdiglem1  45501  nn0sumshdiglem2  45502  ackval1012  45570  ackval2012  45571  ackval3012  45572  ackval42  45576  sinhpcosh  45895