Theorem 2cn 12221

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 12209	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11086	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11140	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2824	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   + caddc 11031  2c2 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-addcl 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12209

This theorem is referenced by:  2ex  12223  2cnd  12224  3cn  12227  2m1e1  12267  3m1e2  12269  2p2e4  12276  times2  12278  2div2e1  12282  1p2e3ALT  12285  3p3e6  12293  4p3e7  12295  5p3e8  12298  6p3e9  12301  2t1e2  12304  2t2e4  12305  3t3e9  12308  2t0e0  12310  4d2e2  12311  2cnne0  12351  halfcn  12356  2halves  12360  8th4div3  12362  halfthird  12363  halfpm6th  12364  2mulicn  12366  2muline0  12367  halfcl  12368  half0  12370  halfaddsub  12375  div4p1lem1div2  12397  3halfnz  12573  zneo  12577  nneo  12578  zeo  12580  7p3e10  12684  4t4e16  12708  6t3e18  12714  7t7e49  12723  8t5e40  12727  9t9e81  12738  decbin0  12749  decbin2  12750  fztpval  13507  fz0tp  13549  fzo0to3tp  13673  fzo1to4tp  13675  expubnd  14103  sq2  14122  sq4e2t8  14124  cu2  14125  subsq2  14136  binom2sub  14145  binom3  14149  zesq  14151  fac2  14204  fac3  14205  faclbnd2  14216  faclbnd4lem1  14218  faclbnd4lem3  14220  faclbnd4lem4  14221  faclbnd5  14223  bcn2  14244  4bc2eq6  14254  swrd2lsw  14877  crre  15039  addcj  15073  imval2  15076  01sqrexlem7  15173  absmax  15255  rddif  15266  sqreulem  15285  amgm2  15295  abs3lemi  15336  iseraltlem2  15608  ackbijnn  15753  climcndslem1  15774  climcndslem2  15775  arisum  15785  arisum2  15786  geo2sum2  15799  geo2lim  15800  geoihalfsum  15807  bpoly2  15982  bpoly3  15983  bpoly4  15984  fsumcube  15985  efcllem  16002  ege2le3  16015  efgt0  16030  tanval2  16060  tanval3  16061  efi4p  16064  efival  16079  sinadd  16091  cosadd  16092  sinmul  16099  cos2tsin  16106  ef01bndlem  16111  cos01bnd  16113  cos1bnd  16114  cos2bnd  16115  cos01gt0  16118  sin02gt0  16119  sin4lt0  16122  odd2np1lem  16269  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  nno  16311  nn0o  16312  flodddiv4  16344  bits0  16357  bitsfzolem  16363  0bits  16368  bitsinv1  16371  sadcadd  16387  smumullem  16421  6gcd4e2  16467  3lcm2e6woprm  16544  6lcm4e12  16545  pythagtriplem1  16746  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem15  16759  pythagtriplem16  16760  pythagtriplem17  16761  iserodd  16765  prmreclem5  16850  prmreclem6  16851  4sqlem11  16885  4sqlem12  16886  prmo2  16970  prmo3  16971  dec5dvds  16994  dec2nprm  16997  2exp5  17015  2exp6  17016  2exp7  17017  2exp8  17018  2exp11  17019  2exp16  17020  7prm  17040  11prm  17044  13prm  17045  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  psgnunilem2  19392  efgtlen  19623  efgredleme  19640  frgpnabllem1  19770  lt6abl  19792  htpycc  24895  pcoval2  24932  pcocn  24933  pcohtpylem  24935  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  csbren  25315  minveclem2  25342  ovolunlem1a  25413  ovolunlem1  25414  vitalilem4  25528  mbfi1fseqlem5  25636  dvmptre  25889  dvsincos  25901  aaliou3lem2  26267  aaliou3lem3  26268  aaliou3lem8  26269  coscn  26371  sinhalfpilem  26388  cospi  26397  ef2pi  26402  ef2kpi  26403  efper  26404  sinperlem  26405  sin2kpi  26408  cos2kpi  26409  sin2pim  26410  cos2pim  26411  sincosq3sgn  26425  sincosq4sgn  26426  tangtx  26430  sinq12gt0  26432  sincosq1eq  26437  sincos4thpi  26438  sincos6thpi  26441  sincos3rdpi  26442  pige3ALT  26445  abssinper  26446  coskpi  26448  sineq0  26449  coseq1  26450  efeq1  26453  efif1olem4  26470  eflogeq  26527  tanarg  26544  cxpsqrtlem  26627  cxpsqrt  26628  logsqrt  26629  2irrexpq  26656  root1eq1  26681  cxpeq  26683  2logb9irrALT  26724  sqrt2cxp2logb9e3  26725  ang180lem2  26736  ang180lem3  26737  quad2  26765  1cubrlem  26767  1cubr  26768  dcubic2  26770  dcubic1  26771  dcubic  26772  mcubic  26773  cubic2  26774  cubic  26775  dquartlem1  26777  dquartlem2  26778  dquart  26779  quart1lem  26781  quart1  26782  quartlem1  26783  quartlem2  26784  quartlem3  26785  quart  26787  sinasin  26815  asinsin  26818  atancj  26836  efiatan  26838  efiatan2  26843  2efiatan  26844  tanatan  26845  atantan  26849  atanbndlem  26851  atans2  26857  dvatan  26861  atantayl2  26864  leibpilem2  26867  log2cnv  26870  log2tlbnd  26871  log2ublem2  26873  log2ublem3  26874  log2ub  26875  birthday  26880  zetacvg  26941  basellem1  27007  basellem3  27009  basellem8  27014  basellem9  27015  cht3  27099  1sgm2ppw  27127  ppiub  27131  chtublem  27138  chtub  27139  perfect1  27155  perfectlem1  27156  perfectlem2  27157  perfect  27158  bcmax  27205  bcp1ctr  27206  bclbnd  27207  bpos1lem  27209  bpos1  27210  bposlem1  27211  bposlem2  27212  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem8  27218  bposlem9  27219  lgsdir2lem2  27253  gausslemma2dlem6  27299  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2lem2  27312  m1lgs  27315  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  2lgsoddprmlem2  27336  2lgsoddprmlem3c  27339  2lgsoddprmlem3d  27340  addsqnreup  27370  addsq2nreurex  27371  rplogsumlem1  27411  dchrisum0fno1  27438  dchrisum0lem1  27443  dchrisum0lem2  27445  logdivsum  27460  mulog2sumlem3  27463  log2sumbnd  27471  selberglem1  27472  selberglem2  27473  selberg2  27478  selberg4lem1  27487  selberg3r  27496  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem2  27518  pntlemk  27533  ax5seglem7  28898  axlowdimlem13  28917  elwspths2spth  29930  clwlkclwwlklem2a4  29959  clwwlknonex2  30071  2clwwlk2  30310  numclwlk1lem1  30331  ex-fl  30409  ex-ceil  30410  ex-exp  30412  ex-fac  30413  ex-abs  30417  ex-ind-dvds  30423  ipidsq  30672  cncph  30781  ip0i  30787  ip1ilem  30788  ipdirilem  30791  minvecolem2  30837  hvsubcan2i  31026  norm-ii-i  31099  norm3lem  31111  normpar2i  31118  polid2i  31119  hhph  31140  mayete3i  31690  nmcexi  31988  opsqrlem6  32107  addltmulALT  32408  ply1dg3rt0irred  33527  fldext2chn  33694  constrelextdg2  33713  2sqr3minply  33746  cos9thpiminplylem4  33751  cos9thpiminplylem5  33752  omssubadd  34267  oddpwdc  34321  fib5  34372  ballotlem2  34456  ballotth  34505  efmul2picn  34563  itgexpif  34573  vtscl  34605  circlemeth  34607  hgt750lemd  34615  logdivsqrle  34617  hgt750lem  34618  hgt750lem2  34619  problem4  35640  problem5  35641  quad3  35642  cnndvlem1  36510  sin2h  37589  cos2h  37590  tan2h  37591  poimirlem29  37628  mblfinlem1  37636  mblfinlem2  37637  mblfinlem3  37638  itg2addnclem3  37652  dvasin  37683  areacirc  37692  heiborlem6  37795  12gcd5e1  41976  12lcm5e60  41981  60lcm7e420  41983  420lcm8e840  41984  3exp7  42026  3lexlogpow5ineq1  42027  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1p1p5  42048  aks4d1p1  42049  posbezout  42073  facp2  42116  1p3e4  42232  sqn5i  42258  235t711  42278  ex-decpmul  42279  cxp112d  42314  cxp111d  42315  cxpi11d  42316  tanhalfpim  42322  fltne  42617  flt4lem5e  42629  sum9cubes  42645  3cubeslem3l  42659  3cubeslem3r  42660  rmxluc  42909  rmyluc  42910  jm2.17a  42933  jm2.18  42961  jm2.23  42969  jm3.1lem1  42990  proot1ex  43169  areaquad  43189  sqrtcval  43614  resqrtvalex  43618  lhe4.4ex1a  44302  sineq0ALT  44910  coskpi2  45848  cosnegpi  45849  cosknegpi  45851  stoweidlem26  46008  wallispilem4  46050  wallispi  46052  wallispi2lem1  46053  stirlinglem8  46063  dirkerper  46078  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkeritg  46084  dirkercncflem1  46085  dirkercncflem2  46086  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  fourierdlem76  46164  fourierdlem103  46191  fourierdlem104  46192  sqwvfourb  46211  fourierswlem  46212  rehalfge1  47320  ceil5half3  47325  modm2nep1  47351  modm1nep2  47353  modm1nem2  47354  fmtnoge3  47515  fmtnorec1  47522  fmtno0  47525  fmtno1  47526  fmtnorec3  47533  fmtnorec4  47534  fmtno5lem2  47539  fmtno5lem4  47541  257prm  47546  fmtnoprmfac2lem1  47551  fmtno4prmfac  47557  fmtno5faclem2  47565  fmtno5faclem3  47566  fmtno5fac  47567  139prmALT  47581  31prm  47582  127prm  47584  mod42tp1mod8  47587  lighneallem2  47591  lighneallem3  47592  lighneallem4a  47593  3exp4mod41  47601  41prothprmlem1  47602  41prothprmlem2  47603  41prothprm  47604  bits0ALTV  47664  0evenALTV  47673  6even  47696  8even  47698  perfectALTVlem1  47706  perfectALTVlem2  47707  perfectALTV  47708  2exp340mod341  47718  8exp8mod9  47721  mogoldbb  47770  nnsum3primes4  47773  bgoldbtbndlem1  47790  gpg5order  48045  gpg5edgnedg  48115  0nodd  48155  0even  48222  2even  48224  2zrngamgm  48230  2t6m3t4e0  48333  linevalexample  48381  zlmodzxzequap  48485  pw2m1lepw2m1  48506  nnlog2ge0lt1  48552  logbpw2m1  48553  nnpw2blen  48566  nnpw2pmod  48569  blen1  48570  blen2  48571  blennnt2  48575  nnolog2flm1  48576  0dig2nn0e  48598  0dig2nn0o  48599  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606  nn0sumshdiglem1  48607  nn0sumshdiglem2  48608  ackval1012  48676  ackval2012  48677  ackval3012  48678  ackval42  48682  sinhpcosh  49726