Theorem 2cn 11700

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 11688	. 2 ⊢ 2 = (1 + 1)
2		ax-1cn 10584	. . 3 ⊢ 1 ∈ ℂ
3	2, 2	addcli 10636	. 2 ⊢ (1 + 1) ∈ ℂ
4	1, 3	eqeltri 2886	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529  2c2 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-2 11688

This theorem is referenced by:  2ex  11702  2cnd  11703  3cn  11706  2m1e1  11751  3m1e2  11753  2p2e4  11760  times2  11762  2div2e1  11766  1p2e3ALT  11769  3p3e6  11777  4p3e7  11779  5p3e8  11782  6p3e9  11785  2t1e2  11788  2t2e4  11789  3t3e9  11792  2t0e0  11794  4d2e2  11795  2cnne0  11835  halfcn  11840  1mhlfehlf  11844  8th4div3  11845  halfpm6th  11846  2mulicn  11848  2muline0  11849  halfcl  11850  half0  11852  2halves  11853  halfaddsub  11858  div4p1lem1div2  11880  3halfnz  12049  zneo  12053  nneo  12054  zeo  12056  7p3e10  12161  4t4e16  12185  6t3e18  12191  7t7e49  12200  8t5e40  12204  9t9e81  12215  decbin0  12226  decbin2  12227  halfthird  12229  fztpval  12964  fz0tp  13003  fz0to4untppr  13005  fzo0to3tp  13118  fzo1to4tp  13120  expubnd  13537  sq2  13556  sq4e2t8  13558  cu2  13559  subsq2  13569  binom2sub  13577  binom3  13581  zesq  13583  fac2  13635  fac3  13636  faclbnd2  13647  faclbnd4lem1  13649  faclbnd4lem3  13651  faclbnd4lem4  13652  faclbnd5  13654  bcn2  13675  4bc2eq6  13685  swrd2lsw  14305  crre  14465  addcj  14499  imval2  14502  sqrlem7  14600  absmax  14681  rddif  14692  sqreulem  14711  amgm2  14721  abs3lemi  14762  iseraltlem2  15031  ackbijnn  15175  climcndslem1  15196  climcndslem2  15197  arisum  15207  arisum2  15208  geo2sum2  15222  geo2lim  15223  geoihalfsum  15230  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  efcllem  15423  ege2le3  15435  efgt0  15448  tanval2  15478  tanval3  15479  efi4p  15482  efival  15497  sinadd  15509  cosadd  15510  sinmul  15517  cos2tsin  15524  ef01bndlem  15529  cos01bnd  15531  cos1bnd  15532  cos2bnd  15533  cos01gt0  15536  sin02gt0  15537  sin4lt0  15540  odd2np1lem  15681  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  nno  15723  nn0o  15724  flodddiv4  15754  bits0  15767  bitsfzolem  15773  0bits  15778  bitsinv1  15781  sadcadd  15797  smumullem  15831  6gcd4e2  15876  3lcm2e6woprm  15949  6lcm4e12  15950  pythagtriplem1  16143  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem15  16156  pythagtriplem16  16157  pythagtriplem17  16158  iserodd  16162  prmreclem5  16246  prmreclem6  16247  4sqlem11  16281  4sqlem12  16282  prmo2  16366  prmo3  16367  dec5dvds  16390  dec2nprm  16393  decexp2  16401  2exp5  16412  2exp6  16413  2exp7  16414  2exp8  16415  2exp16  16416  7prm  16436  11prm  16440  13prm  16441  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  psgnunilem2  18615  efgtlen  18844  efgredleme  18861  frgpnabllem1  18986  lt6abl  19008  htpycc  23585  pcoval2  23621  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  csbren  24003  minveclem2  24030  ovolunlem1a  24100  ovolunlem1  24101  vitalilem4  24215  mbfi1fseqlem5  24323  dvmptre  24572  dvsincos  24584  aaliou3lem2  24939  aaliou3lem3  24940  aaliou3lem8  24941  coscn  25040  sinhalfpilem  25056  cospi  25065  ef2pi  25070  ef2kpi  25071  efper  25072  sinperlem  25073  sin2kpi  25076  cos2kpi  25077  sin2pim  25078  cos2pim  25079  sincosq3sgn  25093  sincosq4sgn  25094  tangtx  25098  sinq12gt0  25100  sincosq1eq  25105  sincos4thpi  25106  sincos6thpi  25108  sincos3rdpi  25109  pige3ALT  25112  abssinper  25113  coskpi  25115  sineq0  25116  coseq1  25117  efeq1  25120  efif1olem4  25137  eflogeq  25193  tanarg  25210  cxpsqrtlem  25293  cxpsqrt  25294  logsqrt  25295  2irrexpq  25321  root1eq1  25344  cxpeq  25346  2logb9irrALT  25384  sqrt2cxp2logb9e3  25385  ang180lem2  25396  ang180lem3  25397  quad2  25425  1cubrlem  25427  1cubr  25428  dcubic2  25430  dcubic1  25431  dcubic  25432  mcubic  25433  cubic2  25434  cubic  25435  dquartlem1  25437  dquartlem2  25438  dquart  25439  quart1lem  25441  quart1  25442  quartlem1  25443  quartlem2  25444  quartlem3  25445  quart  25447  sinasin  25475  asinsin  25478  atancj  25496  efiatan  25498  efiatan2  25503  2efiatan  25504  tanatan  25505  atantan  25509  atanbndlem  25511  atans2  25517  dvatan  25521  atantayl2  25524  leibpilem2  25527  log2cnv  25530  log2tlbnd  25531  log2ublem2  25533  log2ublem3  25534  log2ub  25535  birthday  25540  zetacvg  25600  basellem1  25666  basellem3  25668  basellem8  25673  basellem9  25674  cht3  25758  1sgm2ppw  25784  ppiub  25788  chtublem  25795  chtub  25796  perfect1  25812  perfectlem1  25813  perfectlem2  25814  perfect  25815  bcmax  25862  bcp1ctr  25863  bclbnd  25864  bpos1lem  25866  bpos1  25867  bposlem1  25868  bposlem2  25869  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem8  25875  bposlem9  25876  lgsdir2lem2  25910  gausslemma2dlem6  25956  lgsquadlem1  25964  lgsquadlem2  25965  lgsquad2lem2  25969  m1lgs  25972  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgsoddprmlem2  25993  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  addsqnreup  26027  addsq2nreurex  26028  rplogsumlem1  26068  dchrisum0fno1  26095  dchrisum0lem1  26100  dchrisum0lem2  26102  logdivsum  26117  mulog2sumlem3  26120  log2sumbnd  26128  selberglem1  26129  selberglem2  26130  selberg2  26135  selberg4lem1  26144  selberg3r  26153  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem2  26175  pntlemk  26190  ax5seglem7  26729  axlowdimlem13  26748  elwspths2spth  27753  clwlkclwwlklem2a4  27782  clwwlknonex2  27894  2clwwlk2  28133  numclwlk1lem1  28154  ex-fl  28232  ex-ceil  28233  ex-exp  28235  ex-fac  28236  ex-abs  28240  ex-ind-dvds  28246  ipidsq  28493  cncph  28602  ip0i  28608  ip1ilem  28609  ipdirilem  28612  minvecolem2  28658  hvsubcan2i  28847  norm-ii-i  28920  norm3lem  28932  normpar2i  28939  polid2i  28940  hhph  28961  mayete3i  29511  nmcexi  29809  opsqrlem6  29928  addltmulALT  30229  omssubadd  31668  oddpwdc  31722  fib5  31773  ballotlem2  31856  ballotth  31905  efmul2picn  31977  itgexpif  31987  vtscl  32019  circlemeth  32021  hgt750lemd  32029  logdivsqrle  32031  hgt750lem  32032  hgt750lem2  32033  problem4  33024  problem5  33025  quad3  33026  cnndvlem1  33989  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem29  35086  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  itg2addnclem3  35110  dvasin  35141  areacirc  35150  heiborlem6  35254  12gcd5e1  39291  12lcm5e60  39296  60lcm7e420  39298  420lcm8e840  39299  3lexlogpow5ineq1  39341  facp2  39347  fac2xp3  39385  2xp3dxp2ge1d  39387  sqn5i  39479  235t711  39485  ex-decpmul  39486  3cubeslem3l  39627  3cubeslem3r  39628  rmxluc  39877  rmyluc  39878  jm2.17a  39901  jm2.18  39929  jm2.23  39937  jm3.1lem1  39958  proot1ex  40145  areaquad  40166  sqrtcval  40341  resqrtvalex  40345  lhe4.4ex1a  41033  sineq0ALT  41643  coskpi2  42508  cosnegpi  42509  cosknegpi  42511  stoweidlem26  42668  wallispilem4  42710  wallispi  42712  wallispi2lem1  42713  stirlinglem8  42723  dirkerper  42738  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkeritg  42744  dirkercncflem1  42745  dirkercncflem2  42746  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem76  42824  fourierdlem103  42851  fourierdlem104  42852  sqwvfourb  42871  fourierswlem  42872  fmtnoge3  44047  fmtnorec1  44054  fmtno0  44057  fmtno1  44058  fmtnorec3  44065  fmtnorec4  44066  fmtno5lem2  44071  fmtno5lem4  44073  257prm  44078  fmtnoprmfac2lem1  44083  fmtno4prmfac  44089  fmtno5faclem2  44097  fmtno5faclem3  44098  fmtno5fac  44099  139prmALT  44113  31prm  44114  127prm  44116  2exp11  44118  mod42tp1mod8  44120  lighneallem2  44124  lighneallem3  44125  lighneallem4a  44126  3exp4mod41  44134  41prothprmlem1  44135  41prothprmlem2  44136  41prothprm  44137  bits0ALTV  44197  0evenALTV  44206  6even  44229  8even  44231  perfectALTVlem1  44239  perfectALTVlem2  44240  perfectALTV  44241  2exp340mod341  44251  8exp8mod9  44254  mogoldbb  44303  nnsum3primes4  44306  bgoldbtbndlem1  44323  0nodd  44430  0even  44555  2even  44557  2zrngamgm  44563  2t6m3t4e0  44750  linevalexample  44804  zlmodzxzequap  44908  pw2m1lepw2m1  44929  nnlog2ge0lt1  44980  logbpw2m1  44981  nnpw2blen  44994  nnpw2pmod  44997  blen1  44998  blen2  44999  blennnt2  45003  nnolog2flm1  45004  0dig2nn0e  45026  0dig2nn0o  45027  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  nn0sumshdiglem2  45036  ackval1012  45104  ackval2012  45105  ackval3012  45106  ackval42  45110  sinhpcosh  45266