Theorem 2cn 11455

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 11443	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 10332	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 10385	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2855	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 6924  ℂcc 10272  1c1 10275   + caddc 10277  2c2 11435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754  ax-1cn 10332  ax-addcl 10334

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774  df-2 11443

This theorem is referenced by:  2ex  11457  2cnd  11458  3cn  11461  2m1e1  11513  3m1e2  11515  2p2e4  11522  times2  11524  2div2e1  11528  1p2e3ALT  11531  3p3e6  11539  4p3e7  11541  5p3e8  11544  6p3e9  11547  2t1e2  11550  2t2e4  11551  3t3e9  11554  2t0e0  11556  4d2e2  11557  2cnne0  11597  halfcn  11602  1mhlfehlf  11606  8th4div3  11607  halfpm6th  11608  2mulicn  11610  2muline0  11611  halfcl  11612  half0  11614  2halves  11615  halfaddsub  11620  div4p1lem1div2  11642  3halfnz  11813  zneo  11817  nneo  11818  zeo  11820  7p3e10  11927  4t4e16  11951  6t3e18  11957  7t7e49  11966  8t5e40  11970  9t9e81  11981  decbin0  11992  decbin2  11993  halfthird  11995  fztpval  12725  fz0tp  12764  fz0to4untppr  12766  fzo0to3tp  12878  fzo1to4tp  12880  expubnd  13244  sq2  13284  sq4e2t8  13286  cu2  13287  subsq2  13297  binom2sub  13305  binom3  13309  zesq  13311  fac2  13390  fac3  13391  faclbnd2  13402  faclbnd4lem1  13404  faclbnd4lem3  13406  faclbnd4lem4  13407  faclbnd5  13409  bcn2  13430  4bc2eq6  13440  swrd2lsw  14109  crre  14267  addcj  14301  imval2  14304  sqrlem7  14402  absmax  14483  rddif  14494  sqreulem  14513  amgm2  14523  abs3lemi  14564  iseraltlem2  14830  ackbijnn  14973  climcndslem1  14994  climcndslem2  14995  arisum  15005  arisum2  15006  geo2sum2  15018  geo2lim  15019  geoihalfsum  15026  bpoly2  15199  bpoly3  15200  bpoly4  15201  fsumcube  15202  efcllem  15219  ege2le3  15231  efgt0  15244  tanval2  15274  tanval3  15275  efi4p  15278  efival  15293  sinadd  15305  cosadd  15306  sinmul  15313  cos2tsin  15320  ef01bndlem  15325  cos01bnd  15327  cos1bnd  15328  cos2bnd  15329  cos01gt0  15332  sin02gt0  15333  sin4lt0  15336  znnenlemOLD  15353  odd2np1lem  15478  odd2np1  15479  opoe  15501  omoe  15502  opeo  15503  omeo  15504  nno  15522  nn0o  15523  flodddiv4  15553  bits0  15566  bitsfzolem  15572  0bits  15577  bitsinv1  15580  sadcadd  15596  smumullem  15630  6gcd4e2  15671  3lcm2e6woprm  15744  6lcm4e12  15745  pythagtriplem1  15936  pythagtriplem12  15946  pythagtriplem14  15948  pythagtriplem15  15949  pythagtriplem16  15950  pythagtriplem17  15951  iserodd  15955  prmreclem5  16039  prmreclem6  16040  4sqlem11  16074  4sqlem12  16075  prmo2  16159  prmo3  16160  dec5dvds  16183  dec2nprm  16186  decexp2  16194  2exp6  16205  2exp8  16206  2exp16  16207  7prm  16227  11prm  16231  13prm  16232  37prm  16237  43prm  16238  83prm  16239  139prm  16240  163prm  16241  317prm  16242  631prm  16243  1259lem1  16247  1259lem2  16248  1259lem3  16249  1259lem4  16250  1259lem5  16251  1259prm  16252  2503lem1  16253  2503lem2  16254  2503lem3  16255  4001lem1  16257  4001lem2  16258  4001lem3  16259  4001lem4  16260  4001prm  16261  psgnunilem2  18310  efgtlen  18534  efgredleme  18552  frgpnabllem1  18673  lt6abl  18693  htpycc  23198  pcoval2  23234  pcocn  23235  pcohtpylem  23237  pcopt  23240  pcopt2  23241  pcoass  23242  pcorevlem  23244  csbren  23616  minveclem2  23643  ovolunlem1a  23711  ovolunlem1  23712  vitalilem4  23826  mbfi1fseqlem5  23934  dvmptre  24180  dvsincos  24192  aaliou3lem2  24546  aaliou3lem3  24547  aaliou3lem8  24548  coscn  24647  sinhalfpilem  24664  cospi  24673  ef2pi  24678  ef2kpi  24679  efper  24680  sinperlem  24681  sin2kpi  24684  cos2kpi  24685  sin2pim  24686  cos2pim  24687  sinhalfpip  24693  sinhalfpim  24694  coshalfpip  24695  coshalfpim  24696  sincosq3sgn  24701  sincosq4sgn  24702  tangtx  24706  sinq12gt0  24708  sincosq1eq  24713  sincos4thpi  24714  sincos6thpi  24716  sincos3rdpi  24717  pige3  24718  abssinper  24719  coskpi  24721  sineq0  24722  coseq1  24723  efeq1  24724  efif1olem4  24740  eflogeq  24796  tanarg  24813  cxpsqrtlem  24896  cxpsqrt  24897  logsqrt  24898  2irrexpq  24924  root1eq1  24947  cxpeq  24949  2logb9irrALT  24987  sqrt2cxp2logb9e3  24988  ang180lem2  24999  ang180lem3  25000  quad2  25028  1cubrlem  25030  1cubr  25031  dcubic2  25033  dcubic1  25034  dcubic  25035  mcubic  25036  cubic2  25037  cubic  25038  dquartlem1  25040  dquartlem2  25041  dquart  25042  quart1lem  25044  quart1  25045  quartlem1  25046  quartlem2  25047  quartlem3  25048  quart  25050  sinasin  25078  asinsin  25081  atancj  25099  efiatan  25101  efiatan2  25106  2efiatan  25107  tanatan  25108  atantan  25112  atanbndlem  25114  atans2  25120  dvatan  25124  atantayl2  25127  leibpilem1OLD  25130  leibpilem2  25131  log2cnv  25134  log2tlbnd  25135  log2ublem2  25137  log2ublem3  25138  log2ub  25139  birthday  25144  zetacvg  25204  basellem1  25270  basellem3  25272  basellem8  25277  basellem9  25278  cht3  25362  1sgm2ppw  25388  ppiub  25392  chtublem  25399  chtub  25400  perfect1  25416  perfectlem1  25417  perfectlem2  25418  perfect  25419  bcmax  25466  bcp1ctr  25467  bclbnd  25468  bpos1lem  25470  bpos1  25471  bposlem1  25472  bposlem2  25473  bposlem4  25475  bposlem5  25476  bposlem6  25477  bposlem8  25479  bposlem9  25480  lgsdir2lem2  25514  gausslemma2dlem6  25560  lgsquadlem1  25568  lgsquadlem2  25569  lgsquad2lem2  25573  m1lgs  25576  2lgslem3a  25584  2lgslem3b  25585  2lgslem3c  25586  2lgslem3d  25587  2lgsoddprmlem2  25597  2lgsoddprmlem3c  25600  2lgsoddprmlem3d  25601  rplogsumlem1  25642  dchrisum0fno1  25669  dchrisum0lem1  25674  dchrisum0lem2  25676  logdivsum  25691  mulog2sumlem3  25694  log2sumbnd  25702  selberglem1  25703  selberglem2  25704  selberg2  25709  selberg4lem1  25718  selberg3r  25727  pntpbnd1a  25743  pntpbnd2  25745  pntibndlem2  25749  pntlemk  25764  ax5seglem7  26301  axlowdimlem13  26320  elwspths2spth  27364  clwlkclwwlklem2a4  27394  clwwlknonex2  27528  2clwwlk2  27776  numclwlk1lem1  27814  ex-fl  27896  ex-ceil  27897  ex-exp  27899  ex-fac  27900  ex-abs  27904  ex-ind-dvds  27910  ipidsq  28154  cncph  28263  ip0i  28269  ip1ilem  28270  ipdirilem  28273  minvecolem2  28320  hvsubcan2i  28510  norm-ii-i  28583  norm3lem  28595  normpar2i  28602  polid2i  28603  hhph  28624  mayete3i  29176  nmcexi  29474  opsqrlem6  29593  addltmulALT  29894  omssubadd  30968  oddpwdc  31022  fib5  31074  ballotlem2  31157  ballotth  31206  efmul2picn  31284  itgexpif  31294  vtscl  31326  circlemeth  31328  hgt750lemd  31336  logdivsqrle  31338  hgt750lem  31339  hgt750lem2  31340  problem4  32167  problem5  32168  quad3  32169  cnndvlem1  33118  sin2h  34033  cos2h  34034  tan2h  34035  poimirlem29  34073  mblfinlem1  34081  mblfinlem2  34082  mblfinlem3  34083  itg2addnclem3  34097  dvasin  34130  areacirc  34139  heiborlem6  34248  sqn5i  38161  235t711  38167  ex-decpmul  38168  rmxluc  38474  rmyluc  38475  jm2.17a  38500  jm2.18  38528  jm2.23  38536  jm3.1lem1  38557  proot1ex  38752  areaquad  38774  lhe4.4ex1a  39498  sineq0ALT  40120  coskpi2  41019  cosnegpi  41020  cosknegpi  41022  stoweidlem26  41184  wallispilem4  41226  wallispi  41228  wallispi2lem1  41229  stirlinglem8  41239  dirkerper  41254  dirkertrigeqlem3  41258  dirkertrigeq  41259  dirkeritg  41260  dirkercncflem1  41261  dirkercncflem2  41262  fourierdlem57  41321  fourierdlem58  41322  fourierdlem62  41326  fourierdlem76  41340  fourierdlem103  41367  fourierdlem104  41368  sqwvfourb  41387  fourierswlem  41388  fmtnoge3  42477  fmtnorec1  42484  fmtno0  42487  fmtno1  42488  fmtnorec3  42495  fmtnorec4  42496  fmtno5lem2  42501  fmtno5lem4  42503  257prm  42508  fmtnoprmfac2lem1  42513  fmtno4prmfac  42519  fmtno5faclem2  42527  fmtno5faclem3  42528  fmtno5fac  42529  2exp5  42542  139prmALT  42546  31prm  42547  2exp7  42549  127prm  42550  2exp11  42552  mod42tp1mod8  42554  lighneallem2  42558  lighneallem3  42559  lighneallem4a  42560  3exp4mod41  42568  41prothprmlem1  42569  41prothprmlem2  42570  41prothprm  42571  bits0ALTV  42629  0evenALTV  42638  6even  42659  8even  42661  perfectALTVlem1  42669  perfectALTVlem2  42670  perfectALTV  42671  mogoldbb  42712  nnsum3primes4  42715  bgoldbtbndlem1  42732  0nodd  42839  0even  42960  2even  42962  2zrngamgm  42968  2t6m3t4e0  43155  linevalexample  43213  zlmodzxzequap  43317  pw2m1lepw2m1  43339  nnlog2ge0lt1  43389  logbpw2m1  43390  nnpw2blen  43403  nnpw2pmod  43406  blen1  43407  blen2  43408  blennnt2  43412  nnolog2flm1  43413  0dig2nn0e  43435  0dig2nn0o  43436  nn0sumshdiglemA  43442  nn0sumshdiglemB  43443  nn0sumshdiglem1  43444  nn0sumshdiglem2  43445  sinhpcosh  43603