Theorem 2cn 12307

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 12294	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11146	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11203	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2861	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   + caddc 11091  2c2 12286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-2 12294

This theorem is referenced by:  2ex  12309  2cnd  12310  3cn  12313  2thalfe1  12339  2m1e1OLD  12357  3m1e2  12359  2p2e4  12366  times2  12368  2div2e1  12372  1p2e3ALT  12375  3p3e6  12383  4p3e7  12385  5p3e8  12388  6p3e9  12391  2t1e2  12394  2t2e4  12395  2t3e6  12398  3t3e9  12399  2t4e8  12401  2t0e0  12402  4div2e2  12403  2cnne0  12444  halfcn  12449  2halves  12453  8th4div3  12455  halfthird  12456  halfpm6th  12457  2mulicn  12459  2muline0  12460  halfcl  12461  half0  12463  halfaddsub  12468  div4p1lem1div2  12490  3halfnz  12666  zneo  12670  nneo  12671  zeo  12673  7p3e10  12782  4t4e16  12806  6t3e18  12812  7t7e49  12821  8t5e40  12825  9t9e81  12836  decbin0  12849  decbin2  12850  fztpval  13605  fz0tp  13647  fzo0to3tp  13772  fzo1to4tp  13774  expubnd  14205  sq2  14224  sq4e2t8  14226  cu2  14227  subsq2  14238  binom2sub  14247  binom3  14251  zesq  14253  fac2  14306  fac3  14307  faclbnd2  14318  faclbnd4lem1  14320  faclbnd4lem3  14322  faclbnd4lem4  14323  faclbnd5  14325  bcn2  14346  4bc2eq6  14356  swrd2lsw  14979  crre  15155  addcj  15189  imval2  15192  01sqrexlem7  15289  absmax  15371  rddif  15382  sqreulem  15401  amgm2  15411  abs3lemi  15452  iseraltlem2  15724  ackbijnn  15872  climcndslem1  15893  climcndslem2  15894  arisum  15904  arisum2  15905  geo2sum2  15918  geo2lim  15919  geoihalfsum  15926  bpoly2  16101  bpoly3  16102  bpoly4  16103  fsumcube  16104  efcllem  16121  ege2le3  16134  efgt0  16149  tanval2  16179  tanval3  16180  efi4p  16183  efival  16198  sinadd  16210  cosadd  16211  sinmul  16218  cos2tsin  16225  ef01bndlem  16230  cos01bnd  16232  cos1bnd  16233  cos2bnd  16234  cos01gt0  16237  sin02gt0  16238  sin4lt0  16241  odd2np1lem  16388  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  nno  16430  nn0o  16431  flodddiv4  16463  bits0  16476  bitsfzolem  16482  0bits  16487  bitsinv1  16490  sadcadd  16506  smumullem  16540  6gcd4e2  16586  3lcm2e6woprm  16663  6lcm4e12  16664  pythagtriplem1  16866  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem15  16879  pythagtriplem16  16880  pythagtriplem17  16881  iserodd  16885  prmreclem5  16970  prmreclem6  16971  4sqlem11  17005  4sqlem12  17006  prmo2  17090  prmo3  17091  dec5dvds  17114  dec2nprm  17117  2exp5  17135  2exp6  17136  2exp7  17137  2exp8  17138  2exp11  17139  2exp16  17140  7prm  17160  10nprm  17163  11prm  17165  13prm  17166  37prm  17171  43prm  17172  83prm  17173  139prm  17174  163prm  17175  317prm  17176  631prm  17177  1259lem1  17181  1259lem2  17182  1259lem3  17183  1259lem4  17184  1259lem5  17185  1259prm  17186  2503lem1  17187  2503lem2  17188  2503lem3  17189  4001lem1  17191  4001lem2  17192  4001lem3  17193  4001lem4  17194  4001prm  17195  psgnunilem2  19556  efgtlen  19787  efgredleme  19804  frgpnabllem1  19934  lt6abl  19956  pcoval2  25136  pcocn  25137  pcohtpylem  25139  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  csbren  25519  minveclem2  25546  ovolunlem1a  25616  ovolunlem1  25617  vitalilem4  25731  mbfi1fseqlem5  25839  dvmptre  26089  dvsincos  26101  aaliou3lem2  26465  aaliou3lem3  26466  aaliou3lem8  26467  coscn  26566  2picn  26580  sinhalfpilem  26586  cospi  26595  ef2pi  26600  ef2kpi  26601  efper  26602  sinperlem  26603  sin2kpi  26606  cos2kpi  26607  sin2pim  26608  cos2pim  26609  sincosq3sgn  26623  sincosq4sgn  26624  tangtx  26628  sinq12gt0  26630  sincosq1eq  26635  sincos4thpi  26636  sincos6thpi  26639  sincos3rdpi  26640  pige3ALT  26643  abssinper  26644  coskpi  26646  sineq0  26647  coseq1  26648  efeq1  26651  efif1olem4  26668  eflogeq  26725  tanarg  26742  cxpsqrtlem  26825  cxpsqrt  26826  logsqrt  26827  2irrexpq  26854  root1eq1  26878  cxpeq  26880  2logb9irrALT  26921  sqrt2cxp2logb9e3  26922  ang180lem2  26933  ang180lem3  26934  quad2  26962  1cubrlem  26964  1cubr  26965  dcubic2  26967  dcubic1  26968  dcubic  26969  mcubic  26970  cubic2  26971  cubic  26972  dquartlem1  26974  dquartlem2  26975  dquart  26976  quart1lem  26978  quart1  26979  quartlem1  26980  quartlem2  26981  quartlem3  26982  quart  26984  sinasin  27012  asinsin  27015  atancj  27033  efiatan  27035  efiatan2  27040  2efiatan  27041  tanatan  27042  atantan  27046  atanbndlem  27048  atans2  27054  dvatan  27058  atantayl2  27061  leibpilem2  27064  log2cnv  27067  log2tlbnd  27068  log2ublem2  27070  log2ublem3  27071  log2ub  27072  birthday  27077  zetacvg  27137  basellem1  27203  basellem3  27205  basellem8  27210  basellem9  27211  1sgm2ppw  27322  ppiub  27326  chtublem  27333  chtub  27334  perfect1  27350  perfectlem1  27351  perfectlem2  27352  perfect  27353  bcmax  27400  bcp1ctr  27401  bclbnd  27402  bpos1lem  27404  bpos1  27405  bposlem1  27406  bposlem2  27407  bposlem4  27409  bposlem5  27410  bposlem6  27411  bposlem8  27413  bposlem9  27414  lgsdir2lem2  27448  gausslemma2dlem6  27494  lgsquadlem1  27502  lgsquadlem2  27503  lgsquad2lem2  27507  m1lgs  27510  2lgslem3a  27518  2lgslem3b  27519  2lgslem3c  27520  2lgslem3d  27521  2lgsoddprmlem2  27531  2lgsoddprmlem3c  27534  2lgsoddprmlem3d  27535  addsqnreup  27565  addsq2nreurex  27566  rplogsumlem1  27606  dchrisum0fno1  27633  dchrisum0lem1  27638  dchrisum0lem2  27640  logdivsum  27655  mulog2sumlem3  27658  log2sumbnd  27666  selberglem1  27667  selberglem2  27668  selberg2  27673  selberg4lem1  27682  selberg3r  27691  pntpbnd1a  27707  pntpbnd2  27709  pntibndlem2  27713  pntlemk  27728  ax5seglem7  29194  axlowdimlem13  29213  elwspths2spth  30228  clwlkclwwlklem2a4  30257  clwwlknonex2  30369  2clwwlk2  30608  numclwlk1lem1  30629  ex-fl  30707  ex-ceil  30708  ex-exp  30710  ex-fac  30711  ex-abs  30715  ex-ind-dvds  30721  ipidsq  30971  cncph  31080  ip0i  31086  ip1ilem  31087  ipdirilem  31090  minvecolem2  31136  hvsubcan2i  31325  norm-ii-i  31398  norm3lem  31410  normpar2i  31417  polid2i  31418  hhph  31439  mayete3i  31989  nmcexi  32287  opsqrlem6  32406  addltmulALT  32707  ply1dg3rt0irred  33791  fldext2chn  34035  constrelextdg2  34054  2sqr3minply  34087  cos9thpiminplylem4  34092  cos9thpiminplylem5  34093  omssubadd  34607  oddpwdc  34661  fib5  34712  ballotlem2  34796  ballotth  34845  efmul2picn  34900  itgexpif  34910  vtscl  34942  circlemeth  34944  hgt750lemd  34952  logdivsqrle  34954  hgt750lem  34955  hgt750lem2  34956  problem4  36031  problem5  36032  quad3  36033  cnndvlem1  36988  sin2h  38121  cos2h  38122  tan2h  38123  poimirlem29  38160  mblfinlem1  38168  mblfinlem2  38169  mblfinlem3  38170  itg2addnclem3  38184  dvasin  38215  areacirc  38224  heiborlem6  38327  12gcd5e1  42632  12lcm5e60  42637  60lcm7e420  42639  420lcm8e840  42640  3exp7  42682  3lexlogpow5ineq1  42683  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1p1p5  42704  aks4d1p1  42705  posbezout  42729  facp2  42772  1p3e4  42886  sqn5i  42906  235t711  42926  ex-decpmul  42927  cxp112d  42962  cxp111d  42963  cxpi11d  42964  tanhalfpim  42970  fltne  43238  flt4lem5e  43250  sum9cubes  43266  3cubeslem3l  43279  3cubeslem3r  43280  rmxluc  43525  rmyluc  43526  jm2.17a  43549  jm2.18  43577  jm2.23  43585  jm3.1lem1  43606  proot1ex  43785  areaquad  43805  sqrtcval  44229  resqrtvalex  44233  lhe4.4ex1a  44903  sineq0ALT  45510  coskpi2  46438  cosnegpi  46439  cosknegpi  46441  stoweidlem26  46598  wallispilem4  46640  wallispi  46642  wallispi2lem1  46643  stirlinglem8  46653  dirkerper  46668  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkeritg  46674  dirkercncflem1  46675  fourierdlem57  46735  fourierdlem58  46736  fourierdlem62  46740  fourierdlem76  46754  fourierdlem103  46781  fourierdlem104  46782  sqwvfourb  46801  fourierswlem  46802  nthrucw  47460  sin5tlem1  47465  sin5tlem5  47469  cos5t  47471  goldrasin  47474  goldracos5teq  47477  goldratmolem2  47478  rehalfge1  47931  ceil5half3  47938  modm2nep1  47964  modm1nep2  47966  modm1nem2  47967  fmtnoge3  48137  fmtnorec1  48144  fmtno0  48147  fmtno1  48148  fmtnorec3  48155  fmtnorec4  48156  fmtno5lem2  48161  fmtno5lem4  48163  257prm  48168  fmtnoprmfac2lem1  48173  fmtno4prmfac  48179  fmtno5faclem2  48187  fmtno5faclem3  48188  fmtno5fac  48189  139prmALT  48203  31prm  48204  127prm  48206  lighneallem2  48213  lighneallem3  48214  lighneallem4a  48215  3exp4mod41  48223  41prothprmlem1  48224  41prothprmlem2  48225  41prothprm  48226  bits0ALTV  48299  0evenALTV  48308  6even  48331  8even  48333  perfectALTVlem1  48341  perfectALTVlem2  48342  perfectALTV  48343  2exp340mod341  48353  8exp8mod9  48356  mogoldbb  48405  nnsum3primes4  48408  bgoldbtbndlem1  48425  gpg5order  48680  gpg5edgnedg  48750  0nodd  48790  0even  48857  2even  48859  2zrngamgm  48865  2t6m3t4e0  48979  linevalexample  49026  zlmodzxzequap  49130  pw2m1lepw2m1  49151  nnlog2ge0lt1  49197  logbpw2m1  49198  nnpw2blen  49211  nnpw2pmod  49214  blen1  49215  blen2  49216  blennnt2  49220  nnolog2flm1  49221  0dig2nn0e  49243  0dig2nn0o  49244  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  nn0sumshdiglem1  49252  nn0sumshdiglem2  49253  ackval1012  49321  ackval2012  49322  ackval3012  49323  ackval42  49327  sinhpcosh  50369