Theorem neg1cn 12203

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 11158	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11526	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2149  ℂcc 11098  1c1 11101  -cneg 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-ltxr 11248  df-sub 11443  df-neg 11444

This theorem is referenced by:  m1expcl2  14121  m1expeven  14145  sgnmul  15144  iseraltlem2  15734  iseraltlem3  15735  fsumneg  15838  incexclem  15890  incexc  15891  risefallfac  16078  fallrisefac  16079  fallfac0  16082  0risefac  16092  binomrisefac  16096  n2dvdsm1  16427  m1expo  16433  m1exp1  16434  pwp1fsum  16449  bitsfzo  16493  bezoutlem1  16597  psgnunilem4  19567  m1expaddsub  19568  psgnuni  19569  psgnpmtr  19580  psgn0fv0  19581  psgnsn  19590  psgnprfval1  19592  cnmsgnsubg  21696  cnmsgnbas  21697  cnmsgngrp  21698  psgnghm  21699  psgninv  21701  mdetralt  22734  negcncf  25050  dvmptneg  26094  dvlipcn  26122  lhop2  26143  plysubcl  26348  coesub  26383  dgrsub  26398  quotlem  26430  quotcl2  26432  quotdgr  26433  iaa  26455  dvradcnv  26550  efipi  26604  eulerid  26605  sin2pi  26606  sinmpi  26618  cosmpi  26619  sinppi  26620  cosppi  26621  efif1olem2  26674  logneg  26719  lognegb  26721  logtayl  26791  logtayl2  26793  root1id  26885  root1eq1  26886  root1cj  26887  cxpeq  26888  angneg  26934  ang180lem1  26940  1cubrlem  26972  1cubr  26973  atandm4  27010  atandmtan  27051  atantayl3  27070  leibpi  27073  log2cnv  27075  wilthlem1  27198  wilthlem2  27199  basellem2  27212  basellem5  27215  basellem9  27219  isnsqf  27265  mule1  27278  mumul  27311  musum  27321  ppiub  27334  dchrptlem1  27394  dchrptlem2  27395  lgsneg  27451  lgsdilem  27454  lgsdir2lem3  27457  lgsdir2lem4  27458  lgsdir2  27460  lgsdir  27462  lgsdi  27464  lgsne0  27465  gausslemma2dlem5  27501  gausslemma2d  27504  lgseisenlem1  27505  lgseisenlem2  27506  lgseisenlem4  27508  lgseisen  27509  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  lgsquad2lem1  27514  lgsquad2lem2  27515  lgsquad3  27517  m1lgs  27518  addsqn2reu  27571  addsqrexnreu  27572  dchrisum0flblem1  27638  rpvmasum2  27642  axlowdimlem13  29245  vcm  30869  nvinvfval  30933  nvmval2  30936  nvmf  30938  nvmdi  30941  nvnegneg  30942  nvpncan2  30946  nvaddsub4  30950  nvm1  30958  nvdif  30959  nvmtri  30964  nvabs  30965  nvge0  30966  nvnd  30981  imsmetlem  30983  smcnlem  30990  vmcn  30992  ipval2  31000  4ipval2  31001  ipval3  31002  dipcj  31007  dip0r  31010  sspmval  31026  lno0  31049  lnosub  31052  ip0i  31118  ipdirilem  31122  ipasslem2  31125  ipasslem10  31132  dipsubdir  31141  hvsubf  31308  hvsubcl  31310  hvsubid  31319  hv2neg  31321  hvm1neg  31325  hvaddsubval  31326  hvsub4  31330  hvaddsub12  31331  hvpncan  31332  hvaddsubass  31334  hvsubass  31337  hvsubdistr1  31342  hvsubdistr2  31343  hvsubsub4i  31352  hvnegdii  31355  hvsubeq0i  31356  hvsubcan2i  31357  hvaddcani  31358  hvsubaddi  31359  hvaddeq0  31362  hvsubcan  31367  hvsubcan2  31368  hvsub0  31369  his2sub  31385  hisubcomi  31397  normlem0  31402  normlem9  31411  normsubi  31434  norm3difi  31440  normpar2i  31449  hilablo  31453  shsubcl  31513  hhssabloilem  31554  shsel3  31608  pjsubii  31971  pjssmii  31974  honegsubi  32089  honegneg  32099  hosubneg  32100  hosubdi  32101  honegdi  32102  honegsubdi  32103  honegsubdi2  32104  hosub4  32106  hosubsub4  32111  hosubeq0i  32119  nmopnegi  32258  lnopsubi  32267  lnophdi  32295  lnophmlem2  32310  lnfnsubi  32339  bdophdi  32390  nmoptri2i  32392  superpos  32647  cdj1i  32726  cdj3lem1  32727  quad3d  33035  psgnid  33358  psgnfzto1st  33366  cnmsgn0g  33407  altgnsg  33410  qqhval2lem  34316  signswch  34893  signlem0  34919  subfacval2  35612  subfaclim  35613  quad3  36095  fwddifn0  36589  fwddifnp1  36590  lcmineqlem1  42720  lcmineqlem2  42721  lcmineqlem8  42727  readvrec  43047  negexpidd  43339  rmym1  43588  proot1ex  43849  sqrtcval2  44294  expgrowth  44971  climneg  46252  dirkertrigeqlem1  46738  dirkertrigeqlem3  46740  fourierdlem24  46771  sqwvfourb  46869  fourierswlem  46870  fouriersw  46871  2pwp1prm  48264  3exp4mod41  48291  41prothprmlem2  48293  m1expevenALTV  48335  m1expoddALTV  48336  0nodd  48858  altgsumbc  49051  altgsumbcALT  49052