Theorem 2cn 12445

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 12432	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11285	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11342	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2860	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   + caddc 11230  2c2 12424

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-addcl 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12432

This theorem is used by:  2ex  12447  2cnd  12448  3cn  12451  2thalfe1  12477  2m1e1OLD  12495  3m1e2  12497  2p2e4  12504  times2  12506  2div2e1  12510  1p2e3ALT  12513  3p3e6  12521  4p3e7  12523  5p3e8  12526  6p3e9  12529  2t1e2  12532  2t2e4  12533  2t3e6  12536  3t3e9  12537  2t4e8  12539  2t0e0  12540  4div2e2  12541  2cnne0  12582  halfcn  12587  2halves  12591  8th4div3  12593  halfthird  12594  halfpm6th  12595  2mulicn  12597  2muline0  12598  halfcl  12599  half0  12601  halfaddsub  12606  div4p1lem1div2  12628  3halfnz  12805  zneo  12809  nneo  12810  zeo  12812  7p3e10  12921  4t4e16  12945  6t3e18  12951  7t7e49  12960  8t5e40  12964  9t9e81  12975  decbin0  12988  decbin2  12989  fztpval  13747  fz0tp  13789  fzo0to3tp  13914  fzo1to4tp  13916  expubnd  14348  sq2  14367  sq4e2t8  14369  cu2  14370  subsq2  14382  binom2sub  14391  binom3  14395  zesq  14397  fac2  14450  faclbnd2  14462  faclbnd4lem1  14464  faclbnd4lem3  14466  faclbnd4lem4  14467  faclbnd5  14469  bcn2  14490  4bc2eq6  14500  swrd2lsw  15134  crre  15310  addcj  15344  imval2  15347  01sqrexlem7  15444  absmax  15526  sqreulem  15556  amgm2  15566  abs3lemi  15607  iseraltlem2  15879  ackbijnn  16026  climcndslem1  16047  climcndslem2  16048  arisum  16058  arisum2  16059  geo2sum2  16072  geo2lim  16073  geoihalfsum  16080  bpoly2  16252  bpoly3  16253  bpoly4  16254  fsumcube  16255  efcllem  16272  ege2le3  16285  efgt0  16300  tanval2  16330  tanval3  16331  efi4p  16334  efival  16349  sinadd  16361  cosadd  16362  sinmul  16369  cos2tsin  16376  ef01bndlem  16381  cos01bnd  16383  cos1bnd  16384  cos2bnd  16385  cos01gt0  16388  sin02gt0  16389  sin4lt0  16392  odd2np1lem  16539  odd2np1  16540  opoe  16562  omoe  16563  opeo  16564  omeo  16565  nno  16581  nn0o  16582  flodddiv4  16614  bits0  16627  bitsfzolem  16633  0bits  16638  bitsinv1  16641  sadcadd  16657  smumullem  16691  6gcd4e2  16740  3lcm2e6woprm  16819  6lcm4e12  16820  pythagtriplem1  17023  pythagtriplem12  17033  pythagtriplem14  17035  pythagtriplem15  17036  pythagtriplem16  17037  pythagtriplem17  17038  iserodd  17042  prmreclem5  17127  prmreclem6  17128  4sqlem11  17162  4sqlem12  17163  prmo2  17247  dec5dvds  17271  dec2nprm  17274  2exp5  17292  2exp7  17294  2exp11  17296  2exp16  17297  10nprm  17320  11prm  17322  13prm  17323  37prm  17328  43prm  17329  83prm  17330  139prm  17331  163prm  17332  317prm  17333  631prm  17334  1259lem1  17338  1259lem2  17339  1259lem3  17340  1259lem4  17341  1259lem5  17342  1259prm  17343  2503lem1  17344  2503lem2  17345  2503lem3  17346  4001lem1  17348  4001lem2  17349  4001lem3  17350  4001lem4  17351  4001prm  17352  psgnunilem2  19739  efgtlen  19970  efgredleme  19987  frgpnabllem1  20117  lt6abl  20139  pcoass  25375  pcorevlem  25377  csbren  25750  minveclem2  25777  ovolunlem1a  25847  ovolunlem1  25848  vitalilem4  25962  mbfi1fseqlem5  26070  dvmptre  26319  dvsincos  26331  aaliou3lem2  26700  aaliou3lem3  26701  aaliou3lem8  26702  coscn  26802  2picn  26816  sinhalfpilem  26822  cospi  26831  ef2pi  26836  ef2kpi  26837  efper  26838  sinperlem  26839  sin2kpi  26842  cos2kpi  26843  sin2pim  26844  cos2pim  26845  sincosq3sgn  26859  sincosq4sgn  26860  tangtx  26864  sinq12gt0  26866  sincosq1eq  26871  sincos4thpi  26872  sincos6thpi  26874  sincos3rdpi  26875  pige3ALT  26878  abssinper  26879  coskpi  26881  sineq0  26882  coseq1  26883  efeq1  26886  efif1olem4  26903  eflogeq  26960  tanarg  26977  cxpsqrtlem  27060  cxpsqrt  27061  logsqrt  27062  2irrexpq  27089  root1eq1  27113  cxpeq  27115  2logb9irrALT  27156  sqrt2cxp2logb9e3  27157  ang180lem2  27168  ang180lem3  27169  quad2  27197  1cubrlem  27199  1cubr  27200  dcubic2  27202  dcubic1  27203  dcubic  27204  mcubic  27205  cubic2  27206  cubic  27207  dquartlem1  27209  dquartlem2  27210  dquart  27211  quart1lem  27213  quart1  27214  quartlem1  27215  quartlem2  27216  quartlem3  27217  quart  27219  sinasin  27247  asinsin  27250  atancj  27268  efiatan  27270  efiatan2  27275  2efiatan  27276  tanatan  27277  atantan  27281  atanbndlem  27283  atans2  27289  dvatan  27293  atantayl2  27296  leibpilem2  27299  log2cnv  27302  log2tlbnd  27303  log2ublem2  27305  log2ublem3  27306  log2ub  27307  birthday  27312  zetacvg  27372  basellem1  27438  basellem3  27440  basellem8  27445  basellem9  27446  1sgm2ppw  27557  ppiub  27561  chtublem  27568  chtub  27569  perfect1  27585  perfectlem1  27586  perfectlem2  27587  perfect  27588  bcmax  27635  bcp1ctr  27636  bclbnd  27637  bpos1lem  27639  bpos1  27640  bposlem1  27641  bposlem2  27642  bposlem4  27644  bposlem5  27645  bposlem6  27646  bposlem8  27648  bposlem9  27649  lgsdir2lem2  27683  gausslemma2dlem6  27729  lgsquadlem1  27737  lgsquadlem2  27738  lgsquad2lem2  27742  m1lgs  27745  2lgslem3a  27753  2lgslem3b  27754  2lgslem3c  27755  2lgslem3d  27756  2lgsoddprmlem2  27766  2lgsoddprmlem3c  27769  2lgsoddprmlem3d  27770  addsqnreup  27800  addsq2nreurex  27801  rplogsumlem1  27841  dchrisum0fno1  27868  dchrisum0lem1  27873  dchrisum0lem2  27875  logdivsum  27890  mulog2sumlem3  27893  log2sumbnd  27901  selberglem1  27902  selberglem2  27903  selberg2  27908  selberg4lem1  27917  selberg3r  27926  pntpbnd1a  27942  pntpbnd2  27944  pntibndlem2  27948  pntlemk  27963  fltne  28005  flt4lem5e  28016  fltoprmlem2  28024  ax5seglem7  29543  axlowdimlem13  29562  elwspths2spth  30589  clwlkclwwlklem2a4  30618  clwwlknonex2  30730  2clwwlk2  30979  numclwlk1lem1  31000  ex-fl  31078  ex-ceil  31079  ex-exp  31081  ex-fac  31082  ex-abs  31086  ex-ind-dvds  31092  ipidsq  31342  cncph  31451  ip0i  31457  ip1ilem  31458  ipdirilem  31461  minvecolem2  31507  hvsubcan2i  31696  norm-ii-i  31769  norm3lem  31781  normpar2i  31788  polid2i  31789  hhph  31810  mayete3i  32360  nmcexi  32658  opsqrlem6  32777  addltmulALT  33120  ply1dg3rt0irred  34186  fldext2chn  34430  constrelextdg2  34449  2sqr3minply  34482  cos9thpiminplylem4  34487  cos9thpiminplylem5  34488  oddpwdc  35056  fib5  35107  ballotlem2  35191  ballotth  35240  efmul2picn  35295  itgexpif  35305  vtscl  35337  circlemeth  35339  hgt750lemd  35347  logdivsqrle  35349  hgt750lem  35350  hgt750lem2  35351  problem4  36600  problem5  36601  quad3  36602  cnndvlem1  37581  sin2h  38725  cos2h  38726  tan2h  38727  poimirlem29  38759  mblfinlem1  38767  mblfinlem2  38768  mblfinlem3  38769  itg2addnclem3  38783  dvasin  38814  areacirc  38823  heiborlem6  38942  12gcd5e1  43245  12lcm5e60  43250  60lcm7e420  43252  3exp7  43295  3lexlogpow5ineq1  43296  3lexlogpow5ineq5  43302  aks4d1p1p5  43317  aks4d1p1  43318  posbezout  43342  facp2  43385  25or6to4  43448  4p4e8ALT  43502  1p3e4  43503  2p3e5  43509  2p4e6  43510  2p5e7  43511  2p6e8  43512  2p7e9  43513  3p4e7  43514  3p5e8  43515  sqn5i  43535  235t711  43555  ex-decpmul  43556  cxp112d  43585  cxp111d  43586  cxpi11d  43587  tanhalfpim  43593  sum9cubes  43876  3cubeslem3r  43890  rmxluc  44136  rmyluc  44137  jm2.17a  44160  jm2.18  44188  jm2.23  44196  jm3.1lem1  44217  proot1ex  44390  areaquad  44410  sqrtcval  44833  resqrtvalex  44837  lhe4.4ex1a  45505  sineq0ALT  46110  coskpi2  47081  cosnegpi  47082  cosknegpi  47084  stoweidlem26  47241  wallispilem4  47283  wallispi  47285  wallispi2lem1  47286  stirlinglem8  47296  dirkerper  47311  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkeritg  47317  dirkercncflem1  47318  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  fourierdlem76  47397  fourierdlem103  47424  fourierdlem104  47425  sqwvfourb  47444  fourierswlem  47445  sin5tlem1  48124  sin5tlem5  48128  cos5t  48130  goldpolyfactor  48132  goldrasin  48134  goldracos5teq  48137  goldratmolem2  48138  goldratmolem3  48139  goldratmolem4  48140  rehalfge1  48614  ceil5half3  48621  modm2nep1  48647  modm1nep2  48649  modm1nem2  48650  fmtnoge3  48820  fmtnorec1  48827  fmtno0  48830  fmtno1  48831  fmtnorec3  48838  fmtnorec4  48839  fmtno5lem2  48844  fmtno5lem4  48846  257prm  48851  fmtnoprmfac2lem1  48856  fmtno4prmfac  48862  fmtno5faclem2  48870  fmtno5faclem3  48871  fmtno5fac  48872  139prmALT  48886  31prm  48887  127prm  48889  lighneallem2  48896  lighneallem3  48897  lighneallem4a  48898  3exp4mod41  48906  41prothprmlem1  48907  41prothprmlem2  48908  41prothprm  48909  bits0ALTV  48982  0evenALTV  48991  6even  49014  8even  49016  perfectALTVlem1  49024  perfectALTVlem2  49025  perfectALTV  49026  2exp340mod341  49036  mogoldbb  49088  nnsum3primes4  49091  bgoldbtbndlem1  49108  gpg5order  49363  gpg5edgnedg  49433  0nodd  49472  0even  49539  2even  49541  2zrngamgm  49547  2t6m3t4e0  49665  linevalexample  49712  zlmodzxzequap  49816  pw2m1lepw2m1  49837  nnlog2ge0lt1  49883  logbpw2m1  49884  nnpw2blen  49897  nnpw2pmod  49900  blen1  49901  blen2  49902  blennnt2  49906  nnolog2flm1  49907  0dig2nn0e  49929  0dig2nn0o  49930  nn0sumshdiglemA  49936  nn0sumshdiglemB  49937  nn0sumshdiglem1  49938  nn0sumshdiglem2  49939  ackval1012  50007  ackval2012  50008  ackval3012  50009  ackval42  50013  sinhpcosh  51113