Theorem neg1cn 11124

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

Step	Hyp	Ref	Expression
1		ax-1cn 9994	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 10349	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 1990  ℂcc 9934  1c1 9937  -cneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079  df-sub 10268  df-neg 10269

This theorem is referenced by:  m1expcl2  12882  m1expeven  12907  iseraltlem2  14413  iseraltlem3  14414  fsumneg  14519  incexclem  14568  incexc  14569  risefallfac  14755  fallrisefac  14756  fallfac0  14759  0risefac  14769  binomrisefac  14773  m1expo  15092  m1exp1  15093  n2dvdsm1  15105  pwp1fsum  15114  bitsfzo  15157  bezoutlem1  15256  psgnunilem4  17917  m1expaddsub  17918  psgnuni  17919  psgnpmtr  17930  psgn0fv0  17931  psgnsn  17940  psgnprfval1  17942  cnmsgnsubg  19923  cnmsgnbas  19924  cnmsgngrp  19925  psgnghm  19926  psgninv  19928  mdetralt  20414  negcncf  22721  dvmptneg  23729  dvlipcn  23757  lhop2  23778  plysubcl  23978  coesub  24013  dgrsub  24028  quotlem  24055  quotcl2  24057  quotdgr  24058  iaa  24080  dvradcnv  24175  efipi  24225  eulerid  24226  sin2pi  24227  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  efif1olem2  24289  logneg  24334  lognegb  24336  logtayl  24406  logtayl2  24408  root1id  24495  root1eq1  24496  root1cj  24497  cxpeq  24498  angneg  24533  ang180lem1  24539  1cubrlem  24568  1cubr  24569  atandm4  24606  atandmtan  24647  atantayl3  24666  leibpi  24669  log2cnv  24671  wilthlem1  24794  wilthlem2  24795  basellem2  24808  basellem5  24811  basellem9  24815  isnsqf  24861  mule1  24874  mumul  24907  musum  24917  ppiub  24929  dchrptlem1  24989  dchrptlem2  24990  lgsneg  25046  lgsdilem  25049  lgsdir2lem3  25052  lgsdir2lem4  25053  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsne0  25060  gausslemma2dlem5  25096  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  lgsquad2lem2  25110  lgsquad3  25112  m1lgs  25113  dchrisum0flblem1  25197  rpvmasum2  25201  axlowdimlem13  25834  vcm  27431  nvinvfval  27495  nvmval2  27498  nvmf  27500  nvmdi  27503  nvnegneg  27504  nvpncan2  27508  nvaddsub4  27512  nvm1  27520  nvdif  27521  nvmtri  27526  nvabs  27527  nvge0  27528  nvnd  27543  imsmetlem  27545  smcnlem  27552  vmcn  27554  ipval2  27562  4ipval2  27563  ipval3  27564  dipcj  27569  dip0r  27572  sspmval  27588  lno0  27611  lnosub  27614  ip0i  27680  ipdirilem  27684  ipasslem2  27687  ipasslem10  27694  dipsubdir  27703  hvsubf  27872  hvsubcl  27874  hvsubid  27883  hv2neg  27885  hvm1neg  27889  hvaddsubval  27890  hvsub4  27894  hvaddsub12  27895  hvpncan  27896  hvaddsubass  27898  hvsubass  27901  hvsubdistr1  27906  hvsubdistr2  27907  hvsubsub4i  27916  hvnegdii  27919  hvsubeq0i  27920  hvsubcan2i  27921  hvaddcani  27922  hvsubaddi  27923  hvaddeq0  27926  hvsubcan  27931  hvsubcan2  27932  hvsub0  27933  his2sub  27949  hisubcomi  27961  normlem0  27966  normlem9  27975  normsubi  27998  norm3difi  28004  normpar2i  28013  hilablo  28017  shsubcl  28077  hhssabloilem  28118  shsel3  28174  pjsubii  28537  pjssmii  28540  honegsubi  28655  honegneg  28665  hosubneg  28666  hosubdi  28667  honegdi  28668  honegsubdi  28669  honegsubdi2  28670  hosub4  28672  hosubsub4  28677  hosubeq0i  28685  nmopnegi  28824  lnopsubi  28833  lnophdi  28861  lnophmlem2  28876  lnfnsubi  28905  bdophdi  28956  nmoptri2i  28958  superpos  29213  cdj1i  29292  cdj3lem1  29293  psgnfzto1st  29855  qqhval2lem  30025  sgnmul  30604  signswch  30638  signlem0  30664  subfacval2  31169  subfaclim  31170  quad3  31564  fwddifn0  32271  fwddifnp1  32272  rmym1  37500  proot1ex  37779  expgrowth  38534  climneg  39842  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  fourierdlem24  40348  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  2pwp1prm  41503  3exp4mod41  41533  41prothprmlem2  41535  m1expevenALTV  41560  m1expoddALTV  41561  0nodd  41810  altgsumbc  42130  altgsumbcALT  42131