Theorem 2cn 12197

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 12185	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11061	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11115	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2827	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001  1c1 11004   + caddc 11006  2c2 12177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-addcl 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12185

This theorem is referenced by:  2ex  12199  2cnd  12200  3cn  12203  2m1e1  12243  3m1e2  12245  2p2e4  12252  times2  12254  2div2e1  12258  1p2e3ALT  12261  3p3e6  12269  4p3e7  12271  5p3e8  12274  6p3e9  12277  2t1e2  12280  2t2e4  12281  3t3e9  12284  2t0e0  12286  4d2e2  12287  2cnne0  12327  halfcn  12332  2halves  12336  8th4div3  12338  halfthird  12339  halfpm6th  12340  2mulicn  12342  2muline0  12343  halfcl  12344  half0  12346  halfaddsub  12351  div4p1lem1div2  12373  3halfnz  12549  zneo  12553  nneo  12554  zeo  12556  7p3e10  12660  4t4e16  12684  6t3e18  12690  7t7e49  12699  8t5e40  12703  9t9e81  12714  decbin0  12725  decbin2  12726  fztpval  13483  fz0tp  13525  fzo0to3tp  13649  fzo1to4tp  13651  expubnd  14082  sq2  14101  sq4e2t8  14103  cu2  14104  subsq2  14115  binom2sub  14124  binom3  14128  zesq  14130  fac2  14183  fac3  14184  faclbnd2  14195  faclbnd4lem1  14197  faclbnd4lem3  14199  faclbnd4lem4  14200  faclbnd5  14202  bcn2  14223  4bc2eq6  14233  swrd2lsw  14856  crre  15018  addcj  15052  imval2  15055  01sqrexlem7  15152  absmax  15234  rddif  15245  sqreulem  15264  amgm2  15274  abs3lemi  15315  iseraltlem2  15587  ackbijnn  15732  climcndslem1  15753  climcndslem2  15754  arisum  15764  arisum2  15765  geo2sum2  15778  geo2lim  15779  geoihalfsum  15786  bpoly2  15961  bpoly3  15962  bpoly4  15963  fsumcube  15964  efcllem  15981  ege2le3  15994  efgt0  16009  tanval2  16039  tanval3  16040  efi4p  16043  efival  16058  sinadd  16070  cosadd  16071  sinmul  16078  cos2tsin  16085  ef01bndlem  16090  cos01bnd  16092  cos1bnd  16093  cos2bnd  16094  cos01gt0  16097  sin02gt0  16098  sin4lt0  16101  odd2np1lem  16248  odd2np1  16249  opoe  16271  omoe  16272  opeo  16273  omeo  16274  nno  16290  nn0o  16291  flodddiv4  16323  bits0  16336  bitsfzolem  16342  0bits  16347  bitsinv1  16350  sadcadd  16366  smumullem  16400  6gcd4e2  16446  3lcm2e6woprm  16523  6lcm4e12  16524  pythagtriplem1  16725  pythagtriplem12  16735  pythagtriplem14  16737  pythagtriplem15  16738  pythagtriplem16  16739  pythagtriplem17  16740  iserodd  16744  prmreclem5  16829  prmreclem6  16830  4sqlem11  16864  4sqlem12  16865  prmo2  16949  prmo3  16950  dec5dvds  16973  dec2nprm  16976  2exp5  16994  2exp6  16995  2exp7  16996  2exp8  16997  2exp11  16998  2exp16  16999  7prm  17019  11prm  17023  13prm  17024  37prm  17029  43prm  17030  83prm  17031  139prm  17032  163prm  17033  317prm  17034  631prm  17035  1259lem1  17039  1259lem2  17040  1259lem3  17041  1259lem4  17042  1259lem5  17043  1259prm  17044  2503lem1  17045  2503lem2  17046  2503lem3  17047  4001lem1  17049  4001lem2  17050  4001lem3  17051  4001lem4  17052  4001prm  17053  psgnunilem2  19405  efgtlen  19636  efgredleme  19653  frgpnabllem1  19783  lt6abl  19805  htpycc  24904  pcoval2  24941  pcocn  24942  pcohtpylem  24944  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevlem  24951  csbren  25324  minveclem2  25351  ovolunlem1a  25422  ovolunlem1  25423  vitalilem4  25537  mbfi1fseqlem5  25645  dvmptre  25898  dvsincos  25910  aaliou3lem2  26276  aaliou3lem3  26277  aaliou3lem8  26278  coscn  26380  sinhalfpilem  26397  cospi  26406  ef2pi  26411  ef2kpi  26412  efper  26413  sinperlem  26414  sin2kpi  26417  cos2kpi  26418  sin2pim  26419  cos2pim  26420  sincosq3sgn  26434  sincosq4sgn  26435  tangtx  26439  sinq12gt0  26441  sincosq1eq  26446  sincos4thpi  26447  sincos6thpi  26450  sincos3rdpi  26451  pige3ALT  26454  abssinper  26455  coskpi  26457  sineq0  26458  coseq1  26459  efeq1  26462  efif1olem4  26479  eflogeq  26536  tanarg  26553  cxpsqrtlem  26636  cxpsqrt  26637  logsqrt  26638  2irrexpq  26665  root1eq1  26690  cxpeq  26692  2logb9irrALT  26733  sqrt2cxp2logb9e3  26734  ang180lem2  26745  ang180lem3  26746  quad2  26774  1cubrlem  26776  1cubr  26777  dcubic2  26779  dcubic1  26780  dcubic  26781  mcubic  26782  cubic2  26783  cubic  26784  dquartlem1  26786  dquartlem2  26787  dquart  26788  quart1lem  26790  quart1  26791  quartlem1  26792  quartlem2  26793  quartlem3  26794  quart  26796  sinasin  26824  asinsin  26827  atancj  26845  efiatan  26847  efiatan2  26852  2efiatan  26853  tanatan  26854  atantan  26858  atanbndlem  26860  atans2  26866  dvatan  26870  atantayl2  26873  leibpilem2  26876  log2cnv  26879  log2tlbnd  26880  log2ublem2  26882  log2ublem3  26883  log2ub  26884  birthday  26889  zetacvg  26950  basellem1  27016  basellem3  27018  basellem8  27023  basellem9  27024  cht3  27108  1sgm2ppw  27136  ppiub  27140  chtublem  27147  chtub  27148  perfect1  27164  perfectlem1  27165  perfectlem2  27166  perfect  27167  bcmax  27214  bcp1ctr  27215  bclbnd  27216  bpos1lem  27218  bpos1  27219  bposlem1  27220  bposlem2  27221  bposlem4  27223  bposlem5  27224  bposlem6  27225  bposlem8  27227  bposlem9  27228  lgsdir2lem2  27262  gausslemma2dlem6  27308  lgsquadlem1  27316  lgsquadlem2  27317  lgsquad2lem2  27321  m1lgs  27324  2lgslem3a  27332  2lgslem3b  27333  2lgslem3c  27334  2lgslem3d  27335  2lgsoddprmlem2  27345  2lgsoddprmlem3c  27348  2lgsoddprmlem3d  27349  addsqnreup  27379  addsq2nreurex  27380  rplogsumlem1  27420  dchrisum0fno1  27447  dchrisum0lem1  27452  dchrisum0lem2  27454  logdivsum  27469  mulog2sumlem3  27472  log2sumbnd  27480  selberglem1  27481  selberglem2  27482  selberg2  27487  selberg4lem1  27496  selberg3r  27505  pntpbnd1a  27521  pntpbnd2  27523  pntibndlem2  27527  pntlemk  27542  ax5seglem7  28911  axlowdimlem13  28930  elwspths2spth  29943  clwlkclwwlklem2a4  29972  clwwlknonex2  30084  2clwwlk2  30323  numclwlk1lem1  30344  ex-fl  30422  ex-ceil  30423  ex-exp  30425  ex-fac  30426  ex-abs  30430  ex-ind-dvds  30436  ipidsq  30685  cncph  30794  ip0i  30800  ip1ilem  30801  ipdirilem  30804  minvecolem2  30850  hvsubcan2i  31039  norm-ii-i  31112  norm3lem  31124  normpar2i  31131  polid2i  31132  hhph  31153  mayete3i  31703  nmcexi  32001  opsqrlem6  32120  addltmulALT  32421  ply1dg3rt0irred  33541  fldext2chn  33736  constrelextdg2  33755  2sqr3minply  33788  cos9thpiminplylem4  33793  cos9thpiminplylem5  33794  omssubadd  34308  oddpwdc  34362  fib5  34413  ballotlem2  34497  ballotth  34546  efmul2picn  34604  itgexpif  34614  vtscl  34646  circlemeth  34648  hgt750lemd  34656  logdivsqrle  34658  hgt750lem  34659  hgt750lem2  34660  problem4  35700  problem5  35701  quad3  35702  cnndvlem1  36570  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem29  37688  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  itg2addnclem3  37712  dvasin  37743  areacirc  37752  heiborlem6  37855  12gcd5e1  42035  12lcm5e60  42040  60lcm7e420  42042  420lcm8e840  42043  3exp7  42085  3lexlogpow5ineq1  42086  3lexlogpow2ineq2  42091  3lexlogpow5ineq5  42092  aks4d1p1p5  42107  aks4d1p1  42108  posbezout  42132  facp2  42175  1p3e4  42291  sqn5i  42317  235t711  42337  ex-decpmul  42338  cxp112d  42373  cxp111d  42374  cxpi11d  42375  tanhalfpim  42381  fltne  42676  flt4lem5e  42688  sum9cubes  42704  3cubeslem3l  42718  3cubeslem3r  42719  rmxluc  42968  rmyluc  42969  jm2.17a  42992  jm2.18  43020  jm2.23  43028  jm3.1lem1  43049  proot1ex  43228  areaquad  43248  sqrtcval  43673  resqrtvalex  43677  lhe4.4ex1a  44361  sineq0ALT  44968  coskpi2  45903  cosnegpi  45904  cosknegpi  45906  stoweidlem26  46063  wallispilem4  46105  wallispi  46107  wallispi2lem1  46108  stirlinglem8  46118  dirkerper  46133  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkeritg  46139  dirkercncflem1  46140  dirkercncflem2  46141  fourierdlem57  46200  fourierdlem58  46201  fourierdlem62  46205  fourierdlem76  46219  fourierdlem103  46246  fourierdlem104  46247  sqwvfourb  46266  fourierswlem  46267  rehalfge1  47365  ceil5half3  47370  modm2nep1  47396  modm1nep2  47398  modm1nem2  47399  fmtnoge3  47560  fmtnorec1  47567  fmtno0  47570  fmtno1  47571  fmtnorec3  47578  fmtnorec4  47579  fmtno5lem2  47584  fmtno5lem4  47586  257prm  47591  fmtnoprmfac2lem1  47596  fmtno4prmfac  47602  fmtno5faclem2  47610  fmtno5faclem3  47611  fmtno5fac  47612  139prmALT  47626  31prm  47627  127prm  47629  mod42tp1mod8  47632  lighneallem2  47636  lighneallem3  47637  lighneallem4a  47638  3exp4mod41  47646  41prothprmlem1  47647  41prothprmlem2  47648  41prothprm  47649  bits0ALTV  47709  0evenALTV  47718  6even  47741  8even  47743  perfectALTVlem1  47751  perfectALTVlem2  47752  perfectALTV  47753  2exp340mod341  47763  8exp8mod9  47766  mogoldbb  47815  nnsum3primes4  47818  bgoldbtbndlem1  47835  gpg5order  48090  gpg5edgnedg  48160  0nodd  48200  0even  48267  2even  48269  2zrngamgm  48275  2t6m3t4e0  48378  linevalexample  48426  zlmodzxzequap  48530  pw2m1lepw2m1  48551  nnlog2ge0lt1  48597  logbpw2m1  48598  nnpw2blen  48611  nnpw2pmod  48614  blen1  48615  blen2  48616  blennnt2  48620  nnolog2flm1  48621  0dig2nn0e  48643  0dig2nn0o  48644  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651  nn0sumshdiglem1  48652  nn0sumshdiglem2  48653  ackval1012  48721  ackval2012  48722  ackval3012  48723  ackval42  48727  sinhpcosh  49771