MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2cn Structured version   Visualization version   GIF version

Theorem 2cn 11704
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
StepHypRef Expression
1 df-2 11692 . 2 2 = (1 + 1)
2 ax-1cn 10587 . . 3 1 ∈ ℂ
32, 2addcli 10639 . 2 (1 + 1) ∈ ℂ
41, 3eqeltri 2907 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7148  cc 10527  1c1 10530   + caddc 10532  2c2 11684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791  ax-1cn 10587  ax-addcl 10589
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-clel 2891  df-2 11692
This theorem is referenced by:  2ex  11706  2cnd  11707  3cn  11710  2m1e1  11755  3m1e2  11757  2p2e4  11764  times2  11766  2div2e1  11770  1p2e3ALT  11773  3p3e6  11781  4p3e7  11783  5p3e8  11786  6p3e9  11789  2t1e2  11792  2t2e4  11793  3t3e9  11796  2t0e0  11798  4d2e2  11799  2cnne0  11839  halfcn  11844  1mhlfehlf  11848  8th4div3  11849  halfpm6th  11850  2mulicn  11852  2muline0  11853  halfcl  11854  half0  11856  2halves  11857  halfaddsub  11862  div4p1lem1div2  11884  3halfnz  12053  zneo  12057  nneo  12058  zeo  12060  7p3e10  12165  4t4e16  12189  6t3e18  12195  7t7e49  12204  8t5e40  12208  9t9e81  12219  decbin0  12230  decbin2  12231  halfthird  12233  fztpval  12961  fz0tp  13000  fz0to4untppr  13002  fzo0to3tp  13115  fzo1to4tp  13117  expubnd  13533  sq2  13552  sq4e2t8  13554  cu2  13555  subsq2  13565  binom2sub  13573  binom3  13577  zesq  13579  fac2  13631  fac3  13632  faclbnd2  13643  faclbnd4lem1  13645  faclbnd4lem3  13647  faclbnd4lem4  13648  faclbnd5  13650  bcn2  13671  4bc2eq6  13681  swrd2lsw  14306  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  15725  nn0o  15726  flodddiv4  15756  bits0  15769  bitsfzolem  15775  0bits  15780  bitsinv1  15783  sadcadd  15799  smumullem  15833  6gcd4e2  15878  3lcm2e6woprm  15951  6lcm4e12  15952  pythagtriplem1  16145  pythagtriplem12  16155  pythagtriplem14  16157  pythagtriplem15  16158  pythagtriplem16  16159  pythagtriplem17  16160  iserodd  16164  prmreclem5  16248  prmreclem6  16249  4sqlem11  16283  4sqlem12  16284  prmo2  16368  prmo3  16369  dec5dvds  16392  dec2nprm  16395  decexp2  16403  2exp6  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  18985  lt6abl  19007  htpycc  23576  pcoval2  23612  pcocn  23613  pcohtpylem  23615  pcopt  23618  pcopt2  23619  pcoass  23620  pcorevlem  23622  csbren  23994  minveclem2  24021  ovolunlem1a  24089  ovolunlem1  24090  vitalilem4  24204  mbfi1fseqlem5  24312  dvmptre  24558  dvsincos  24570  aaliou3lem2  24924  aaliou3lem3  24925  aaliou3lem8  24926  coscn  25025  sinhalfpilem  25041  cospi  25050  ef2pi  25055  ef2kpi  25056  efper  25057  sinperlem  25058  sin2kpi  25061  cos2kpi  25062  sin2pim  25063  cos2pim  25064  sincosq3sgn  25078  sincosq4sgn  25079  tangtx  25083  sinq12gt0  25085  sincosq1eq  25090  sincos4thpi  25091  sincos6thpi  25093  sincos3rdpi  25094  pige3ALT  25097  abssinper  25098  coskpi  25100  sineq0  25101  coseq1  25102  efeq1  25105  efif1olem4  25121  eflogeq  25177  tanarg  25194  cxpsqrtlem  25277  cxpsqrt  25278  logsqrt  25279  2irrexpq  25305  root1eq1  25328  cxpeq  25330  2logb9irrALT  25368  sqrt2cxp2logb9e3  25369  ang180lem2  25380  ang180lem3  25381  quad2  25409  1cubrlem  25411  1cubr  25412  dcubic2  25414  dcubic1  25415  dcubic  25416  mcubic  25417  cubic2  25418  cubic  25419  dquartlem1  25421  dquartlem2  25422  dquart  25423  quart1lem  25425  quart1  25426  quartlem1  25427  quartlem2  25428  quartlem3  25429  quart  25431  sinasin  25459  asinsin  25462  atancj  25480  efiatan  25482  efiatan2  25487  2efiatan  25488  tanatan  25489  atantan  25493  atanbndlem  25495  atans2  25501  dvatan  25505  atantayl2  25508  leibpilem2  25511  log2cnv  25514  log2tlbnd  25515  log2ublem2  25517  log2ublem3  25518  log2ub  25519  birthday  25524  zetacvg  25584  basellem1  25650  basellem3  25652  basellem8  25657  basellem9  25658  cht3  25742  1sgm2ppw  25768  ppiub  25772  chtublem  25779  chtub  25780  perfect1  25796  perfectlem1  25797  perfectlem2  25798  perfect  25799  bcmax  25846  bcp1ctr  25847  bclbnd  25848  bpos1lem  25850  bpos1  25851  bposlem1  25852  bposlem2  25853  bposlem4  25855  bposlem5  25856  bposlem6  25857  bposlem8  25859  bposlem9  25860  lgsdir2lem2  25894  gausslemma2dlem6  25940  lgsquadlem1  25948  lgsquadlem2  25949  lgsquad2lem2  25953  m1lgs  25956  2lgslem3a  25964  2lgslem3b  25965  2lgslem3c  25966  2lgslem3d  25967  2lgsoddprmlem2  25977  2lgsoddprmlem3c  25980  2lgsoddprmlem3d  25981  addsqnreup  26011  addsq2nreurex  26012  rplogsumlem1  26052  dchrisum0fno1  26079  dchrisum0lem1  26084  dchrisum0lem2  26086  logdivsum  26101  mulog2sumlem3  26104  log2sumbnd  26112  selberglem1  26113  selberglem2  26114  selberg2  26119  selberg4lem1  26128  selberg3r  26137  pntpbnd1a  26153  pntpbnd2  26155  pntibndlem2  26159  pntlemk  26174  ax5seglem7  26713  axlowdimlem13  26732  elwspths2spth  27738  clwlkclwwlklem2a4  27767  clwwlknonex2  27880  2clwwlk2  28119  numclwlk1lem1  28140  ex-fl  28218  ex-ceil  28219  ex-exp  28221  ex-fac  28222  ex-abs  28226  ex-ind-dvds  28232  ipidsq  28479  cncph  28588  ip0i  28594  ip1ilem  28595  ipdirilem  28598  minvecolem2  28644  hvsubcan2i  28833  norm-ii-i  28906  norm3lem  28918  normpar2i  28925  polid2i  28926  hhph  28947  mayete3i  29497  nmcexi  29795  opsqrlem6  29914  addltmulALT  30215  omssubadd  31546  oddpwdc  31600  fib5  31651  ballotlem2  31734  ballotth  31783  efmul2picn  31855  itgexpif  31865  vtscl  31897  circlemeth  31899  hgt750lemd  31907  logdivsqrle  31909  hgt750lem  31910  hgt750lem2  31911  problem4  32899  problem5  32900  quad3  32901  cnndvlem1  33864  sin2h  34869  cos2h  34870  tan2h  34871  poimirlem29  34908  mblfinlem1  34916  mblfinlem2  34917  mblfinlem3  34918  itg2addnclem3  34932  dvasin  34965  areacirc  34974  heiborlem6  35081  sqn5i  39156  235t711  39162  ex-decpmul  39163  3cubeslem3l  39268  3cubeslem3r  39269  rmxluc  39518  rmyluc  39519  jm2.17a  39542  jm2.18  39570  jm2.23  39578  jm3.1lem1  39599  proot1ex  39786  areaquad  39808  lhe4.4ex1a  40646  sineq0ALT  41256  coskpi2  42131  cosnegpi  42132  cosknegpi  42134  stoweidlem26  42296  wallispilem4  42338  wallispi  42340  wallispi2lem1  42341  stirlinglem8  42351  dirkerper  42366  dirkertrigeqlem3  42370  dirkertrigeq  42371  dirkeritg  42372  dirkercncflem1  42373  dirkercncflem2  42374  fourierdlem57  42433  fourierdlem58  42434  fourierdlem62  42438  fourierdlem76  42452  fourierdlem103  42479  fourierdlem104  42480  sqwvfourb  42499  fourierswlem  42500  fmtnoge3  43677  fmtnorec1  43684  fmtno0  43687  fmtno1  43688  fmtnorec3  43695  fmtnorec4  43696  fmtno5lem2  43701  fmtno5lem4  43703  257prm  43708  fmtnoprmfac2lem1  43713  fmtno4prmfac  43719  fmtno5faclem2  43727  fmtno5faclem3  43728  fmtno5fac  43729  2exp5  43740  139prmALT  43744  31prm  43745  2exp7  43747  127prm  43748  2exp11  43750  mod42tp1mod8  43752  lighneallem2  43756  lighneallem3  43757  lighneallem4a  43758  3exp4mod41  43766  41prothprmlem1  43767  41prothprmlem2  43768  41prothprm  43769  bits0ALTV  43829  0evenALTV  43838  6even  43861  8even  43863  perfectALTVlem1  43871  perfectALTVlem2  43872  perfectALTV  43873  2exp340mod341  43883  8exp8mod9  43886  mogoldbb  43935  nnsum3primes4  43938  bgoldbtbndlem1  43955  0nodd  44062  0even  44187  2even  44189  2zrngamgm  44195  2t6m3t4e0  44381  linevalexample  44435  zlmodzxzequap  44539  pw2m1lepw2m1  44560  nnlog2ge0lt1  44611  logbpw2m1  44612  nnpw2blen  44625  nnpw2pmod  44628  blen1  44629  blen2  44630  blennnt2  44634  nnolog2flm1  44635  0dig2nn0e  44657  0dig2nn0o  44658  nn0sumshdiglemA  44664  nn0sumshdiglemB  44665  nn0sumshdiglem1  44666  nn0sumshdiglem2  44667  sinhpcosh  44824
  Copyright terms: Public domain W3C validator