Theorem 2cn 12207

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 12195	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11071	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11125	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2829	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  1c1 11014   + caddc 11016  2c2 12187

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-addcl 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-2 12195

This theorem is referenced by:  2ex  12209  2cnd  12210  3cn  12213  2m1e1  12253  3m1e2  12255  2p2e4  12262  times2  12264  2div2e1  12268  1p2e3ALT  12271  3p3e6  12279  4p3e7  12281  5p3e8  12284  6p3e9  12287  2t1e2  12290  2t2e4  12291  3t3e9  12294  2t0e0  12296  4div2e2  12297  2cnne0  12337  halfcn  12342  2halves  12346  8th4div3  12348  halfthird  12349  halfpm6th  12350  2mulicn  12352  2muline0  12353  halfcl  12354  half0  12356  halfaddsub  12361  div4p1lem1div2  12383  3halfnz  12558  zneo  12562  nneo  12563  zeo  12565  7p3e10  12669  4t4e16  12693  6t3e18  12699  7t7e49  12708  8t5e40  12712  9t9e81  12723  decbin0  12734  decbin2  12735  fztpval  13488  fz0tp  13530  fzo0to3tp  13654  fzo1to4tp  13656  expubnd  14087  sq2  14106  sq4e2t8  14108  cu2  14109  subsq2  14120  binom2sub  14129  binom3  14133  zesq  14135  fac2  14188  fac3  14189  faclbnd2  14200  faclbnd4lem1  14202  faclbnd4lem3  14204  faclbnd4lem4  14205  faclbnd5  14207  bcn2  14228  4bc2eq6  14238  swrd2lsw  14861  crre  15023  addcj  15057  imval2  15060  01sqrexlem7  15157  absmax  15239  rddif  15250  sqreulem  15269  amgm2  15279  abs3lemi  15320  iseraltlem2  15592  ackbijnn  15737  climcndslem1  15758  climcndslem2  15759  arisum  15769  arisum2  15770  geo2sum2  15783  geo2lim  15784  geoihalfsum  15791  bpoly2  15966  bpoly3  15967  bpoly4  15968  fsumcube  15969  efcllem  15986  ege2le3  15999  efgt0  16014  tanval2  16044  tanval3  16045  efi4p  16048  efival  16063  sinadd  16075  cosadd  16076  sinmul  16083  cos2tsin  16090  ef01bndlem  16095  cos01bnd  16097  cos1bnd  16098  cos2bnd  16099  cos01gt0  16102  sin02gt0  16103  sin4lt0  16106  odd2np1lem  16253  odd2np1  16254  opoe  16276  omoe  16277  opeo  16278  omeo  16279  nno  16295  nn0o  16296  flodddiv4  16328  bits0  16341  bitsfzolem  16347  0bits  16352  bitsinv1  16355  sadcadd  16371  smumullem  16405  6gcd4e2  16451  3lcm2e6woprm  16528  6lcm4e12  16529  pythagtriplem1  16730  pythagtriplem12  16740  pythagtriplem14  16742  pythagtriplem15  16743  pythagtriplem16  16744  pythagtriplem17  16745  iserodd  16749  prmreclem5  16834  prmreclem6  16835  4sqlem11  16869  4sqlem12  16870  prmo2  16954  prmo3  16955  dec5dvds  16978  dec2nprm  16981  2exp5  16999  2exp6  17000  2exp7  17001  2exp8  17002  2exp11  17003  2exp16  17004  7prm  17024  11prm  17028  13prm  17029  37prm  17034  43prm  17035  83prm  17036  139prm  17037  163prm  17038  317prm  17039  631prm  17040  1259lem1  17044  1259lem2  17045  1259lem3  17046  1259lem4  17047  1259lem5  17048  1259prm  17049  2503lem1  17050  2503lem2  17051  2503lem3  17052  4001lem1  17054  4001lem2  17055  4001lem3  17056  4001lem4  17057  4001prm  17058  psgnunilem2  19409  efgtlen  19640  efgredleme  19657  frgpnabllem1  19787  lt6abl  19809  htpycc  24907  pcoval2  24944  pcocn  24945  pcohtpylem  24947  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevlem  24954  csbren  25327  minveclem2  25354  ovolunlem1a  25425  ovolunlem1  25426  vitalilem4  25540  mbfi1fseqlem5  25648  dvmptre  25901  dvsincos  25913  aaliou3lem2  26279  aaliou3lem3  26280  aaliou3lem8  26281  coscn  26383  sinhalfpilem  26400  cospi  26409  ef2pi  26414  ef2kpi  26415  efper  26416  sinperlem  26417  sin2kpi  26420  cos2kpi  26421  sin2pim  26422  cos2pim  26423  sincosq3sgn  26437  sincosq4sgn  26438  tangtx  26442  sinq12gt0  26444  sincosq1eq  26449  sincos4thpi  26450  sincos6thpi  26453  sincos3rdpi  26454  pige3ALT  26457  abssinper  26458  coskpi  26460  sineq0  26461  coseq1  26462  efeq1  26465  efif1olem4  26482  eflogeq  26539  tanarg  26556  cxpsqrtlem  26639  cxpsqrt  26640  logsqrt  26641  2irrexpq  26668  root1eq1  26693  cxpeq  26695  2logb9irrALT  26736  sqrt2cxp2logb9e3  26737  ang180lem2  26748  ang180lem3  26749  quad2  26777  1cubrlem  26779  1cubr  26780  dcubic2  26782  dcubic1  26783  dcubic  26784  mcubic  26785  cubic2  26786  cubic  26787  dquartlem1  26789  dquartlem2  26790  dquart  26791  quart1lem  26793  quart1  26794  quartlem1  26795  quartlem2  26796  quartlem3  26797  quart  26799  sinasin  26827  asinsin  26830  atancj  26848  efiatan  26850  efiatan2  26855  2efiatan  26856  tanatan  26857  atantan  26861  atanbndlem  26863  atans2  26869  dvatan  26873  atantayl2  26876  leibpilem2  26879  log2cnv  26882  log2tlbnd  26883  log2ublem2  26885  log2ublem3  26886  log2ub  26887  birthday  26892  zetacvg  26953  basellem1  27019  basellem3  27021  basellem8  27026  basellem9  27027  cht3  27111  1sgm2ppw  27139  ppiub  27143  chtublem  27150  chtub  27151  perfect1  27167  perfectlem1  27168  perfectlem2  27169  perfect  27170  bcmax  27217  bcp1ctr  27218  bclbnd  27219  bpos1lem  27221  bpos1  27222  bposlem1  27223  bposlem2  27224  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem8  27230  bposlem9  27231  lgsdir2lem2  27265  gausslemma2dlem6  27311  lgsquadlem1  27319  lgsquadlem2  27320  lgsquad2lem2  27324  m1lgs  27327  2lgslem3a  27335  2lgslem3b  27336  2lgslem3c  27337  2lgslem3d  27338  2lgsoddprmlem2  27348  2lgsoddprmlem3c  27351  2lgsoddprmlem3d  27352  addsqnreup  27382  addsq2nreurex  27383  rplogsumlem1  27423  dchrisum0fno1  27450  dchrisum0lem1  27455  dchrisum0lem2  27457  logdivsum  27472  mulog2sumlem3  27475  log2sumbnd  27483  selberglem1  27484  selberglem2  27485  selberg2  27490  selberg4lem1  27499  selberg3r  27508  pntpbnd1a  27524  pntpbnd2  27526  pntibndlem2  27530  pntlemk  27545  ax5seglem7  28915  axlowdimlem13  28934  elwspths2spth  29950  clwlkclwwlklem2a4  29979  clwwlknonex2  30091  2clwwlk2  30330  numclwlk1lem1  30351  ex-fl  30429  ex-ceil  30430  ex-exp  30432  ex-fac  30433  ex-abs  30437  ex-ind-dvds  30443  ipidsq  30692  cncph  30801  ip0i  30807  ip1ilem  30808  ipdirilem  30811  minvecolem2  30857  hvsubcan2i  31046  norm-ii-i  31119  norm3lem  31131  normpar2i  31138  polid2i  31139  hhph  31160  mayete3i  31710  nmcexi  32008  opsqrlem6  32127  addltmulALT  32428  ply1dg3rt0irred  33553  fldext2chn  33762  constrelextdg2  33781  2sqr3minply  33814  cos9thpiminplylem4  33819  cos9thpiminplylem5  33820  omssubadd  34334  oddpwdc  34388  fib5  34439  ballotlem2  34523  ballotth  34572  efmul2picn  34630  itgexpif  34640  vtscl  34672  circlemeth  34674  hgt750lemd  34682  logdivsqrle  34684  hgt750lem  34685  hgt750lem2  34686  problem4  35733  problem5  35734  quad3  35735  cnndvlem1  36602  sin2h  37670  cos2h  37671  tan2h  37672  poimirlem29  37709  mblfinlem1  37717  mblfinlem2  37718  mblfinlem3  37719  itg2addnclem3  37733  dvasin  37764  areacirc  37773  heiborlem6  37876  12gcd5e1  42116  12lcm5e60  42121  60lcm7e420  42123  420lcm8e840  42124  3exp7  42166  3lexlogpow5ineq1  42167  3lexlogpow2ineq2  42172  3lexlogpow5ineq5  42173  aks4d1p1p5  42188  aks4d1p1  42189  posbezout  42213  facp2  42256  1p3e4  42377  sqn5i  42403  235t711  42423  ex-decpmul  42424  cxp112d  42459  cxp111d  42460  cxpi11d  42461  tanhalfpim  42467  fltne  42762  flt4lem5e  42774  sum9cubes  42790  3cubeslem3l  42803  3cubeslem3r  42804  rmxluc  43053  rmyluc  43054  jm2.17a  43077  jm2.18  43105  jm2.23  43113  jm3.1lem1  43134  proot1ex  43313  areaquad  43333  sqrtcval  43758  resqrtvalex  43762  lhe4.4ex1a  44446  sineq0ALT  45053  coskpi2  45988  cosnegpi  45989  cosknegpi  45991  stoweidlem26  46148  wallispilem4  46190  wallispi  46192  wallispi2lem1  46193  stirlinglem8  46203  dirkerper  46218  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkeritg  46224  dirkercncflem1  46225  dirkercncflem2  46226  fourierdlem57  46285  fourierdlem58  46286  fourierdlem62  46290  fourierdlem76  46304  fourierdlem103  46331  fourierdlem104  46332  sqwvfourb  46351  fourierswlem  46352  nthrucw  47008  rehalfge1  47459  ceil5half3  47464  modm2nep1  47490  modm1nep2  47492  modm1nem2  47493  fmtnoge3  47654  fmtnorec1  47661  fmtno0  47664  fmtno1  47665  fmtnorec3  47672  fmtnorec4  47673  fmtno5lem2  47678  fmtno5lem4  47680  257prm  47685  fmtnoprmfac2lem1  47690  fmtno4prmfac  47696  fmtno5faclem2  47704  fmtno5faclem3  47705  fmtno5fac  47706  139prmALT  47720  31prm  47721  127prm  47723  mod42tp1mod8  47726  lighneallem2  47730  lighneallem3  47731  lighneallem4a  47732  3exp4mod41  47740  41prothprmlem1  47741  41prothprmlem2  47742  41prothprm  47743  bits0ALTV  47803  0evenALTV  47812  6even  47835  8even  47837  perfectALTVlem1  47845  perfectALTVlem2  47846  perfectALTV  47847  2exp340mod341  47857  8exp8mod9  47860  mogoldbb  47909  nnsum3primes4  47912  bgoldbtbndlem1  47929  gpg5order  48184  gpg5edgnedg  48254  0nodd  48294  0even  48361  2even  48363  2zrngamgm  48369  2t6m3t4e0  48472  linevalexample  48520  zlmodzxzequap  48624  pw2m1lepw2m1  48645  nnlog2ge0lt1  48691  logbpw2m1  48692  nnpw2blen  48705  nnpw2pmod  48708  blen1  48709  blen2  48710  blennnt2  48714  nnolog2flm1  48715  0dig2nn0e  48737  0dig2nn0o  48738  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745  nn0sumshdiglem1  48746  nn0sumshdiglem2  48747  ackval1012  48815  ackval2012  48816  ackval3012  48817  ackval42  48821  sinhpcosh  49865