Theorem 2cn 12317

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 12304	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11159	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11216	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2859	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  1c1 11102   + caddc 11104  2c2 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12304

This theorem is referenced by:  2ex  12319  2cnd  12320  3cn  12323  2thalfe1  12349  2m1e1OLD  12367  3m1e2  12369  2p2e4  12376  times2  12378  2div2e1  12382  1p2e3ALT  12385  3p3e6  12393  4p3e7  12395  5p3e8  12398  6p3e9  12401  2t1e2  12404  2t2e4  12405  2t3e6  12408  3t3e9  12409  2t4e8  12411  2t0e0  12412  4div2e2  12413  2cnne0  12454  halfcn  12459  2halves  12463  8th4div3  12465  halfthird  12466  halfpm6th  12467  2mulicn  12469  2muline0  12470  halfcl  12471  half0  12473  halfaddsub  12478  div4p1lem1div2  12500  3halfnz  12676  zneo  12680  nneo  12681  zeo  12683  7p3e10  12792  4t4e16  12816  6t3e18  12822  7t7e49  12831  8t5e40  12835  9t9e81  12846  decbin0  12859  decbin2  12860  fztpval  13616  fz0tp  13658  fzo0to3tp  13783  fzo1to4tp  13785  expubnd  14216  sq2  14235  sq4e2t8  14237  cu2  14238  subsq2  14249  binom2sub  14258  binom3  14262  zesq  14264  fac2  14317  faclbnd2  14329  faclbnd4lem1  14331  faclbnd4lem3  14333  faclbnd4lem4  14334  faclbnd5  14336  bcn2  14357  4bc2eq6  14367  swrd2lsw  14991  crre  15167  addcj  15201  imval2  15204  01sqrexlem7  15301  absmax  15383  sqreulem  15413  amgm2  15423  abs3lemi  15464  iseraltlem2  15736  ackbijnn  15884  climcndslem1  15905  climcndslem2  15906  arisum  15916  arisum2  15917  geo2sum2  15930  geo2lim  15931  geoihalfsum  15938  bpoly2  16112  bpoly3  16113  bpoly4  16114  fsumcube  16115  efcllem  16132  ege2le3  16145  efgt0  16160  tanval2  16190  tanval3  16191  efi4p  16194  efival  16209  sinadd  16221  cosadd  16222  sinmul  16229  cos2tsin  16236  ef01bndlem  16241  cos01bnd  16243  cos1bnd  16244  cos2bnd  16245  cos01gt0  16248  sin02gt0  16249  sin4lt0  16252  odd2np1lem  16399  odd2np1  16400  opoe  16422  omoe  16423  opeo  16424  omeo  16425  nno  16441  nn0o  16442  flodddiv4  16474  bits0  16487  bitsfzolem  16493  0bits  16498  bitsinv1  16501  sadcadd  16517  smumullem  16551  6gcd4e2  16597  3lcm2e6woprm  16674  6lcm4e12  16675  pythagtriplem1  16877  pythagtriplem12  16887  pythagtriplem14  16889  pythagtriplem15  16890  pythagtriplem16  16891  pythagtriplem17  16892  iserodd  16896  prmreclem5  16981  prmreclem6  16982  4sqlem11  17016  4sqlem12  17017  prmo2  17101  dec5dvds  17125  dec2nprm  17128  2exp5  17146  2exp7  17148  2exp8  17149  2exp11  17150  2exp16  17151  10nprm  17174  11prm  17176  13prm  17177  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  psgnunilem2  19566  efgtlen  19797  efgredleme  19814  frgpnabllem1  19944  lt6abl  19966  pcoass  25164  pcorevlem  25166  csbren  25539  minveclem2  25566  ovolunlem1a  25636  ovolunlem1  25637  vitalilem4  25751  mbfi1fseqlem5  25859  dvmptre  26109  dvsincos  26121  aaliou3lem2  26485  aaliou3lem3  26486  aaliou3lem8  26487  coscn  26586  2picn  26600  sinhalfpilem  26606  cospi  26615  ef2pi  26620  ef2kpi  26621  efper  26622  sinperlem  26623  sin2kpi  26626  cos2kpi  26627  sin2pim  26628  cos2pim  26629  sincosq3sgn  26643  sincosq4sgn  26644  tangtx  26648  sinq12gt0  26650  sincosq1eq  26655  sincos4thpi  26656  sincos6thpi  26659  sincos3rdpi  26660  pige3ALT  26663  abssinper  26664  coskpi  26666  sineq0  26667  coseq1  26668  efeq1  26671  efif1olem4  26688  eflogeq  26745  tanarg  26762  cxpsqrtlem  26845  cxpsqrt  26846  logsqrt  26847  2irrexpq  26874  root1eq1  26898  cxpeq  26900  2logb9irrALT  26941  sqrt2cxp2logb9e3  26942  ang180lem2  26953  ang180lem3  26954  quad2  26982  1cubrlem  26984  1cubr  26985  dcubic2  26987  dcubic1  26988  dcubic  26989  mcubic  26990  cubic2  26991  cubic  26992  dquartlem1  26994  dquartlem2  26995  dquart  26996  quart1lem  26998  quart1  26999  quartlem1  27000  quartlem2  27001  quartlem3  27002  quart  27004  sinasin  27032  asinsin  27035  atancj  27053  efiatan  27055  efiatan2  27060  2efiatan  27061  tanatan  27062  atantan  27066  atanbndlem  27068  atans2  27074  dvatan  27078  atantayl2  27081  leibpilem2  27084  log2cnv  27087  log2tlbnd  27088  log2ublem2  27090  log2ublem3  27091  log2ub  27092  birthday  27097  zetacvg  27157  basellem1  27223  basellem3  27225  basellem8  27230  basellem9  27231  1sgm2ppw  27342  ppiub  27346  chtublem  27353  chtub  27354  perfect1  27370  perfectlem1  27371  perfectlem2  27372  perfect  27373  bcmax  27420  bcp1ctr  27421  bclbnd  27422  bpos1lem  27424  bpos1  27425  bposlem1  27426  bposlem2  27427  bposlem4  27429  bposlem5  27430  bposlem6  27431  bposlem8  27433  bposlem9  27434  lgsdir2lem2  27468  gausslemma2dlem6  27514  lgsquadlem1  27522  lgsquadlem2  27523  lgsquad2lem2  27527  m1lgs  27530  2lgslem3a  27538  2lgslem3b  27539  2lgslem3c  27540  2lgslem3d  27541  2lgsoddprmlem2  27551  2lgsoddprmlem3c  27554  2lgsoddprmlem3d  27555  addsqnreup  27585  addsq2nreurex  27586  rplogsumlem1  27626  dchrisum0fno1  27653  dchrisum0lem1  27658  dchrisum0lem2  27660  logdivsum  27675  mulog2sumlem3  27678  log2sumbnd  27686  selberglem1  27687  selberglem2  27688  selberg2  27693  selberg4lem1  27702  selberg3r  27711  pntpbnd1a  27727  pntpbnd2  27729  pntibndlem2  27733  pntlemk  27748  ax5seglem7  29263  axlowdimlem13  29282  elwspths2spth  30297  clwlkclwwlklem2a4  30326  clwwlknonex2  30438  2clwwlk2  30677  numclwlk1lem1  30698  ex-fl  30776  ex-ceil  30777  ex-exp  30779  ex-fac  30780  ex-abs  30784  ex-ind-dvds  30790  ipidsq  31040  cncph  31149  ip0i  31155  ip1ilem  31156  ipdirilem  31159  minvecolem2  31205  hvsubcan2i  31394  norm-ii-i  31467  norm3lem  31479  normpar2i  31486  polid2i  31487  hhph  31508  mayete3i  32058  nmcexi  32356  opsqrlem6  32475  addltmulALT  32776  ply1dg3rt0irred  33852  fldext2chn  34096  constrelextdg2  34115  2sqr3minply  34148  cos9thpiminplylem4  34153  cos9thpiminplylem5  34154  omssubadd  34668  oddpwdc  34722  fib5  34773  ballotlem2  34857  ballotth  34906  efmul2picn  34961  itgexpif  34971  vtscl  35003  circlemeth  35005  hgt750lemd  35013  logdivsqrle  35015  hgt750lem  35016  hgt750lem2  35017  problem4  36138  problem5  36139  quad3  36140  cnndvlem1  37104  sin2h  38239  cos2h  38240  tan2h  38241  poimirlem29  38278  mblfinlem1  38286  mblfinlem2  38287  mblfinlem3  38288  itg2addnclem3  38302  dvasin  38333  areacirc  38342  heiborlem6  38445  12gcd5e1  42748  12lcm5e60  42753  60lcm7e420  42755  420lcm8e840  42756  3exp7  42798  3lexlogpow5ineq1  42799  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1p1p5  42820  aks4d1p1  42821  posbezout  42845  facp2  42888  25or6to4  42951  1p3e4  43004  sqn5i  43024  235t711  43044  ex-decpmul  43045  cxp112d  43080  cxp111d  43081  cxpi11d  43082  tanhalfpim  43088  fltne  43356  flt4lem5e  43368  sum9cubes  43384  3cubeslem3l  43397  3cubeslem3r  43398  rmxluc  43643  rmyluc  43644  jm2.17a  43667  jm2.18  43695  jm2.23  43703  jm3.1lem1  43724  proot1ex  43903  areaquad  43923  sqrtcval  44347  resqrtvalex  44351  lhe4.4ex1a  45019  sineq0ALT  45625  coskpi2  46560  cosnegpi  46561  cosknegpi  46563  stoweidlem26  46720  wallispilem4  46762  wallispi  46764  wallispi2lem1  46765  stirlinglem8  46775  dirkerper  46790  dirkertrigeqlem3  46794  dirkertrigeq  46795  dirkeritg  46796  dirkercncflem1  46797  fourierdlem57  46857  fourierdlem58  46858  fourierdlem62  46862  fourierdlem76  46876  fourierdlem103  46903  fourierdlem104  46904  sqwvfourb  46923  fourierswlem  46924  nthrucw  47582  sin5tlem1  47587  sin5tlem5  47591  cos5t  47593  goldrasin  47596  goldracos5teq  47599  goldratmolem2  47600  rehalfge1  48053  ceil5half3  48060  modm2nep1  48086  modm1nep2  48088  modm1nem2  48089  fmtnoge3  48259  fmtnorec1  48266  fmtno0  48269  fmtno1  48270  fmtnorec3  48277  fmtnorec4  48278  fmtno5lem2  48283  fmtno5lem4  48285  257prm  48290  fmtnoprmfac2lem1  48295  fmtno4prmfac  48301  fmtno5faclem2  48309  fmtno5faclem3  48310  fmtno5fac  48311  139prmALT  48325  31prm  48326  127prm  48328  lighneallem2  48335  lighneallem3  48336  lighneallem4a  48337  3exp4mod41  48345  41prothprmlem1  48346  41prothprmlem2  48347  41prothprm  48348  bits0ALTV  48421  0evenALTV  48430  6even  48453  8even  48455  perfectALTVlem1  48463  perfectALTVlem2  48464  perfectALTV  48465  2exp340mod341  48475  8exp8mod9  48478  mogoldbb  48527  nnsum3primes4  48530  bgoldbtbndlem1  48547  gpg5order  48802  gpg5edgnedg  48872  0nodd  48912  0even  48979  2even  48981  2zrngamgm  48987  2t6m3t4e0  49105  linevalexample  49152  zlmodzxzequap  49256  pw2m1lepw2m1  49277  nnlog2ge0lt1  49323  logbpw2m1  49324  nnpw2blen  49337  nnpw2pmod  49340  blen1  49341  blen2  49342  blennnt2  49346  nnolog2flm1  49347  0dig2nn0e  49369  0dig2nn0o  49370  nn0sumshdiglemA  49376  nn0sumshdiglemB  49377  nn0sumshdiglem1  49378  nn0sumshdiglem2  49379  ackval1012  49447  ackval2012  49448  ackval3012  49449  ackval42  49453  sinhpcosh  50495