Theorem neg1cn 12380

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 11213	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11577	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2108  ℂcc 11153  1c1 11156  -cneg 11493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494  df-neg 11495

This theorem is referenced by:  m1expcl2  14126  m1expeven  14150  iseraltlem2  15719  iseraltlem3  15720  fsumneg  15823  incexclem  15872  incexc  15873  risefallfac  16060  fallrisefac  16061  fallfac0  16064  0risefac  16074  binomrisefac  16078  n2dvdsm1  16406  m1expo  16412  m1exp1  16413  pwp1fsum  16428  bitsfzo  16472  bezoutlem1  16576  psgnunilem4  19515  m1expaddsub  19516  psgnuni  19517  psgnpmtr  19528  psgn0fv0  19529  psgnsn  19538  psgnprfval1  19540  cnmsgnsubg  21595  cnmsgnbas  21596  cnmsgngrp  21597  psgnghm  21598  psgninv  21600  mdetralt  22614  negcncf  24948  negcncfOLD  24949  dvmptneg  26004  dvlipcn  26033  lhop2  26054  plysubcl  26261  coesub  26296  dgrsub  26312  quotlem  26342  quotcl2  26344  quotdgr  26345  iaa  26367  dvradcnv  26464  efipi  26515  eulerid  26516  sin2pi  26517  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  efif1olem2  26585  logneg  26630  lognegb  26632  logtayl  26702  logtayl2  26704  root1id  26797  root1eq1  26798  root1cj  26799  cxpeq  26800  angneg  26846  ang180lem1  26852  1cubrlem  26884  1cubr  26885  atandm4  26922  atandmtan  26963  atantayl3  26982  leibpi  26985  log2cnv  26987  wilthlem1  27111  wilthlem2  27112  basellem2  27125  basellem5  27128  basellem9  27132  isnsqf  27178  mule1  27191  mumul  27224  musum  27234  ppiub  27248  dchrptlem1  27308  dchrptlem2  27309  lgsneg  27365  lgsdilem  27368  lgsdir2lem3  27371  lgsdir2lem4  27372  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsne0  27379  gausslemma2dlem5  27415  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem1  27428  lgsquad2lem2  27429  lgsquad3  27431  m1lgs  27432  addsqn2reu  27485  addsqrexnreu  27486  dchrisum0flblem1  27552  rpvmasum2  27556  axlowdimlem13  28969  vcm  30595  nvinvfval  30659  nvmval2  30662  nvmf  30664  nvmdi  30667  nvnegneg  30668  nvpncan2  30672  nvaddsub4  30676  nvm1  30684  nvdif  30685  nvmtri  30690  nvabs  30691  nvge0  30692  nvnd  30707  imsmetlem  30709  smcnlem  30716  vmcn  30718  ipval2  30726  4ipval2  30727  ipval3  30728  dipcj  30733  dip0r  30736  sspmval  30752  lno0  30775  lnosub  30778  ip0i  30844  ipdirilem  30848  ipasslem2  30851  ipasslem10  30858  dipsubdir  30867  hvsubf  31034  hvsubcl  31036  hvsubid  31045  hv2neg  31047  hvm1neg  31051  hvaddsubval  31052  hvsub4  31056  hvaddsub12  31057  hvpncan  31058  hvaddsubass  31060  hvsubass  31063  hvsubdistr1  31068  hvsubdistr2  31069  hvsubsub4i  31078  hvnegdii  31081  hvsubeq0i  31082  hvsubcan2i  31083  hvaddcani  31084  hvsubaddi  31085  hvaddeq0  31088  hvsubcan  31093  hvsubcan2  31094  hvsub0  31095  his2sub  31111  hisubcomi  31123  normlem0  31128  normlem9  31137  normsubi  31160  norm3difi  31166  normpar2i  31175  hilablo  31179  shsubcl  31239  hhssabloilem  31280  shsel3  31334  pjsubii  31697  pjssmii  31700  honegsubi  31815  honegneg  31825  hosubneg  31826  hosubdi  31827  honegdi  31828  honegsubdi  31829  honegsubdi2  31830  hosub4  31832  hosubsub4  31837  hosubeq0i  31845  nmopnegi  31984  lnopsubi  31993  lnophdi  32021  lnophmlem2  32036  lnfnsubi  32065  bdophdi  32116  nmoptri2i  32118  superpos  32373  cdj1i  32452  cdj3lem1  32453  quad3d  32754  psgnid  33117  psgnfzto1st  33125  cnmsgn0g  33166  altgnsg  33169  qqhval2lem  33982  sgnmul  34545  signswch  34576  signlem0  34602  subfacval2  35192  subfaclim  35193  quad3  35675  fwddifn0  36165  fwddifnp1  36166  lcmineqlem1  42030  lcmineqlem2  42031  lcmineqlem8  42037  2xp3dxp2ge1d  42242  readvrec  42392  negexpidd  42693  rmym1  42947  proot1ex  43208  sqrtcval2  43655  expgrowth  44354  climneg  45625  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  fourierdlem24  46146  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  2pwp1prm  47576  3exp4mod41  47603  41prothprmlem2  47605  m1expevenALTV  47634  m1expoddALTV  47635  0nodd  48086  altgsumbc  48268  altgsumbcALT  48269