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

Theorem neg1cn 11109
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 9979 . 2 1 ∈ ℂ
21negcli 10334 1 -1 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  cc 9919  1c1 9922  -cneg 10252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-ltxr 10064  df-sub 10253  df-neg 10254
This theorem is referenced by:  m1expcl2  12865  m1expeven  12890  iseraltlem2  14394  iseraltlem3  14395  fsumneg  14500  incexclem  14549  incexc  14550  risefallfac  14736  fallrisefac  14737  fallfac0  14740  0risefac  14750  binomrisefac  14754  m1expo  15073  m1exp1  15074  n2dvdsm1  15086  pwp1fsum  15095  bitsfzo  15138  bezoutlem1  15237  psgnunilem4  17898  m1expaddsub  17899  psgnuni  17900  psgnpmtr  17911  psgn0fv0  17912  psgnsn  17921  psgnprfval1  17923  cnmsgnsubg  19904  cnmsgnbas  19905  cnmsgngrp  19906  psgnghm  19907  psgninv  19909  mdetralt  20395  negcncf  22702  dvmptneg  23710  dvlipcn  23738  lhop2  23759  plysubcl  23959  coesub  23994  dgrsub  24009  quotlem  24036  quotcl2  24038  quotdgr  24039  iaa  24061  dvradcnv  24156  efipi  24206  eulerid  24207  sin2pi  24208  sinmpi  24220  cosmpi  24221  sinppi  24222  cosppi  24223  efif1olem2  24270  logneg  24315  lognegb  24317  logtayl  24387  logtayl2  24389  root1id  24476  root1eq1  24477  root1cj  24478  cxpeq  24479  angneg  24514  ang180lem1  24520  1cubrlem  24549  1cubr  24550  atandm4  24587  atandmtan  24628  atantayl3  24647  leibpi  24650  log2cnv  24652  wilthlem1  24775  wilthlem2  24776  basellem2  24789  basellem5  24792  basellem9  24796  isnsqf  24842  mule1  24855  mumul  24888  musum  24898  ppiub  24910  dchrptlem1  24970  dchrptlem2  24971  lgsneg  25027  lgsdilem  25030  lgsdir2lem3  25033  lgsdir2lem4  25034  lgsdir2  25036  lgsdir  25038  lgsdi  25040  lgsne0  25041  gausslemma2dlem5  25077  gausslemma2d  25080  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem4  25084  lgseisen  25085  lgsquadlem1  25086  lgsquadlem2  25087  lgsquadlem3  25088  lgsquad2lem1  25090  lgsquad2lem2  25091  lgsquad3  25093  m1lgs  25094  dchrisum0flblem1  25178  rpvmasum2  25182  axlowdimlem13  25815  vcm  27401  nvinvfval  27465  nvmval2  27468  nvmf  27470  nvmdi  27473  nvnegneg  27474  nvpncan2  27478  nvaddsub4  27482  nvm1  27490  nvdif  27491  nvmtri  27496  nvabs  27497  nvge0  27498  nvnd  27513  imsmetlem  27515  smcnlem  27522  vmcn  27524  ipval2  27532  4ipval2  27533  ipval3  27534  dipcj  27539  dip0r  27542  sspmval  27558  lno0  27581  lnosub  27584  ip0i  27650  ipdirilem  27654  ipasslem2  27657  ipasslem10  27664  dipsubdir  27673  hvsubf  27842  hvsubcl  27844  hvsubid  27853  hv2neg  27855  hvm1neg  27859  hvaddsubval  27860  hvsub4  27864  hvaddsub12  27865  hvpncan  27866  hvaddsubass  27868  hvsubass  27871  hvsubdistr1  27876  hvsubdistr2  27877  hvsubsub4i  27886  hvnegdii  27889  hvsubeq0i  27890  hvsubcan2i  27891  hvaddcani  27892  hvsubaddi  27893  hvaddeq0  27896  hvsubcan  27901  hvsubcan2  27902  hvsub0  27903  his2sub  27919  hisubcomi  27931  normlem0  27936  normlem9  27945  normsubi  27968  norm3difi  27974  normpar2i  27983  hilablo  27987  shsubcl  28047  hhssabloilem  28088  shsel3  28144  pjsubii  28507  pjssmii  28510  honegsubi  28625  honegneg  28635  hosubneg  28636  hosubdi  28637  honegdi  28638  honegsubdi  28639  honegsubdi2  28640  hosub4  28642  hosubsub4  28647  hosubeq0i  28655  nmopnegi  28794  lnopsubi  28803  lnophdi  28831  lnophmlem2  28846  lnfnsubi  28875  bdophdi  28926  nmoptri2i  28928  superpos  29183  cdj1i  29262  cdj3lem1  29263  psgnfzto1st  29829  qqhval2lem  29999  sgnmul  30578  signswch  30612  signlem0  30638  subfacval2  31143  subfaclim  31144  quad3  31538  fwddifn0  32246  fwddifnp1  32247  rmym1  37319  proot1ex  37598  expgrowth  38354  climneg  39642  dirkertrigeqlem1  40078  dirkertrigeqlem3  40080  fourierdlem24  40111  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  2pwp1prm  41268  3exp4mod41  41298  41prothprmlem2  41300  m1expevenALTV  41325  m1expoddALTV  41326  0nodd  41575  altgsumbc  41895  altgsumbcALT  41896
  Copyright terms: Public domain W3C validator