Theorem 2cn 12254

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 12242	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11094	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11149	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2836	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   + caddc 11039  2c2 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815  df-2 12242

This theorem is referenced by:  2ex  12256  2cnd  12257  3cn  12260  2m1e1  12300  3m1e2  12302  2p2e4  12309  times2  12311  2div2e1  12315  1p2e3ALT  12318  3p3e6  12326  4p3e7  12328  5p3e8  12331  6p3e9  12334  2t1e2  12337  2t2e4  12338  3t3e9  12341  2t0e0  12343  4div2e2  12344  2cnne0  12384  halfcn  12389  2halves  12393  8th4div3  12395  halfthird  12396  halfpm6th  12397  2mulicn  12399  2muline0  12400  halfcl  12401  half0  12403  halfaddsub  12408  div4p1lem1div2  12430  3halfnz  12606  zneo  12610  nneo  12611  zeo  12613  7p3e10  12717  4t4e16  12741  6t3e18  12747  7t7e49  12756  8t5e40  12760  9t9e81  12771  decbin0  12782  decbin2  12783  fztpval  13538  fz0tp  13580  fzo0to3tp  13705  fzo1to4tp  13707  expubnd  14138  sq2  14157  sq4e2t8  14159  cu2  14160  subsq2  14171  binom2sub  14180  binom3  14184  zesq  14186  fac2  14239  fac3  14240  faclbnd2  14251  faclbnd4lem1  14253  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd5  14258  bcn2  14279  4bc2eq6  14289  swrd2lsw  14912  crre  15074  addcj  15108  imval2  15111  01sqrexlem7  15208  absmax  15290  rddif  15301  sqreulem  15320  amgm2  15330  abs3lemi  15371  iseraltlem2  15643  ackbijnn  15791  climcndslem1  15812  climcndslem2  15813  arisum  15823  arisum2  15824  geo2sum2  15837  geo2lim  15838  geoihalfsum  15845  bpoly2  16020  bpoly3  16021  bpoly4  16022  fsumcube  16023  efcllem  16040  ege2le3  16053  efgt0  16068  tanval2  16098  tanval3  16099  efi4p  16102  efival  16117  sinadd  16129  cosadd  16130  sinmul  16137  cos2tsin  16144  ef01bndlem  16149  cos01bnd  16151  cos1bnd  16152  cos2bnd  16153  cos01gt0  16156  sin02gt0  16157  sin4lt0  16160  odd2np1lem  16307  odd2np1  16308  opoe  16330  omoe  16331  opeo  16332  omeo  16333  nno  16349  nn0o  16350  flodddiv4  16382  bits0  16395  bitsfzolem  16401  0bits  16406  bitsinv1  16409  sadcadd  16425  smumullem  16459  6gcd4e2  16505  3lcm2e6woprm  16582  6lcm4e12  16583  pythagtriplem1  16785  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem15  16798  pythagtriplem16  16799  pythagtriplem17  16800  iserodd  16804  prmreclem5  16889  prmreclem6  16890  4sqlem11  16924  4sqlem12  16925  prmo2  17009  prmo3  17010  dec5dvds  17033  dec2nprm  17036  2exp5  17054  2exp6  17055  2exp7  17056  2exp8  17057  2exp11  17058  2exp16  17059  7prm  17079  11prm  17083  13prm  17084  37prm  17089  43prm  17090  83prm  17091  139prm  17092  163prm  17093  317prm  17094  631prm  17095  1259lem1  17099  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  1259prm  17104  2503lem1  17105  2503lem2  17106  2503lem3  17107  4001lem1  17109  4001lem2  17110  4001lem3  17111  4001lem4  17112  4001prm  17113  psgnunilem2  19468  efgtlen  19699  efgredleme  19716  frgpnabllem1  19846  lt6abl  19868  htpycc  24972  pcoval2  25008  pcocn  25009  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  csbren  25391  minveclem2  25418  ovolunlem1a  25488  ovolunlem1  25489  vitalilem4  25603  mbfi1fseqlem5  25711  dvmptre  25961  dvsincos  25973  aaliou3lem2  26334  aaliou3lem3  26335  aaliou3lem8  26336  coscn  26435  sinhalfpilem  26452  cospi  26461  ef2pi  26466  ef2kpi  26467  efper  26468  sinperlem  26469  sin2kpi  26472  cos2kpi  26473  sin2pim  26474  cos2pim  26475  sincosq3sgn  26489  sincosq4sgn  26490  tangtx  26494  sinq12gt0  26496  sincosq1eq  26501  sincos4thpi  26502  sincos6thpi  26505  sincos3rdpi  26506  pige3ALT  26509  abssinper  26510  coskpi  26512  sineq0  26513  coseq1  26514  efeq1  26517  efif1olem4  26534  eflogeq  26591  tanarg  26608  cxpsqrtlem  26691  cxpsqrt  26692  logsqrt  26693  2irrexpq  26720  root1eq1  26744  cxpeq  26746  2logb9irrALT  26787  sqrt2cxp2logb9e3  26788  ang180lem2  26799  ang180lem3  26800  quad2  26828  1cubrlem  26830  1cubr  26831  dcubic2  26833  dcubic1  26834  dcubic  26835  mcubic  26836  cubic2  26837  cubic  26838  dquartlem1  26840  dquartlem2  26841  dquart  26842  quart1lem  26844  quart1  26845  quartlem1  26846  quartlem2  26847  quartlem3  26848  quart  26850  sinasin  26878  asinsin  26881  atancj  26899  efiatan  26901  efiatan2  26906  2efiatan  26907  tanatan  26908  atantan  26912  atanbndlem  26914  atans2  26920  dvatan  26924  atantayl2  26927  leibpilem2  26930  log2cnv  26933  log2tlbnd  26934  log2ublem2  26936  log2ublem3  26937  log2ub  26938  birthday  26943  zetacvg  27003  basellem1  27069  basellem3  27071  basellem8  27076  basellem9  27077  cht3  27161  1sgm2ppw  27188  ppiub  27192  chtublem  27199  chtub  27200  perfect1  27216  perfectlem1  27217  perfectlem2  27218  perfect  27219  bcmax  27266  bcp1ctr  27267  bclbnd  27268  bpos1lem  27270  bpos1  27271  bposlem1  27272  bposlem2  27273  bposlem4  27275  bposlem5  27276  bposlem6  27277  bposlem8  27279  bposlem9  27280  lgsdir2lem2  27314  gausslemma2dlem6  27360  lgsquadlem1  27368  lgsquadlem2  27369  lgsquad2lem2  27373  m1lgs  27376  2lgslem3a  27384  2lgslem3b  27385  2lgslem3c  27386  2lgslem3d  27387  2lgsoddprmlem2  27397  2lgsoddprmlem3c  27400  2lgsoddprmlem3d  27401  addsqnreup  27431  addsq2nreurex  27432  rplogsumlem1  27472  dchrisum0fno1  27499  dchrisum0lem1  27504  dchrisum0lem2  27506  logdivsum  27521  mulog2sumlem3  27524  log2sumbnd  27532  selberglem1  27533  selberglem2  27534  selberg2  27539  selberg4lem1  27548  selberg3r  27557  pntpbnd1a  27573  pntpbnd2  27575  pntibndlem2  27579  pntlemk  27594  ax5seglem7  29029  axlowdimlem13  29048  elwspths2spth  30063  clwlkclwwlklem2a4  30092  clwwlknonex2  30204  2clwwlk2  30443  numclwlk1lem1  30464  ex-fl  30542  ex-ceil  30543  ex-exp  30545  ex-fac  30546  ex-abs  30550  ex-ind-dvds  30556  ipidsq  30806  cncph  30915  ip0i  30921  ip1ilem  30922  ipdirilem  30925  minvecolem2  30971  hvsubcan2i  31160  norm-ii-i  31233  norm3lem  31245  normpar2i  31252  polid2i  31253  hhph  31274  mayete3i  31824  nmcexi  32122  opsqrlem6  32241  addltmulALT  32542  ply1dg3rt0irred  33674  fldext2chn  33919  constrelextdg2  33938  2sqr3minply  33971  cos9thpiminplylem4  33976  cos9thpiminplylem5  33977  omssubadd  34491  oddpwdc  34545  fib5  34596  ballotlem2  34680  ballotth  34729  efmul2picn  34787  itgexpif  34797  vtscl  34829  circlemeth  34831  hgt750lemd  34839  logdivsqrle  34841  hgt750lem  34842  hgt750lem2  34843  problem4  35903  problem5  35904  quad3  35905  cnndvlem1  36850  sin2h  37984  cos2h  37985  tan2h  37986  poimirlem29  38023  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  itg2addnclem3  38047  dvasin  38078  areacirc  38087  heiborlem6  38190  12gcd5e1  42495  12lcm5e60  42500  60lcm7e420  42502  420lcm8e840  42503  3exp7  42545  3lexlogpow5ineq1  42546  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1p1p5  42567  aks4d1p1  42568  posbezout  42592  facp2  42635  1p3e4  42749  sqn5i  42769  235t711  42789  ex-decpmul  42790  cxp112d  42825  cxp111d  42826  cxpi11d  42827  tanhalfpim  42833  fltne  43101  flt4lem5e  43113  sum9cubes  43129  3cubeslem3l  43142  3cubeslem3r  43143  rmxluc  43388  rmyluc  43389  jm2.17a  43412  jm2.18  43440  jm2.23  43448  jm3.1lem1  43469  proot1ex  43648  areaquad  43668  sqrtcval  44092  resqrtvalex  44096  lhe4.4ex1a  44780  sineq0ALT  45387  coskpi2  46316  cosnegpi  46317  cosknegpi  46319  stoweidlem26  46476  wallispilem4  46518  wallispi  46520  wallispi2lem1  46521  stirlinglem8  46531  dirkerper  46546  dirkertrigeqlem3  46550  dirkertrigeq  46551  dirkeritg  46552  dirkercncflem1  46553  dirkercncflem2  46554  fourierdlem57  46613  fourierdlem58  46614  fourierdlem62  46618  fourierdlem76  46632  fourierdlem103  46659  fourierdlem104  46660  sqwvfourb  46679  fourierswlem  46680  nthrucw  47338  sin5tlem1  47343  sin5tlem5  47347  cos5t  47349  goldrasin  47352  goldracos5teq  47355  goldratmolem2  47356  rehalfge1  47809  ceil5half3  47816  modm2nep1  47842  modm1nep2  47844  modm1nem2  47845  fmtnoge3  48015  fmtnorec1  48022  fmtno0  48025  fmtno1  48026  fmtnorec3  48033  fmtnorec4  48034  fmtno5lem2  48039  fmtno5lem4  48041  257prm  48046  fmtnoprmfac2lem1  48051  fmtno4prmfac  48057  fmtno5faclem2  48065  fmtno5faclem3  48066  fmtno5fac  48067  139prmALT  48081  31prm  48082  127prm  48084  mod42tp1mod8  48087  lighneallem2  48091  lighneallem3  48092  lighneallem4a  48093  3exp4mod41  48101  41prothprmlem1  48102  41prothprmlem2  48103  41prothprm  48104  bits0ALTV  48177  0evenALTV  48186  6even  48209  8even  48211  perfectALTVlem1  48219  perfectALTVlem2  48220  perfectALTV  48221  2exp340mod341  48231  8exp8mod9  48234  mogoldbb  48283  nnsum3primes4  48286  bgoldbtbndlem1  48303  gpg5order  48558  gpg5edgnedg  48628  0nodd  48668  0even  48735  2even  48737  2zrngamgm  48743  2t6m3t4e0  48846  linevalexample  48893  zlmodzxzequap  48997  pw2m1lepw2m1  49018  nnlog2ge0lt1  49064  logbpw2m1  49065  nnpw2blen  49078  nnpw2pmod  49081  blen1  49082  blen2  49083  blennnt2  49087  nnolog2flm1  49088  0dig2nn0e  49110  0dig2nn0o  49111  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  nn0sumshdiglem1  49119  nn0sumshdiglem2  49120  ackval1012  49188  ackval2012  49189  ackval3012  49190  ackval42  49194  sinhpcosh  50237