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

Theorem neg1cn 11001
Description: -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
neg1cn -1 ∈ ℂ

Proof of Theorem neg1cn
StepHypRef Expression
1 ax-1cn 9873 . 2 1 ∈ ℂ
21negcli 10228 1 -1 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  cc 9813  1c1 9816  -cneg 10146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-sub 10147  df-neg 10148
This theorem is referenced by:  m1expcl2  12744  m1expeven  12769  iseraltlem2  14261  iseraltlem3  14262  fsumneg  14361  incexclem  14407  incexc  14408  risefallfac  14594  fallrisefac  14595  fallfac0  14598  0risefac  14608  binomrisefac  14612  m1expo  14930  m1exp1  14931  n2dvdsm1  14943  pwp1fsum  14952  bitsfzo  14995  bezoutlem1  15094  psgnunilem4  17740  m1expaddsub  17741  psgnuni  17742  psgnpmtr  17753  psgn0fv0  17754  psgnsn  17763  psgnprfval1  17765  cnmsgnsubg  19742  cnmsgnbas  19743  cnmsgngrp  19744  psgnghm  19745  psgninv  19747  mdetralt  20233  negcncf  22529  dvmptneg  23535  dvlipcn  23561  lhop2  23582  plysubcl  23782  coesub  23817  dgrsub  23832  quotlem  23859  quotcl2  23861  quotdgr  23862  iaa  23884  dvradcnv  23979  efipi  24029  eulerid  24030  sin2pi  24031  sinmpi  24043  cosmpi  24044  sinppi  24045  cosppi  24046  efif1olem2  24093  logneg  24138  lognegb  24140  logtayl  24206  logtayl2  24208  root1id  24295  root1eq1  24296  root1cj  24297  cxpeq  24298  angneg  24333  ang180lem1  24339  1cubrlem  24368  1cubr  24369  atandm4  24406  atandmtan  24447  atantayl3  24466  leibpi  24469  log2cnv  24471  wilthlem1  24594  wilthlem2  24595  basellem2  24608  basellem5  24611  basellem9  24615  isnsqf  24661  mule1  24674  mumul  24707  musum  24717  ppiub  24729  dchrptlem1  24789  dchrptlem2  24790  lgsneg  24846  lgsdilem  24849  lgsdir2lem3  24852  lgsdir2lem4  24853  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsne0  24860  gausslemma2dlem5  24896  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem1  24909  lgsquad2lem2  24910  lgsquad3  24912  m1lgs  24913  dchrisum0flblem1  24997  rpvmasum2  25001  axlowdimlem13  25634  vcm  26815  nvinvfval  26879  nvmval2  26882  nvmf  26884  nvmdi  26887  nvnegneg  26888  nvpncan2  26892  nvaddsub4  26896  nvm1  26904  nvdif  26905  nvmtri  26910  nvabs  26911  nvge0  26912  nvnd  26927  imsmetlem  26929  smcnlem  26936  vmcn  26938  ipval2  26946  4ipval2  26947  ipval3  26948  dipcj  26953  dip0r  26956  sspmval  26972  lno0  26995  lnosub  26998  ip0i  27064  ipdirilem  27068  ipasslem2  27071  ipasslem10  27078  dipsubdir  27087  hvsubf  27256  hvsubcl  27258  hvsubid  27267  hv2neg  27269  hvm1neg  27273  hvaddsubval  27274  hvsub4  27278  hvaddsub12  27279  hvpncan  27280  hvaddsubass  27282  hvsubass  27285  hvsubdistr1  27290  hvsubdistr2  27291  hvsubsub4i  27300  hvnegdii  27303  hvsubeq0i  27304  hvsubcan2i  27305  hvaddcani  27306  hvsubaddi  27307  hvaddeq0  27310  hvsubcan  27315  hvsubcan2  27316  hvsub0  27317  his2sub  27333  hisubcomi  27345  normlem0  27350  normlem9  27359  normsubi  27382  norm3difi  27388  normpar2i  27397  hilablo  27401  shsubcl  27461  hhssabloilem  27502  shsel3  27558  pjsubii  27921  pjssmii  27924  honegsubi  28039  honegneg  28049  hosubneg  28050  hosubdi  28051  honegdi  28052  honegsubdi  28053  honegsubdi2  28054  hosub4  28056  hosubsub4  28061  hosubeq0i  28069  nmopnegi  28208  lnopsubi  28217  lnophdi  28245  lnophmlem2  28260  lnfnsubi  28289  bdophdi  28340  nmoptri2i  28342  superpos  28597  cdj1i  28676  cdj3lem1  28677  psgnfzto1st  29186  qqhval2lem  29353  sgnmul  29931  signswch  29964  signlem0  29990  subfacval2  30423  subfaclim  30424  quad3  30818  fwddifn0  31441  fwddifnp1  31442  rmym1  36518  proot1ex  36798  expgrowth  37556  climneg  38677  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  fourierdlem24  39024  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  2pwp1prm  40041  3exp4mod41  40071  41prothprmlem2  40073  m1expevenALTV  40098  m1expoddALTV  40099  0nodd  41600  altgsumbc  41923  altgsumbcALT  41924
  Copyright terms: Public domain W3C validator