Theorem 2cn 12334

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 12321	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 11176	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 11233	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2862	1 ⊢ 2 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  1c1 11119   + caddc 11121  2c2 12313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-2 12321

This theorem is used by:  2ex  12336  2cnd  12337  3cn  12340  2thalfe1  12366  2m1e1OLD  12384  3m1e2  12386  2p2e4  12393  times2  12395  2div2e1  12399  1p2e3ALT  12402  3p3e6  12410  4p3e7  12412  5p3e8  12415  6p3e9  12418  2t1e2  12421  2t2e4  12422  2t3e6  12425  3t3e9  12426  2t4e8  12428  2t0e0  12429  4div2e2  12430  2cnne0  12471  halfcn  12476  2halves  12480  8th4div3  12482  halfthird  12483  halfpm6th  12484  2mulicn  12486  2muline0  12487  halfcl  12488  half0  12490  halfaddsub  12495  div4p1lem1div2  12517  3halfnz  12693  zneo  12697  nneo  12698  zeo  12700  7p3e10  12809  4t4e16  12833  6t3e18  12839  7t7e49  12848  8t5e40  12852  9t9e81  12863  decbin0  12876  decbin2  12877  fztpval  13633  fz0tp  13675  fzo0to3tp  13800  fzo1to4tp  13802  expubnd  14234  sq2  14253  sq4e2t8  14255  cu2  14256  subsq2  14267  binom2sub  14276  binom3  14280  zesq  14282  fac2  14335  faclbnd2  14347  faclbnd4lem1  14349  faclbnd4lem3  14351  faclbnd4lem4  14352  faclbnd5  14354  bcn2  14375  4bc2eq6  14385  swrd2lsw  15015  crre  15191  addcj  15225  imval2  15228  01sqrexlem7  15325  absmax  15407  sqreulem  15437  amgm2  15447  abs3lemi  15488  iseraltlem2  15760  ackbijnn  15908  climcndslem1  15929  climcndslem2  15930  arisum  15940  arisum2  15941  geo2sum2  15954  geo2lim  15955  geoihalfsum  15962  bpoly2  16136  bpoly3  16137  bpoly4  16138  fsumcube  16139  efcllem  16156  ege2le3  16169  efgt0  16184  tanval2  16214  tanval3  16215  efi4p  16218  efival  16233  sinadd  16245  cosadd  16246  sinmul  16253  cos2tsin  16260  ef01bndlem  16265  cos01bnd  16267  cos1bnd  16268  cos2bnd  16269  cos01gt0  16272  sin02gt0  16273  sin4lt0  16276  odd2np1lem  16423  odd2np1  16424  opoe  16446  omoe  16447  opeo  16448  omeo  16449  nno  16465  nn0o  16466  flodddiv4  16498  bits0  16511  bitsfzolem  16517  0bits  16522  bitsinv1  16525  sadcadd  16541  smumullem  16575  6gcd4e2  16621  3lcm2e6woprm  16698  6lcm4e12  16699  pythagtriplem1  16901  pythagtriplem12  16911  pythagtriplem14  16913  pythagtriplem15  16914  pythagtriplem16  16915  pythagtriplem17  16916  iserodd  16920  prmreclem5  17005  prmreclem6  17006  4sqlem11  17040  4sqlem12  17041  prmo2  17125  dec5dvds  17149  dec2nprm  17152  2exp5  17170  2exp7  17172  2exp11  17174  2exp16  17175  10nprm  17198  11prm  17200  13prm  17201  37prm  17206  43prm  17207  83prm  17208  139prm  17209  163prm  17210  317prm  17211  631prm  17212  1259lem1  17216  1259lem2  17217  1259lem3  17218  1259lem4  17219  1259lem5  17220  1259prm  17221  2503lem1  17222  2503lem2  17223  2503lem3  17224  4001lem1  17226  4001lem2  17227  4001lem3  17228  4001lem4  17229  4001prm  17230  psgnunilem2  19596  efgtlen  19827  efgredleme  19844  frgpnabllem1  19974  lt6abl  19996  pcoass  25220  pcorevlem  25222  csbren  25595  minveclem2  25622  ovolunlem1a  25692  ovolunlem1  25693  vitalilem4  25807  mbfi1fseqlem5  25915  dvmptre  26165  dvsincos  26177  aaliou3lem2  26543  aaliou3lem3  26544  aaliou3lem8  26545  coscn  26645  2picn  26659  sinhalfpilem  26665  cospi  26674  ef2pi  26679  ef2kpi  26680  efper  26681  sinperlem  26682  sin2kpi  26685  cos2kpi  26686  sin2pim  26687  cos2pim  26688  sincosq3sgn  26702  sincosq4sgn  26703  tangtx  26707  sinq12gt0  26709  sincosq1eq  26714  sincos4thpi  26715  sincos6thpi  26718  sincos3rdpi  26719  pige3ALT  26722  abssinper  26723  coskpi  26725  sineq0  26726  coseq1  26727  efeq1  26730  efif1olem4  26747  eflogeq  26804  tanarg  26821  cxpsqrtlem  26904  cxpsqrt  26905  logsqrt  26906  2irrexpq  26933  root1eq1  26957  cxpeq  26959  2logb9irrALT  27000  sqrt2cxp2logb9e3  27001  ang180lem2  27012  ang180lem3  27013  quad2  27041  1cubrlem  27043  1cubr  27044  dcubic2  27046  dcubic1  27047  dcubic  27048  mcubic  27049  cubic2  27050  cubic  27051  dquartlem1  27053  dquartlem2  27054  dquart  27055  quart1lem  27057  quart1  27058  quartlem1  27059  quartlem2  27060  quartlem3  27061  quart  27063  sinasin  27091  asinsin  27094  atancj  27112  efiatan  27114  efiatan2  27119  2efiatan  27120  tanatan  27121  atantan  27125  atanbndlem  27127  atans2  27133  dvatan  27137  atantayl2  27140  leibpilem2  27143  log2cnv  27146  log2tlbnd  27147  log2ublem2  27149  log2ublem3  27150  log2ub  27151  birthday  27156  zetacvg  27216  basellem1  27282  basellem3  27284  basellem8  27289  basellem9  27290  1sgm2ppw  27401  ppiub  27405  chtublem  27412  chtub  27413  perfect1  27429  perfectlem1  27430  perfectlem2  27431  perfect  27432  bcmax  27479  bcp1ctr  27480  bclbnd  27481  bpos1lem  27483  bpos1  27484  bposlem1  27485  bposlem2  27486  bposlem4  27488  bposlem5  27489  bposlem6  27490  bposlem8  27492  bposlem9  27493  lgsdir2lem2  27527  gausslemma2dlem6  27573  lgsquadlem1  27581  lgsquadlem2  27582  lgsquad2lem2  27586  m1lgs  27589  2lgslem3a  27597  2lgslem3b  27598  2lgslem3c  27599  2lgslem3d  27600  2lgsoddprmlem2  27610  2lgsoddprmlem3c  27613  2lgsoddprmlem3d  27614  addsqnreup  27644  addsq2nreurex  27645  rplogsumlem1  27685  dchrisum0fno1  27712  dchrisum0lem1  27717  dchrisum0lem2  27719  logdivsum  27734  mulog2sumlem3  27737  log2sumbnd  27745  selberglem1  27746  selberglem2  27747  selberg2  27752  selberg4lem1  27761  selberg3r  27770  pntpbnd1a  27786  pntpbnd2  27788  pntibndlem2  27792  pntlemk  27807  ax5seglem7  29322  axlowdimlem13  29341  elwspths2spth  30356  clwlkclwwlklem2a4  30385  clwwlknonex2  30497  2clwwlk2  30736  numclwlk1lem1  30757  ex-fl  30835  ex-ceil  30836  ex-exp  30838  ex-fac  30839  ex-abs  30843  ex-ind-dvds  30849  ipidsq  31099  cncph  31208  ip0i  31214  ip1ilem  31215  ipdirilem  31218  minvecolem2  31264  hvsubcan2i  31453  norm-ii-i  31526  norm3lem  31538  normpar2i  31545  polid2i  31546  hhph  31567  mayete3i  32117  nmcexi  32415  opsqrlem6  32534  addltmulALT  32835  ply1dg3rt0irred  33905  fldext2chn  34149  constrelextdg2  34168  2sqr3minply  34201  cos9thpiminplylem4  34206  cos9thpiminplylem5  34207  omssubadd  34721  oddpwdc  34775  fib5  34826  ballotlem2  34910  ballotth  34959  efmul2picn  35014  itgexpif  35024  vtscl  35056  circlemeth  35058  hgt750lemd  35066  logdivsqrle  35068  hgt750lem  35069  hgt750lem2  35070  problem4  36180  problem5  36181  quad3  36182  cnndvlem1  37166  sin2h  38301  cos2h  38302  tan2h  38303  poimirlem29  38340  mblfinlem1  38348  mblfinlem2  38349  mblfinlem3  38350  itg2addnclem3  38364  dvasin  38395  areacirc  38404  heiborlem6  38507  12gcd5e1  42810  12lcm5e60  42815  60lcm7e420  42817  3exp7  42860  3lexlogpow5ineq1  42861  3lexlogpow5ineq5  42867  aks4d1p1p5  42882  aks4d1p1  42883  posbezout  42907  facp2  42950  25or6to4  43013  1p3e4  43066  sqn5i  43086  235t711  43106  ex-decpmul  43107  cxp112d  43142  cxp111d  43143  cxpi11d  43144  tanhalfpim  43150  fltne  43416  flt4lem5e  43428  sum9cubes  43444  3cubeslem3r  43458  rmxluc  43703  rmyluc  43704  jm2.17a  43727  jm2.18  43755  jm2.23  43763  jm3.1lem1  43784  proot1ex  43963  areaquad  43983  sqrtcval  44407  resqrtvalex  44411  lhe4.4ex1a  45079  sineq0ALT  45685  coskpi2  46620  cosnegpi  46621  cosknegpi  46623  stoweidlem26  46780  wallispilem4  46822  wallispi  46824  wallispi2lem1  46825  stirlinglem8  46835  dirkerper  46850  dirkertrigeqlem3  46854  dirkertrigeq  46855  dirkeritg  46856  dirkercncflem1  46857  fourierdlem57  46917  fourierdlem58  46918  fourierdlem62  46922  fourierdlem76  46936  fourierdlem103  46963  fourierdlem104  46964  sqwvfourb  46983  fourierswlem  46984  sin5tlem1  47650  sin5tlem5  47654  cos5t  47656  goldrasin  47659  goldracos5teq  47662  goldratmolem2  47663  rehalfge1  48116  ceil5half3  48123  modm2nep1  48149  modm1nep2  48151  modm1nem2  48152  fmtnoge3  48322  fmtnorec1  48329  fmtno0  48332  fmtno1  48333  fmtnorec3  48340  fmtnorec4  48341  fmtno5lem2  48346  fmtno5lem4  48348  257prm  48353  fmtnoprmfac2lem1  48358  fmtno4prmfac  48364  fmtno5faclem2  48372  fmtno5faclem3  48373  fmtno5fac  48374  139prmALT  48388  31prm  48389  127prm  48391  lighneallem2  48398  lighneallem3  48399  lighneallem4a  48400  3exp4mod41  48408  41prothprmlem1  48409  41prothprmlem2  48410  41prothprm  48411  bits0ALTV  48484  0evenALTV  48493  6even  48516  8even  48518  perfectALTVlem1  48526  perfectALTVlem2  48527  perfectALTV  48528  2exp340mod341  48538  mogoldbb  48590  nnsum3primes4  48593  bgoldbtbndlem1  48610  gpg5order  48865  gpg5edgnedg  48935  0nodd  48975  0even  49042  2even  49044  2zrngamgm  49050  2t6m3t4e0  49168  linevalexample  49215  zlmodzxzequap  49319  pw2m1lepw2m1  49340  nnlog2ge0lt1  49386  logbpw2m1  49387  nnpw2blen  49400  nnpw2pmod  49403  blen1  49404  blen2  49405  blennnt2  49409  nnolog2flm1  49410  0dig2nn0e  49432  0dig2nn0o  49433  nn0sumshdiglemA  49439  nn0sumshdiglemB  49440  nn0sumshdiglem1  49441  nn0sumshdiglem2  49442  ackval1012  49510  ackval2012  49511  ackval3012  49512  ackval42  49516  sinhpcosh  50558