Theorem 2cn 12290

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 12277	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11128	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11185	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2857	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   + caddc 11073  2c2 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-addcl 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-2 12277

This theorem is referenced by:  2ex  12292  2cnd  12293  3cn  12296  2thalfe1  12322  2m1e1OLD  12340  3m1e2  12342  2p2e4  12349  times2  12351  2div2e1  12355  1p2e3ALT  12358  3p3e6  12366  4p3e7  12368  5p3e8  12371  6p3e9  12374  2t1e2  12377  2t2e4  12378  2t3e6  12381  3t3e9  12382  2t4e8  12384  2t0e0  12385  4div2e2  12386  2cnne0  12427  halfcn  12432  2halves  12436  8th4div3  12438  halfthird  12439  halfpm6th  12440  2mulicn  12442  2muline0  12443  halfcl  12444  half0  12446  halfaddsub  12451  div4p1lem1div2  12473  3halfnz  12649  zneo  12653  nneo  12654  zeo  12656  7p3e10  12765  4t4e16  12789  6t3e18  12795  7t7e49  12804  8t5e40  12808  9t9e81  12819  decbin0  12832  decbin2  12833  fztpval  13588  fz0tp  13630  fzo0to3tp  13755  fzo1to4tp  13757  expubnd  14188  sq2  14207  sq4e2t8  14209  cu2  14210  subsq2  14221  binom2sub  14230  binom3  14234  zesq  14236  fac2  14289  fac3  14290  faclbnd2  14301  faclbnd4lem1  14303  faclbnd4lem3  14305  faclbnd4lem4  14306  faclbnd5  14308  bcn2  14329  4bc2eq6  14339  swrd2lsw  14962  crre  15124  addcj  15158  imval2  15161  01sqrexlem7  15258  absmax  15340  rddif  15351  sqreulem  15370  amgm2  15380  abs3lemi  15421  iseraltlem2  15693  ackbijnn  15841  climcndslem1  15862  climcndslem2  15863  arisum  15873  arisum2  15874  geo2sum2  15887  geo2lim  15888  geoihalfsum  15895  bpoly2  16070  bpoly3  16071  bpoly4  16072  fsumcube  16073  efcllem  16090  ege2le3  16103  efgt0  16118  tanval2  16148  tanval3  16149  efi4p  16152  efival  16167  sinadd  16179  cosadd  16180  sinmul  16187  cos2tsin  16194  ef01bndlem  16199  cos01bnd  16201  cos1bnd  16202  cos2bnd  16203  cos01gt0  16206  sin02gt0  16207  sin4lt0  16210  odd2np1lem  16357  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  nno  16399  nn0o  16400  flodddiv4  16432  bits0  16445  bitsfzolem  16451  0bits  16456  bitsinv1  16459  sadcadd  16475  smumullem  16509  6gcd4e2  16555  3lcm2e6woprm  16632  6lcm4e12  16633  pythagtriplem1  16835  pythagtriplem12  16845  pythagtriplem14  16847  pythagtriplem15  16848  pythagtriplem16  16849  pythagtriplem17  16850  iserodd  16854  prmreclem5  16939  prmreclem6  16940  4sqlem11  16974  4sqlem12  16975  prmo2  17059  prmo3  17060  dec5dvds  17083  dec2nprm  17086  2exp5  17104  2exp6  17105  2exp7  17106  2exp8  17107  2exp11  17108  2exp16  17109  7prm  17129  10nprm  17132  11prm  17134  13prm  17135  37prm  17140  43prm  17141  83prm  17142  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  1259prm  17155  2503lem1  17156  2503lem2  17157  2503lem3  17158  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  4001prm  17164  psgnunilem2  19518  efgtlen  19749  efgredleme  19766  frgpnabllem1  19896  lt6abl  19918  pcoval2  25058  pcocn  25059  pcohtpylem  25061  pcopt  25064  pcopt2  25065  pcoass  25066  pcorevlem  25068  csbren  25441  minveclem2  25468  ovolunlem1a  25538  ovolunlem1  25539  vitalilem4  25653  mbfi1fseqlem5  25761  dvmptre  26011  dvsincos  26023  aaliou3lem2  26384  aaliou3lem3  26385  aaliou3lem8  26386  coscn  26485  2picn  26499  sinhalfpilem  26505  cospi  26514  ef2pi  26519  ef2kpi  26520  efper  26521  sinperlem  26522  sin2kpi  26525  cos2kpi  26526  sin2pim  26527  cos2pim  26528  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sinq12gt0  26549  sincosq1eq  26554  sincos4thpi  26555  sincos6thpi  26558  sincos3rdpi  26559  pige3ALT  26562  abssinper  26563  coskpi  26565  sineq0  26566  coseq1  26567  efeq1  26570  efif1olem4  26587  eflogeq  26644  tanarg  26661  cxpsqrtlem  26744  cxpsqrt  26745  logsqrt  26746  2irrexpq  26773  root1eq1  26797  cxpeq  26799  2logb9irrALT  26840  sqrt2cxp2logb9e3  26841  ang180lem2  26852  ang180lem3  26853  quad2  26881  1cubrlem  26883  1cubr  26884  dcubic2  26886  dcubic1  26887  dcubic  26888  mcubic  26889  cubic2  26890  cubic  26891  dquartlem1  26893  dquartlem2  26894  dquart  26895  quart1lem  26897  quart1  26898  quartlem1  26899  quartlem2  26900  quartlem3  26901  quart  26903  sinasin  26931  asinsin  26934  atancj  26952  efiatan  26954  efiatan2  26959  2efiatan  26960  tanatan  26961  atantan  26965  atanbndlem  26967  atans2  26973  dvatan  26977  atantayl2  26980  leibpilem2  26983  log2cnv  26986  log2tlbnd  26987  log2ublem2  26989  log2ublem3  26990  log2ub  26991  birthday  26996  zetacvg  27056  basellem1  27122  basellem3  27124  basellem8  27129  basellem9  27130  1sgm2ppw  27241  ppiub  27245  chtublem  27252  chtub  27253  perfect1  27269  perfectlem1  27270  perfectlem2  27271  perfect  27272  bcmax  27319  bcp1ctr  27320  bclbnd  27321  bpos1lem  27323  bpos1  27324  bposlem1  27325  bposlem2  27326  bposlem4  27328  bposlem5  27329  bposlem6  27330  bposlem8  27332  bposlem9  27333  lgsdir2lem2  27367  gausslemma2dlem6  27413  lgsquadlem1  27421  lgsquadlem2  27422  lgsquad2lem2  27426  m1lgs  27429  2lgslem3a  27437  2lgslem3b  27438  2lgslem3c  27439  2lgslem3d  27440  2lgsoddprmlem2  27450  2lgsoddprmlem3c  27453  2lgsoddprmlem3d  27454  addsqnreup  27484  addsq2nreurex  27485  rplogsumlem1  27525  dchrisum0fno1  27552  dchrisum0lem1  27557  dchrisum0lem2  27559  logdivsum  27574  mulog2sumlem3  27577  log2sumbnd  27585  selberglem1  27586  selberglem2  27587  selberg2  27592  selberg4lem1  27601  selberg3r  27610  pntpbnd1a  27626  pntpbnd2  27628  pntibndlem2  27632  pntlemk  27647  ax5seglem7  29082  axlowdimlem13  29101  elwspths2spth  30116  clwlkclwwlklem2a4  30145  clwwlknonex2  30257  2clwwlk2  30496  numclwlk1lem1  30517  ex-fl  30595  ex-ceil  30596  ex-exp  30598  ex-fac  30599  ex-abs  30603  ex-ind-dvds  30609  ipidsq  30859  cncph  30968  ip0i  30974  ip1ilem  30975  ipdirilem  30978  minvecolem2  31024  hvsubcan2i  31213  norm-ii-i  31286  norm3lem  31298  normpar2i  31305  polid2i  31306  hhph  31327  mayete3i  31877  nmcexi  32175  opsqrlem6  32294  addltmulALT  32595  ply1dg3rt0irred  33741  fldext2chn  33986  constrelextdg2  34005  2sqr3minply  34038  cos9thpiminplylem4  34043  cos9thpiminplylem5  34044  omssubadd  34558  oddpwdc  34612  fib5  34663  ballotlem2  34747  ballotth  34796  efmul2picn  34854  itgexpif  34864  vtscl  34896  circlemeth  34898  hgt750lemd  34906  logdivsqrle  34908  hgt750lem  34909  hgt750lem2  34910  problem4  35982  problem5  35983  quad3  35984  cnndvlem1  36939  sin2h  38073  cos2h  38074  tan2h  38075  poimirlem29  38112  mblfinlem1  38120  mblfinlem2  38121  mblfinlem3  38122  itg2addnclem3  38136  dvasin  38167  areacirc  38176  heiborlem6  38279  12gcd5e1  42584  12lcm5e60  42589  60lcm7e420  42591  420lcm8e840  42592  3exp7  42634  3lexlogpow5ineq1  42635  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1p1p5  42656  aks4d1p1  42657  posbezout  42681  facp2  42724  1p3e4  42838  sqn5i  42858  235t711  42878  ex-decpmul  42879  cxp112d  42914  cxp111d  42915  cxpi11d  42916  tanhalfpim  42922  fltne  43190  flt4lem5e  43202  sum9cubes  43218  3cubeslem3l  43231  3cubeslem3r  43232  rmxluc  43477  rmyluc  43478  jm2.17a  43501  jm2.18  43529  jm2.23  43537  jm3.1lem1  43558  proot1ex  43737  areaquad  43757  sqrtcval  44181  resqrtvalex  44185  lhe4.4ex1a  44869  sineq0ALT  45476  coskpi2  46404  cosnegpi  46405  cosknegpi  46407  stoweidlem26  46564  wallispilem4  46606  wallispi  46608  wallispi2lem1  46609  stirlinglem8  46619  dirkerper  46634  dirkertrigeqlem3  46638  dirkertrigeq  46639  dirkeritg  46640  dirkercncflem1  46641  fourierdlem57  46701  fourierdlem58  46702  fourierdlem62  46706  fourierdlem76  46720  fourierdlem103  46747  fourierdlem104  46748  sqwvfourb  46767  fourierswlem  46768  nthrucw  47426  sin5tlem1  47431  sin5tlem5  47435  cos5t  47437  goldrasin  47440  goldracos5teq  47443  goldratmolem2  47444  rehalfge1  47897  ceil5half3  47904  modm2nep1  47930  modm1nep2  47932  modm1nem2  47933  fmtnoge3  48103  fmtnorec1  48110  fmtno0  48113  fmtno1  48114  fmtnorec3  48121  fmtnorec4  48122  fmtno5lem2  48127  fmtno5lem4  48129  257prm  48134  fmtnoprmfac2lem1  48139  fmtno4prmfac  48145  fmtno5faclem2  48153  fmtno5faclem3  48154  fmtno5fac  48155  139prmALT  48169  31prm  48170  127prm  48172  lighneallem2  48179  lighneallem3  48180  lighneallem4a  48181  3exp4mod41  48189  41prothprmlem1  48190  41prothprmlem2  48191  41prothprm  48192  bits0ALTV  48265  0evenALTV  48274  6even  48297  8even  48299  perfectALTVlem1  48307  perfectALTVlem2  48308  perfectALTV  48309  2exp340mod341  48319  8exp8mod9  48322  mogoldbb  48371  nnsum3primes4  48374  bgoldbtbndlem1  48391  gpg5order  48646  gpg5edgnedg  48716  0nodd  48756  0even  48823  2even  48825  2zrngamgm  48831  2t6m3t4e0  48934  linevalexample  48981  zlmodzxzequap  49085  pw2m1lepw2m1  49106  nnlog2ge0lt1  49152  logbpw2m1  49153  nnpw2blen  49166  nnpw2pmod  49169  blen1  49170  blen2  49171  blennnt2  49175  nnolog2flm1  49176  0dig2nn0e  49198  0dig2nn0o  49199  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  nn0sumshdiglem1  49207  nn0sumshdiglem2  49208  ackval1012  49276  ackval2012  49277  ackval3012  49278  ackval42  49282  sinhpcosh  50325