Theorem 2cn 12261

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  2c2 12241

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 11126  ax-addcl 11128

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

This theorem is referenced by:  2ex  12263  2cnd  12264  3cn  12267  2m1e1  12307  3m1e2  12309  2p2e4  12316  times2  12318  2div2e1  12322  1p2e3ALT  12325  3p3e6  12333  4p3e7  12335  5p3e8  12338  6p3e9  12341  2t1e2  12344  2t2e4  12345  3t3e9  12348  2t0e0  12350  4d2e2  12351  2cnne0  12391  halfcn  12396  2halves  12400  8th4div3  12402  halfthird  12403  halfpm6th  12404  2mulicn  12406  2muline0  12407  halfcl  12408  half0  12410  halfaddsub  12415  div4p1lem1div2  12437  3halfnz  12613  zneo  12617  nneo  12618  zeo  12620  7p3e10  12724  4t4e16  12748  6t3e18  12754  7t7e49  12763  8t5e40  12767  9t9e81  12778  decbin0  12789  decbin2  12790  fztpval  13547  fz0tp  13589  fzo0to3tp  13713  fzo1to4tp  13715  expubnd  14143  sq2  14162  sq4e2t8  14164  cu2  14165  subsq2  14176  binom2sub  14185  binom3  14189  zesq  14191  fac2  14244  fac3  14245  faclbnd2  14256  faclbnd4lem1  14258  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd5  14263  bcn2  14284  4bc2eq6  14294  swrd2lsw  14918  crre  15080  addcj  15114  imval2  15117  01sqrexlem7  15214  absmax  15296  rddif  15307  sqreulem  15326  amgm2  15336  abs3lemi  15377  iseraltlem2  15649  ackbijnn  15794  climcndslem1  15815  climcndslem2  15816  arisum  15826  arisum2  15827  geo2sum2  15840  geo2lim  15841  geoihalfsum  15848  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  efcllem  16043  ege2le3  16056  efgt0  16071  tanval2  16101  tanval3  16102  efi4p  16105  efival  16120  sinadd  16132  cosadd  16133  sinmul  16140  cos2tsin  16147  ef01bndlem  16152  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  cos01gt0  16159  sin02gt0  16160  sin4lt0  16163  odd2np1lem  16310  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  nno  16352  nn0o  16353  flodddiv4  16385  bits0  16398  bitsfzolem  16404  0bits  16409  bitsinv1  16412  sadcadd  16428  smumullem  16462  6gcd4e2  16508  3lcm2e6woprm  16585  6lcm4e12  16586  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  iserodd  16806  prmreclem5  16891  prmreclem6  16892  4sqlem11  16926  4sqlem12  16927  prmo2  17011  prmo3  17012  dec5dvds  17035  dec2nprm  17038  2exp5  17056  2exp6  17057  2exp7  17058  2exp8  17059  2exp11  17060  2exp16  17061  7prm  17081  11prm  17085  13prm  17086  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  psgnunilem2  19425  efgtlen  19656  efgredleme  19673  frgpnabllem1  19803  lt6abl  19825  htpycc  24879  pcoval2  24916  pcocn  24917  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  csbren  25299  minveclem2  25326  ovolunlem1a  25397  ovolunlem1  25398  vitalilem4  25512  mbfi1fseqlem5  25620  dvmptre  25873  dvsincos  25885  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem8  26253  coscn  26355  sinhalfpilem  26372  cospi  26381  ef2pi  26386  ef2kpi  26387  efper  26388  sinperlem  26389  sin2kpi  26392  cos2kpi  26393  sin2pim  26394  cos2pim  26395  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sinq12gt0  26416  sincosq1eq  26421  sincos4thpi  26422  sincos6thpi  26425  sincos3rdpi  26426  pige3ALT  26429  abssinper  26430  coskpi  26432  sineq0  26433  coseq1  26434  efeq1  26437  efif1olem4  26454  eflogeq  26511  tanarg  26528  cxpsqrtlem  26611  cxpsqrt  26612  logsqrt  26613  2irrexpq  26640  root1eq1  26665  cxpeq  26667  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  ang180lem2  26720  ang180lem3  26721  quad2  26749  1cubrlem  26751  1cubr  26752  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  quartlem3  26769  quart  26771  sinasin  26799  asinsin  26802  atancj  26820  efiatan  26822  efiatan2  26827  2efiatan  26828  tanatan  26829  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl2  26848  leibpilem2  26851  log2cnv  26854  log2tlbnd  26855  log2ublem2  26857  log2ublem3  26858  log2ub  26859  birthday  26864  zetacvg  26925  basellem1  26991  basellem3  26993  basellem8  26998  basellem9  26999  cht3  27083  1sgm2ppw  27111  ppiub  27115  chtublem  27122  chtub  27123  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  bcmax  27189  bcp1ctr  27190  bclbnd  27191  bpos1lem  27193  bpos1  27194  bposlem1  27195  bposlem2  27196  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem2  27237  gausslemma2dlem6  27283  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem2  27296  m1lgs  27299  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgsoddprmlem2  27320  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  addsqnreup  27354  addsq2nreurex  27355  rplogsumlem1  27395  dchrisum0fno1  27422  dchrisum0lem1  27427  dchrisum0lem2  27429  logdivsum  27444  mulog2sumlem3  27447  log2sumbnd  27455  selberglem1  27456  selberglem2  27457  selberg2  27462  selberg4lem1  27471  selberg3r  27480  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2  27502  pntlemk  27517  ax5seglem7  28862  axlowdimlem13  28881  elwspths2spth  29897  clwlkclwwlklem2a4  29926  clwwlknonex2  30038  2clwwlk2  30277  numclwlk1lem1  30298  ex-fl  30376  ex-ceil  30377  ex-exp  30379  ex-fac  30380  ex-abs  30384  ex-ind-dvds  30390  ipidsq  30639  cncph  30748  ip0i  30754  ip1ilem  30755  ipdirilem  30758  minvecolem2  30804  hvsubcan2i  30993  norm-ii-i  31066  norm3lem  31078  normpar2i  31085  polid2i  31086  hhph  31107  mayete3i  31657  nmcexi  31955  opsqrlem6  32074  addltmulALT  32375  ply1dg3rt0irred  33551  fldext2chn  33718  constrelextdg2  33737  2sqr3minply  33770  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  omssubadd  34291  oddpwdc  34345  fib5  34396  ballotlem2  34480  ballotth  34529  efmul2picn  34587  itgexpif  34597  vtscl  34629  circlemeth  34631  hgt750lemd  34639  logdivsqrle  34641  hgt750lem  34642  hgt750lem2  34643  problem4  35655  problem5  35656  quad3  35657  cnndvlem1  36525  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem29  37643  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  itg2addnclem3  37667  dvasin  37698  areacirc  37707  heiborlem6  37810  12gcd5e1  41991  12lcm5e60  41996  60lcm7e420  41998  420lcm8e840  41999  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p5  42063  aks4d1p1  42064  posbezout  42088  facp2  42131  1p3e4  42247  sqn5i  42273  235t711  42293  ex-decpmul  42294  cxp112d  42329  cxp111d  42330  cxpi11d  42331  tanhalfpim  42337  fltne  42632  flt4lem5e  42644  sum9cubes  42660  3cubeslem3l  42674  3cubeslem3r  42675  rmxluc  42925  rmyluc  42926  jm2.17a  42949  jm2.18  42977  jm2.23  42985  jm3.1lem1  43006  proot1ex  43185  areaquad  43205  sqrtcval  43630  resqrtvalex  43634  lhe4.4ex1a  44318  sineq0ALT  44926  coskpi2  45864  cosnegpi  45865  cosknegpi  45867  stoweidlem26  46024  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  stirlinglem8  46079  dirkerper  46094  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem2  46102  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem76  46180  fourierdlem103  46207  fourierdlem104  46208  sqwvfourb  46227  fourierswlem  46228  rehalfge1  47336  ceil5half3  47341  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  fmtnoge3  47531  fmtnorec1  47538  fmtno0  47541  fmtno1  47542  fmtnorec3  47549  fmtnorec4  47550  fmtno5lem2  47555  fmtno5lem4  47557  257prm  47562  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  fmtno5faclem2  47581  fmtno5faclem3  47582  fmtno5fac  47583  139prmALT  47597  31prm  47598  127prm  47600  mod42tp1mod8  47603  lighneallem2  47607  lighneallem3  47608  lighneallem4a  47609  3exp4mod41  47617  41prothprmlem1  47618  41prothprmlem2  47619  41prothprm  47620  bits0ALTV  47680  0evenALTV  47689  6even  47712  8even  47714  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  2exp340mod341  47734  8exp8mod9  47737  mogoldbb  47786  nnsum3primes4  47789  bgoldbtbndlem1  47806  gpg5order  48051  0nodd  48158  0even  48225  2even  48227  2zrngamgm  48233  2t6m3t4e0  48336  linevalexample  48384  zlmodzxzequap  48488  pw2m1lepw2m1  48509  nnlog2ge0lt1  48555  logbpw2m1  48556  nnpw2blen  48569  nnpw2pmod  48572  blen1  48573  blen2  48574  blennnt2  48578  nnolog2flm1  48579  0dig2nn0e  48601  0dig2nn0o  48602  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval42  48685  sinhpcosh  49729