Theorem 2cn 11713

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 11701	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 10595	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 10647	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2909	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   + caddc 10540  2c2 11693

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-2 11701

This theorem is referenced by:  2ex  11715  2cnd  11716  3cn  11719  2m1e1  11764  3m1e2  11766  2p2e4  11773  times2  11775  2div2e1  11779  1p2e3ALT  11782  3p3e6  11790  4p3e7  11792  5p3e8  11795  6p3e9  11798  2t1e2  11801  2t2e4  11802  3t3e9  11805  2t0e0  11807  4d2e2  11808  2cnne0  11848  halfcn  11853  1mhlfehlf  11857  8th4div3  11858  halfpm6th  11859  2mulicn  11861  2muline0  11862  halfcl  11863  half0  11865  2halves  11866  halfaddsub  11871  div4p1lem1div2  11893  3halfnz  12062  zneo  12066  nneo  12067  zeo  12069  7p3e10  12174  4t4e16  12198  6t3e18  12204  7t7e49  12213  8t5e40  12217  9t9e81  12228  decbin0  12239  decbin2  12240  halfthird  12242  fztpval  12970  fz0tp  13009  fz0to4untppr  13011  fzo0to3tp  13124  fzo1to4tp  13126  expubnd  13542  sq2  13561  sq4e2t8  13563  cu2  13564  subsq2  13574  binom2sub  13582  binom3  13586  zesq  13588  fac2  13640  fac3  13641  faclbnd2  13652  faclbnd4lem1  13654  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd5  13659  bcn2  13680  4bc2eq6  13690  swrd2lsw  14314  crre  14473  addcj  14507  imval2  14510  sqrlem7  14608  absmax  14689  rddif  14700  sqreulem  14719  amgm2  14729  abs3lemi  14770  iseraltlem2  15039  ackbijnn  15183  climcndslem1  15204  climcndslem2  15205  arisum  15215  arisum2  15216  geo2sum2  15230  geo2lim  15231  geoihalfsum  15238  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  efcllem  15431  ege2le3  15443  efgt0  15456  tanval2  15486  tanval3  15487  efi4p  15490  efival  15505  sinadd  15517  cosadd  15518  sinmul  15525  cos2tsin  15532  ef01bndlem  15537  cos01bnd  15539  cos1bnd  15540  cos2bnd  15541  cos01gt0  15544  sin02gt0  15545  sin4lt0  15548  odd2np1lem  15689  odd2np1  15690  opoe  15712  omoe  15713  opeo  15714  omeo  15715  nno  15733  nn0o  15734  flodddiv4  15764  bits0  15777  bitsfzolem  15783  0bits  15788  bitsinv1  15791  sadcadd  15807  smumullem  15841  6gcd4e2  15886  3lcm2e6woprm  15959  6lcm4e12  15960  pythagtriplem1  16153  pythagtriplem12  16163  pythagtriplem14  16165  pythagtriplem15  16166  pythagtriplem16  16167  pythagtriplem17  16168  iserodd  16172  prmreclem5  16256  prmreclem6  16257  4sqlem11  16291  4sqlem12  16292  prmo2  16376  prmo3  16377  dec5dvds  16400  dec2nprm  16403  decexp2  16411  2exp6  16422  2exp8  16423  2exp16  16424  7prm  16444  11prm  16448  13prm  16449  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  psgnunilem2  18623  efgtlen  18852  efgredleme  18869  frgpnabllem1  18993  lt6abl  19015  htpycc  23584  pcoval2  23620  pcocn  23621  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  csbren  24002  minveclem2  24029  ovolunlem1a  24097  ovolunlem1  24098  vitalilem4  24212  mbfi1fseqlem5  24320  dvmptre  24566  dvsincos  24578  aaliou3lem2  24932  aaliou3lem3  24933  aaliou3lem8  24934  coscn  25033  sinhalfpilem  25049  cospi  25058  ef2pi  25063  ef2kpi  25064  efper  25065  sinperlem  25066  sin2kpi  25069  cos2kpi  25070  sin2pim  25071  cos2pim  25072  sincosq3sgn  25086  sincosq4sgn  25087  tangtx  25091  sinq12gt0  25093  sincosq1eq  25098  sincos4thpi  25099  sincos6thpi  25101  sincos3rdpi  25102  pige3ALT  25105  abssinper  25106  coskpi  25108  sineq0  25109  coseq1  25110  efeq1  25113  efif1olem4  25129  eflogeq  25185  tanarg  25202  cxpsqrtlem  25285  cxpsqrt  25286  logsqrt  25287  2irrexpq  25313  root1eq1  25336  cxpeq  25338  2logb9irrALT  25376  sqrt2cxp2logb9e3  25377  ang180lem2  25388  ang180lem3  25389  quad2  25417  1cubrlem  25419  1cubr  25420  dcubic2  25422  dcubic1  25423  dcubic  25424  mcubic  25425  cubic2  25426  cubic  25427  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  quartlem3  25437  quart  25439  sinasin  25467  asinsin  25470  atancj  25488  efiatan  25490  efiatan2  25495  2efiatan  25496  tanatan  25497  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl2  25516  leibpilem2  25519  log2cnv  25522  log2tlbnd  25523  log2ublem2  25525  log2ublem3  25526  log2ub  25527  birthday  25532  zetacvg  25592  basellem1  25658  basellem3  25660  basellem8  25665  basellem9  25666  cht3  25750  1sgm2ppw  25776  ppiub  25780  chtublem  25787  chtub  25788  perfect1  25804  perfectlem1  25805  perfectlem2  25806  perfect  25807  bcmax  25854  bcp1ctr  25855  bclbnd  25856  bpos1lem  25858  bpos1  25859  bposlem1  25860  bposlem2  25861  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgsdir2lem2  25902  gausslemma2dlem6  25948  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem2  25961  m1lgs  25964  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgsoddprmlem2  25985  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  addsqnreup  26019  addsq2nreurex  26020  rplogsumlem1  26060  dchrisum0fno1  26087  dchrisum0lem1  26092  dchrisum0lem2  26094  logdivsum  26109  mulog2sumlem3  26112  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  selberg2  26127  selberg4lem1  26136  selberg3r  26145  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemk  26182  ax5seglem7  26721  axlowdimlem13  26740  elwspths2spth  27746  clwlkclwwlklem2a4  27775  clwwlknonex2  27888  2clwwlk2  28127  numclwlk1lem1  28148  ex-fl  28226  ex-ceil  28227  ex-exp  28229  ex-fac  28230  ex-abs  28234  ex-ind-dvds  28240  ipidsq  28487  cncph  28596  ip0i  28602  ip1ilem  28603  ipdirilem  28606  minvecolem2  28652  hvsubcan2i  28841  norm-ii-i  28914  norm3lem  28926  normpar2i  28933  polid2i  28934  hhph  28955  mayete3i  29505  nmcexi  29803  opsqrlem6  29922  addltmulALT  30223  omssubadd  31558  oddpwdc  31612  fib5  31663  ballotlem2  31746  ballotth  31795  efmul2picn  31867  itgexpif  31877  vtscl  31909  circlemeth  31911  hgt750lemd  31919  logdivsqrle  31921  hgt750lem  31922  hgt750lem2  31923  problem4  32911  problem5  32912  quad3  32913  cnndvlem1  33876  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem29  34936  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  itg2addnclem3  34960  dvasin  34993  areacirc  35002  heiborlem6  35109  12gcd5e1  39124  12lcm5e60  39129  60lcm7e420  39131  420lcm8e840  39132  fac2xp3  39143  facp2  39144  2xp3dxp2ge1d  39146  sqn5i  39220  235t711  39226  ex-decpmul  39227  3cubeslem3l  39332  3cubeslem3r  39333  rmxluc  39582  rmyluc  39583  jm2.17a  39606  jm2.18  39634  jm2.23  39642  jm3.1lem1  39663  proot1ex  39850  areaquad  39872  lhe4.4ex1a  40710  sineq0ALT  41320  coskpi2  42196  cosnegpi  42197  cosknegpi  42199  stoweidlem26  42360  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  stirlinglem8  42415  dirkerper  42430  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkeritg  42436  dirkercncflem1  42437  dirkercncflem2  42438  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem76  42516  fourierdlem103  42543  fourierdlem104  42544  sqwvfourb  42563  fourierswlem  42564  fmtnoge3  43741  fmtnorec1  43748  fmtno0  43751  fmtno1  43752  fmtnorec3  43759  fmtnorec4  43760  fmtno5lem2  43765  fmtno5lem4  43767  257prm  43772  fmtnoprmfac2lem1  43777  fmtno4prmfac  43783  fmtno5faclem2  43791  fmtno5faclem3  43792  fmtno5fac  43793  2exp5  43804  139prmALT  43808  31prm  43809  2exp7  43811  127prm  43812  2exp11  43814  mod42tp1mod8  43816  lighneallem2  43820  lighneallem3  43821  lighneallem4a  43822  3exp4mod41  43830  41prothprmlem1  43831  41prothprmlem2  43832  41prothprm  43833  bits0ALTV  43893  0evenALTV  43902  6even  43925  8even  43927  perfectALTVlem1  43935  perfectALTVlem2  43936  perfectALTV  43937  2exp340mod341  43947  8exp8mod9  43950  mogoldbb  43999  nnsum3primes4  44002  bgoldbtbndlem1  44019  0nodd  44126  0even  44251  2even  44253  2zrngamgm  44259  2t6m3t4e0  44445  linevalexample  44499  zlmodzxzequap  44603  pw2m1lepw2m1  44624  nnlog2ge0lt1  44675  logbpw2m1  44676  nnpw2blen  44689  nnpw2pmod  44692  blen1  44693  blen2  44694  blennnt2  44698  nnolog2flm1  44699  0dig2nn0e  44721  0dig2nn0o  44722  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  nn0sumshdiglem2  44731  sinhpcosh  44888