Theorem neg1cn 12134

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 11088	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11453	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 11028  1c1 11031  -cneg 11369

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  m1expcl2  14012  m1expeven  14036  iseraltlem2  15610  iseraltlem3  15611  fsumneg  15714  incexclem  15763  incexc  15764  risefallfac  15951  fallrisefac  15952  fallfac0  15955  0risefac  15965  binomrisefac  15969  n2dvdsm1  16300  m1expo  16306  m1exp1  16307  pwp1fsum  16322  bitsfzo  16366  bezoutlem1  16470  psgnunilem4  19430  m1expaddsub  19431  psgnuni  19432  psgnpmtr  19443  psgn0fv0  19444  psgnsn  19453  psgnprfval1  19455  cnmsgnsubg  21536  cnmsgnbas  21537  cnmsgngrp  21538  psgnghm  21539  psgninv  21541  mdetralt  22556  negcncf  24875  negcncfOLD  24876  dvmptneg  25930  dvlipcn  25959  lhop2  25980  plysubcl  26187  coesub  26222  dgrsub  26238  quotlem  26268  quotcl2  26270  quotdgr  26271  iaa  26293  dvradcnv  26390  efipi  26442  eulerid  26443  sin2pi  26444  sinmpi  26456  cosmpi  26457  sinppi  26458  cosppi  26459  efif1olem2  26512  logneg  26557  lognegb  26559  logtayl  26629  logtayl2  26631  root1id  26724  root1eq1  26725  root1cj  26726  cxpeq  26727  angneg  26773  ang180lem1  26779  1cubrlem  26811  1cubr  26812  atandm4  26849  atandmtan  26890  atantayl3  26909  leibpi  26912  log2cnv  26914  wilthlem1  27038  wilthlem2  27039  basellem2  27052  basellem5  27055  basellem9  27059  isnsqf  27105  mule1  27118  mumul  27151  musum  27161  ppiub  27175  dchrptlem1  27235  dchrptlem2  27236  lgsneg  27292  lgsdilem  27295  lgsdir2lem3  27298  lgsdir2lem4  27299  lgsdir2  27301  lgsdir  27303  lgsdi  27305  lgsne0  27306  gausslemma2dlem5  27342  gausslemma2d  27345  lgseisenlem1  27346  lgseisenlem2  27347  lgseisenlem4  27349  lgseisen  27350  lgsquadlem1  27351  lgsquadlem2  27352  lgsquadlem3  27353  lgsquad2lem1  27355  lgsquad2lem2  27356  lgsquad3  27358  m1lgs  27359  addsqn2reu  27412  addsqrexnreu  27413  dchrisum0flblem1  27479  rpvmasum2  27483  axlowdimlem13  29031  vcm  30655  nvinvfval  30719  nvmval2  30722  nvmf  30724  nvmdi  30727  nvnegneg  30728  nvpncan2  30732  nvaddsub4  30736  nvm1  30744  nvdif  30745  nvmtri  30750  nvabs  30751  nvge0  30752  nvnd  30767  imsmetlem  30769  smcnlem  30776  vmcn  30778  ipval2  30786  4ipval2  30787  ipval3  30788  dipcj  30793  dip0r  30796  sspmval  30812  lno0  30835  lnosub  30838  ip0i  30904  ipdirilem  30908  ipasslem2  30911  ipasslem10  30918  dipsubdir  30927  hvsubf  31094  hvsubcl  31096  hvsubid  31105  hv2neg  31107  hvm1neg  31111  hvaddsubval  31112  hvsub4  31116  hvaddsub12  31117  hvpncan  31118  hvaddsubass  31120  hvsubass  31123  hvsubdistr1  31128  hvsubdistr2  31129  hvsubsub4i  31138  hvnegdii  31141  hvsubeq0i  31142  hvsubcan2i  31143  hvaddcani  31144  hvsubaddi  31145  hvaddeq0  31148  hvsubcan  31153  hvsubcan2  31154  hvsub0  31155  his2sub  31171  hisubcomi  31183  normlem0  31188  normlem9  31197  normsubi  31220  norm3difi  31226  normpar2i  31235  hilablo  31239  shsubcl  31299  hhssabloilem  31340  shsel3  31394  pjsubii  31757  pjssmii  31760  honegsubi  31875  honegneg  31885  hosubneg  31886  hosubdi  31887  honegdi  31888  honegsubdi  31889  honegsubdi2  31890  hosub4  31892  hosubsub4  31897  hosubeq0i  31905  nmopnegi  32044  lnopsubi  32053  lnophdi  32081  lnophmlem2  32096  lnfnsubi  32125  bdophdi  32176  nmoptri2i  32178  superpos  32433  cdj1i  32512  cdj3lem1  32513  quad3d  32831  sgnmul  32918  psgnid  33181  psgnfzto1st  33189  cnmsgn0g  33230  altgnsg  33233  qqhval2lem  34140  signswch  34720  signlem0  34746  subfacval2  35383  subfaclim  35384  quad3  35866  fwddifn0  36360  fwddifnp1  36361  lcmineqlem1  42351  lcmineqlem2  42352  lcmineqlem8  42358  readvrec  42684  negexpidd  42991  rmym1  43244  proot1ex  43505  sqrtcval2  43950  expgrowth  44643  climneg  45923  dirkertrigeqlem1  46409  dirkertrigeqlem3  46411  fourierdlem24  46442  sqwvfourb  46540  fourierswlem  46541  fouriersw  46542  2pwp1prm  47902  3exp4mod41  47929  41prothprmlem2  47931  m1expevenALTV  47960  m1expoddALTV  47961  0nodd  48483  altgsumbc  48665  altgsumbcALT  48666