Theorem neg1cn 12128

Description: -1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
neg1cn	⊢ -1 ∈ ℂ

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 11082	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11447	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2113  ℂcc 11022  1c1 11025  -cneg 11363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169  df-sub 11364  df-neg 11365

This theorem is referenced by:  m1expcl2  14006  m1expeven  14030  iseraltlem2  15604  iseraltlem3  15605  fsumneg  15708  incexclem  15757  incexc  15758  risefallfac  15945  fallrisefac  15946  fallfac0  15949  0risefac  15959  binomrisefac  15963  n2dvdsm1  16294  m1expo  16300  m1exp1  16301  pwp1fsum  16316  bitsfzo  16360  bezoutlem1  16464  psgnunilem4  19424  m1expaddsub  19425  psgnuni  19426  psgnpmtr  19437  psgn0fv0  19438  psgnsn  19447  psgnprfval1  19449  cnmsgnsubg  21530  cnmsgnbas  21531  cnmsgngrp  21532  psgnghm  21533  psgninv  21535  mdetralt  22550  negcncf  24869  negcncfOLD  24870  dvmptneg  25924  dvlipcn  25953  lhop2  25974  plysubcl  26181  coesub  26216  dgrsub  26232  quotlem  26262  quotcl2  26264  quotdgr  26265  iaa  26287  dvradcnv  26384  efipi  26436  eulerid  26437  sin2pi  26438  sinmpi  26450  cosmpi  26451  sinppi  26452  cosppi  26453  efif1olem2  26506  logneg  26551  lognegb  26553  logtayl  26623  logtayl2  26625  root1id  26718  root1eq1  26719  root1cj  26720  cxpeq  26721  angneg  26767  ang180lem1  26773  1cubrlem  26805  1cubr  26806  atandm4  26843  atandmtan  26884  atantayl3  26903  leibpi  26906  log2cnv  26908  wilthlem1  27032  wilthlem2  27033  basellem2  27046  basellem5  27049  basellem9  27053  isnsqf  27099  mule1  27112  mumul  27145  musum  27155  ppiub  27169  dchrptlem1  27229  dchrptlem2  27230  lgsneg  27286  lgsdilem  27289  lgsdir2lem3  27292  lgsdir2lem4  27293  lgsdir2  27295  lgsdir  27297  lgsdi  27299  lgsne0  27300  gausslemma2dlem5  27336  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  lgsquad2lem1  27349  lgsquad2lem2  27350  lgsquad3  27352  m1lgs  27353  addsqn2reu  27406  addsqrexnreu  27407  dchrisum0flblem1  27473  rpvmasum2  27477  axlowdimlem13  28976  vcm  30600  nvinvfval  30664  nvmval2  30667  nvmf  30669  nvmdi  30672  nvnegneg  30673  nvpncan2  30677  nvaddsub4  30681  nvm1  30689  nvdif  30690  nvmtri  30695  nvabs  30696  nvge0  30697  nvnd  30712  imsmetlem  30714  smcnlem  30721  vmcn  30723  ipval2  30731  4ipval2  30732  ipval3  30733  dipcj  30738  dip0r  30741  sspmval  30757  lno0  30780  lnosub  30783  ip0i  30849  ipdirilem  30853  ipasslem2  30856  ipasslem10  30863  dipsubdir  30872  hvsubf  31039  hvsubcl  31041  hvsubid  31050  hv2neg  31052  hvm1neg  31056  hvaddsubval  31057  hvsub4  31061  hvaddsub12  31062  hvpncan  31063  hvaddsubass  31065  hvsubass  31068  hvsubdistr1  31073  hvsubdistr2  31074  hvsubsub4i  31083  hvnegdii  31086  hvsubeq0i  31087  hvsubcan2i  31088  hvaddcani  31089  hvsubaddi  31090  hvaddeq0  31093  hvsubcan  31098  hvsubcan2  31099  hvsub0  31100  his2sub  31116  hisubcomi  31128  normlem0  31133  normlem9  31142  normsubi  31165  norm3difi  31171  normpar2i  31180  hilablo  31184  shsubcl  31244  hhssabloilem  31285  shsel3  31339  pjsubii  31702  pjssmii  31705  honegsubi  31820  honegneg  31830  hosubneg  31831  hosubdi  31832  honegdi  31833  honegsubdi  31834  honegsubdi2  31835  hosub4  31837  hosubsub4  31842  hosubeq0i  31850  nmopnegi  31989  lnopsubi  31998  lnophdi  32026  lnophmlem2  32041  lnfnsubi  32070  bdophdi  32121  nmoptri2i  32123  superpos  32378  cdj1i  32457  cdj3lem1  32458  quad3d  32778  sgnmul  32865  psgnid  33128  psgnfzto1st  33136  cnmsgn0g  33177  altgnsg  33180  qqhval2lem  34087  signswch  34667  signlem0  34693  subfacval2  35330  subfaclim  35331  quad3  35813  fwddifn0  36307  fwddifnp1  36308  lcmineqlem1  42222  lcmineqlem2  42223  lcmineqlem8  42229  readvrec  42559  negexpidd  42866  rmym1  43119  proot1ex  43380  sqrtcval2  43825  expgrowth  44518  climneg  45798  dirkertrigeqlem1  46284  dirkertrigeqlem3  46286  fourierdlem24  46317  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  2pwp1prm  47777  3exp4mod41  47804  41prothprmlem2  47806  m1expevenALTV  47835  m1expoddALTV  47836  0nodd  48358  altgsumbc  48540  altgsumbcALT  48541