Theorem neg1cn 12330

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 11170	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11532	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2106  ℂcc 11110  1c1 11113  -cneg 11449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450  df-neg 11451

This theorem is referenced by:  m1expcl2  14055  m1expeven  14079  iseraltlem2  15633  iseraltlem3  15634  fsumneg  15737  incexclem  15786  incexc  15787  risefallfac  15972  fallrisefac  15973  fallfac0  15976  0risefac  15986  binomrisefac  15990  n2dvdsm1  16316  m1expo  16322  m1exp1  16323  pwp1fsum  16338  bitsfzo  16380  bezoutlem1  16485  psgnunilem4  19406  m1expaddsub  19407  psgnuni  19408  psgnpmtr  19419  psgn0fv0  19420  psgnsn  19429  psgnprfval1  19431  cnmsgnsubg  21349  cnmsgnbas  21350  cnmsgngrp  21351  psgnghm  21352  psgninv  21354  mdetralt  22330  negcncf  24662  dvmptneg  25707  dvlipcn  25735  lhop2  25756  plysubcl  25960  coesub  25995  dgrsub  26010  quotlem  26037  quotcl2  26039  quotdgr  26040  iaa  26062  dvradcnv  26157  efipi  26207  eulerid  26208  sin2pi  26209  sinmpi  26221  cosmpi  26222  sinppi  26223  cosppi  26224  efif1olem2  26276  logneg  26320  lognegb  26322  logtayl  26392  logtayl2  26394  root1id  26486  root1eq1  26487  root1cj  26488  cxpeq  26489  angneg  26532  ang180lem1  26538  1cubrlem  26570  1cubr  26571  atandm4  26608  atandmtan  26649  atantayl3  26668  leibpi  26671  log2cnv  26673  wilthlem1  26796  wilthlem2  26797  basellem2  26810  basellem5  26813  basellem9  26817  isnsqf  26863  mule1  26876  mumul  26909  musum  26919  ppiub  26931  dchrptlem1  26991  dchrptlem2  26992  lgsneg  27048  lgsdilem  27051  lgsdir2lem3  27054  lgsdir2lem4  27055  lgsdir2  27057  lgsdir  27059  lgsdi  27061  lgsne0  27062  gausslemma2dlem5  27098  gausslemma2d  27101  lgseisenlem1  27102  lgseisenlem2  27103  lgseisenlem4  27105  lgseisen  27106  lgsquadlem1  27107  lgsquadlem2  27108  lgsquadlem3  27109  lgsquad2lem1  27111  lgsquad2lem2  27112  lgsquad3  27114  m1lgs  27115  addsqn2reu  27168  addsqrexnreu  27169  dchrisum0flblem1  27235  rpvmasum2  27239  axlowdimlem13  28467  vcm  30084  nvinvfval  30148  nvmval2  30151  nvmf  30153  nvmdi  30156  nvnegneg  30157  nvpncan2  30161  nvaddsub4  30165  nvm1  30173  nvdif  30174  nvmtri  30179  nvabs  30180  nvge0  30181  nvnd  30196  imsmetlem  30198  smcnlem  30205  vmcn  30207  ipval2  30215  4ipval2  30216  ipval3  30217  dipcj  30222  dip0r  30225  sspmval  30241  lno0  30264  lnosub  30267  ip0i  30333  ipdirilem  30337  ipasslem2  30340  ipasslem10  30347  dipsubdir  30356  hvsubf  30523  hvsubcl  30525  hvsubid  30534  hv2neg  30536  hvm1neg  30540  hvaddsubval  30541  hvsub4  30545  hvaddsub12  30546  hvpncan  30547  hvaddsubass  30549  hvsubass  30552  hvsubdistr1  30557  hvsubdistr2  30558  hvsubsub4i  30567  hvnegdii  30570  hvsubeq0i  30571  hvsubcan2i  30572  hvaddcani  30573  hvsubaddi  30574  hvaddeq0  30577  hvsubcan  30582  hvsubcan2  30583  hvsub0  30584  his2sub  30600  hisubcomi  30612  normlem0  30617  normlem9  30626  normsubi  30649  norm3difi  30655  normpar2i  30664  hilablo  30668  shsubcl  30728  hhssabloilem  30769  shsel3  30823  pjsubii  31186  pjssmii  31189  honegsubi  31304  honegneg  31314  hosubneg  31315  hosubdi  31316  honegdi  31317  honegsubdi  31318  honegsubdi2  31319  hosub4  31321  hosubsub4  31326  hosubeq0i  31334  nmopnegi  31473  lnopsubi  31482  lnophdi  31510  lnophmlem2  31525  lnfnsubi  31554  bdophdi  31605  nmoptri2i  31607  superpos  31862  cdj1i  31941  cdj3lem1  31942  psgnid  32514  psgnfzto1st  32522  cnmsgn0g  32563  altgnsg  32566  qqhval2lem  33247  sgnmul  33827  signswch  33858  signlem0  33884  subfacval2  34464  subfaclim  34465  quad3  34941  fwddifn0  35428  fwddifnp1  35429  gg-negcncf  35452  lcmineqlem1  41200  lcmineqlem2  41201  lcmineqlem8  41207  2xp3dxp2ge1d  41328  negexpidd  41722  rmym1  41976  proot1ex  42245  sqrtcval2  42695  expgrowth  43396  climneg  44625  dirkertrigeqlem1  45113  dirkertrigeqlem3  45115  fourierdlem24  45146  sqwvfourb  45244  fourierswlem  45245  fouriersw  45246  2pwp1prm  46556  3exp4mod41  46583  41prothprmlem2  46585  m1expevenALTV  46614  m1expoddALTV  46615  0nodd  46847  altgsumbc  47117  altgsumbcALT  47118