Theorem 2cn 12338

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 12326	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11264	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2834	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-2 12326

This theorem is referenced by:  2ex  12340  2cnd  12341  3cn  12344  2m1e1  12389  3m1e2  12391  2p2e4  12398  times2  12400  2div2e1  12404  1p2e3ALT  12407  3p3e6  12415  4p3e7  12417  5p3e8  12420  6p3e9  12423  2t1e2  12426  2t2e4  12427  3t3e9  12430  2t0e0  12432  4d2e2  12433  2cnne0  12473  halfcn  12478  1mhlfehlf  12482  8th4div3  12483  halfpm6th  12484  2mulicn  12486  2muline0  12487  halfcl  12488  half0  12490  2halves  12491  halfaddsub  12496  div4p1lem1div2  12518  3halfnz  12694  zneo  12698  nneo  12699  zeo  12701  7p3e10  12805  4t4e16  12829  6t3e18  12835  7t7e49  12844  8t5e40  12848  9t9e81  12859  decbin0  12870  decbin2  12871  halfthird  12873  fztpval  13622  fz0tp  13664  fzo0to3tp  13787  fzo1to4tp  13789  expubnd  14213  sq2  14232  sq4e2t8  14234  cu2  14235  subsq2  14246  binom2sub  14255  binom3  14259  zesq  14261  fac2  14314  fac3  14315  faclbnd2  14326  faclbnd4lem1  14328  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd5  14333  bcn2  14354  4bc2eq6  14364  swrd2lsw  14987  crre  15149  addcj  15183  imval2  15186  01sqrexlem7  15283  absmax  15364  rddif  15375  sqreulem  15394  amgm2  15404  abs3lemi  15445  iseraltlem2  15715  ackbijnn  15860  climcndslem1  15881  climcndslem2  15882  arisum  15892  arisum2  15893  geo2sum2  15906  geo2lim  15907  geoihalfsum  15914  bpoly2  16089  bpoly3  16090  bpoly4  16091  fsumcube  16092  efcllem  16109  ege2le3  16122  efgt0  16135  tanval2  16165  tanval3  16166  efi4p  16169  efival  16184  sinadd  16196  cosadd  16197  sinmul  16204  cos2tsin  16211  ef01bndlem  16216  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  cos01gt0  16223  sin02gt0  16224  sin4lt0  16227  odd2np1lem  16373  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  nno  16415  nn0o  16416  flodddiv4  16448  bits0  16461  bitsfzolem  16467  0bits  16472  bitsinv1  16475  sadcadd  16491  smumullem  16525  6gcd4e2  16571  3lcm2e6woprm  16648  6lcm4e12  16649  pythagtriplem1  16849  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem15  16862  pythagtriplem16  16863  pythagtriplem17  16864  iserodd  16868  prmreclem5  16953  prmreclem6  16954  4sqlem11  16988  4sqlem12  16989  prmo2  17073  prmo3  17074  dec5dvds  17097  dec2nprm  17100  decexp2  17108  2exp5  17119  2exp6  17120  2exp7  17121  2exp8  17122  2exp11  17123  2exp16  17124  7prm  17144  11prm  17148  13prm  17149  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  psgnunilem2  19527  efgtlen  19758  efgredleme  19775  frgpnabllem1  19905  lt6abl  19927  htpycc  25025  pcoval2  25062  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  csbren  25446  minveclem2  25473  ovolunlem1a  25544  ovolunlem1  25545  vitalilem4  25659  mbfi1fseqlem5  25768  dvmptre  26021  dvsincos  26033  aaliou3lem2  26399  aaliou3lem3  26400  aaliou3lem8  26401  coscn  26503  sinhalfpilem  26519  cospi  26528  ef2pi  26533  ef2kpi  26534  efper  26535  sinperlem  26536  sin2kpi  26539  cos2kpi  26540  sin2pim  26541  cos2pim  26542  sincosq3sgn  26556  sincosq4sgn  26557  tangtx  26561  sinq12gt0  26563  sincosq1eq  26568  sincos4thpi  26569  sincos6thpi  26572  sincos3rdpi  26573  pige3ALT  26576  abssinper  26577  coskpi  26579  sineq0  26580  coseq1  26581  efeq1  26584  efif1olem4  26601  eflogeq  26658  tanarg  26675  cxpsqrtlem  26758  cxpsqrt  26759  logsqrt  26760  2irrexpq  26787  root1eq1  26812  cxpeq  26814  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  ang180lem2  26867  ang180lem3  26868  quad2  26896  1cubrlem  26898  1cubr  26899  dcubic2  26901  dcubic1  26902  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1lem  26912  quart1  26913  quartlem1  26914  quartlem2  26915  quartlem3  26916  quart  26918  sinasin  26946  asinsin  26949  atancj  26967  efiatan  26969  efiatan2  26974  2efiatan  26975  tanatan  26976  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl2  26995  leibpilem2  26998  log2cnv  27001  log2tlbnd  27002  log2ublem2  27004  log2ublem3  27005  log2ub  27006  birthday  27011  zetacvg  27072  basellem1  27138  basellem3  27140  basellem8  27145  basellem9  27146  cht3  27230  1sgm2ppw  27258  ppiub  27262  chtublem  27269  chtub  27270  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  bcmax  27336  bcp1ctr  27337  bclbnd  27338  bpos1lem  27340  bpos1  27341  bposlem1  27342  bposlem2  27343  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem2  27384  gausslemma2dlem6  27430  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem2  27443  m1lgs  27446  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgsoddprmlem2  27467  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  addsqnreup  27501  addsq2nreurex  27502  rplogsumlem1  27542  dchrisum0fno1  27569  dchrisum0lem1  27574  dchrisum0lem2  27576  logdivsum  27591  mulog2sumlem3  27594  log2sumbnd  27602  selberglem1  27603  selberglem2  27604  selberg2  27609  selberg4lem1  27618  selberg3r  27627  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntlemk  27664  ax5seglem7  28964  axlowdimlem13  28983  elwspths2spth  29996  clwlkclwwlklem2a4  30025  clwwlknonex2  30137  2clwwlk2  30376  numclwlk1lem1  30397  ex-fl  30475  ex-ceil  30476  ex-exp  30478  ex-fac  30479  ex-abs  30483  ex-ind-dvds  30489  ipidsq  30738  cncph  30847  ip0i  30853  ip1ilem  30854  ipdirilem  30857  minvecolem2  30903  hvsubcan2i  31092  norm-ii-i  31165  norm3lem  31177  normpar2i  31184  polid2i  31185  hhph  31206  mayete3i  31756  nmcexi  32054  opsqrlem6  32173  addltmulALT  32474  ply1dg3rt0irred  33586  fldext2chn  33733  constrelextdg2  33751  2sqr3minply  33752  omssubadd  34281  oddpwdc  34335  fib5  34386  ballotlem2  34469  ballotth  34518  efmul2picn  34589  itgexpif  34599  vtscl  34631  circlemeth  34633  hgt750lemd  34641  logdivsqrle  34643  hgt750lem  34644  hgt750lem2  34645  problem4  35652  problem5  35653  quad3  35654  cnndvlem1  36519  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem29  37635  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  itg2addnclem3  37659  dvasin  37690  areacirc  37699  heiborlem6  37802  12gcd5e1  41984  12lcm5e60  41989  60lcm7e420  41991  420lcm8e840  41992  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1p1p5  42056  aks4d1p1  42057  posbezout  42081  facp2  42124  fac2xp3  42220  2xp3dxp2ge1d  42222  sqn5i  42298  235t711  42317  ex-decpmul  42318  cxp112d  42355  cxp111d  42356  cxpi11d  42357  tanhalfpim  42363  fltne  42630  flt4lem5e  42642  sum9cubes  42658  3cubeslem3l  42673  3cubeslem3r  42674  rmxluc  42924  rmyluc  42925  jm2.17a  42948  jm2.18  42976  jm2.23  42984  jm3.1lem1  43005  proot1ex  43184  areaquad  43204  sqrtcval  43630  resqrtvalex  43634  lhe4.4ex1a  44324  sineq0ALT  44934  coskpi2  45821  cosnegpi  45822  cosknegpi  45824  stoweidlem26  45981  wallispilem4  46023  wallispi  46025  wallispi2lem1  46026  stirlinglem8  46036  dirkerper  46051  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkeritg  46057  dirkercncflem1  46058  dirkercncflem2  46059  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem76  46137  fourierdlem103  46164  fourierdlem104  46165  sqwvfourb  46184  fourierswlem  46185  ceil5half3  47279  fmtnoge3  47454  fmtnorec1  47461  fmtno0  47464  fmtno1  47465  fmtnorec3  47472  fmtnorec4  47473  fmtno5lem2  47478  fmtno5lem4  47480  257prm  47485  fmtnoprmfac2lem1  47490  fmtno4prmfac  47496  fmtno5faclem2  47504  fmtno5faclem3  47505  fmtno5fac  47506  139prmALT  47520  31prm  47521  127prm  47523  mod42tp1mod8  47526  lighneallem2  47530  lighneallem3  47531  lighneallem4a  47532  3exp4mod41  47540  41prothprmlem1  47541  41prothprmlem2  47542  41prothprm  47543  bits0ALTV  47603  0evenALTV  47612  6even  47635  8even  47637  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  2exp340mod341  47657  8exp8mod9  47660  mogoldbb  47709  nnsum3primes4  47712  bgoldbtbndlem1  47729  gpg5order  47948  0nodd  48013  0even  48080  2even  48082  2zrngamgm  48088  2t6m3t4e0  48192  linevalexample  48240  zlmodzxzequap  48344  pw2m1lepw2m1  48365  nnlog2ge0lt1  48415  logbpw2m1  48416  nnpw2blen  48429  nnpw2pmod  48432  blen1  48433  blen2  48434  blennnt2  48438  nnolog2flm1  48439  0dig2nn0e  48461  0dig2nn0o  48462  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdiglem2  48471  ackval1012  48539  ackval2012  48540  ackval3012  48541  ackval42  48545  sinhpcosh  48970