Theorem neg1cn 12087

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 10929	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11289	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2106  ℂcc 10869  1c1 10872  -cneg 11206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-ltxr 11014  df-sub 11207  df-neg 11208

This theorem is referenced by:  m1expcl2  13804  m1expeven  13830  iseraltlem2  15394  iseraltlem3  15395  fsumneg  15499  incexclem  15548  incexc  15549  risefallfac  15734  fallrisefac  15735  fallfac0  15738  0risefac  15748  binomrisefac  15752  n2dvdsm1  16078  m1expo  16084  m1exp1  16085  pwp1fsum  16100  bitsfzo  16142  bezoutlem1  16247  psgnunilem4  19105  m1expaddsub  19106  psgnuni  19107  psgnpmtr  19118  psgn0fv0  19119  psgnsn  19128  psgnprfval1  19130  cnmsgnsubg  20782  cnmsgnbas  20783  cnmsgngrp  20784  psgnghm  20785  psgninv  20787  mdetralt  21757  negcncf  24085  dvmptneg  25130  dvlipcn  25158  lhop2  25179  plysubcl  25383  coesub  25418  dgrsub  25433  quotlem  25460  quotcl2  25462  quotdgr  25463  iaa  25485  dvradcnv  25580  efipi  25630  eulerid  25631  sin2pi  25632  sinmpi  25644  cosmpi  25645  sinppi  25646  cosppi  25647  efif1olem2  25699  logneg  25743  lognegb  25745  logtayl  25815  logtayl2  25817  root1id  25907  root1eq1  25908  root1cj  25909  cxpeq  25910  angneg  25953  ang180lem1  25959  1cubrlem  25991  1cubr  25992  atandm4  26029  atandmtan  26070  atantayl3  26089  leibpi  26092  log2cnv  26094  wilthlem1  26217  wilthlem2  26218  basellem2  26231  basellem5  26234  basellem9  26238  isnsqf  26284  mule1  26297  mumul  26330  musum  26340  ppiub  26352  dchrptlem1  26412  dchrptlem2  26413  lgsneg  26469  lgsdilem  26472  lgsdir2lem3  26475  lgsdir2lem4  26476  lgsdir2  26478  lgsdir  26480  lgsdi  26482  lgsne0  26483  gausslemma2dlem5  26519  gausslemma2d  26522  lgseisenlem1  26523  lgseisenlem2  26524  lgseisenlem4  26526  lgseisen  26527  lgsquadlem1  26528  lgsquadlem2  26529  lgsquadlem3  26530  lgsquad2lem1  26532  lgsquad2lem2  26533  lgsquad3  26535  m1lgs  26536  addsqn2reu  26589  addsqrexnreu  26590  dchrisum0flblem1  26656  rpvmasum2  26660  axlowdimlem13  27322  vcm  28938  nvinvfval  29002  nvmval2  29005  nvmf  29007  nvmdi  29010  nvnegneg  29011  nvpncan2  29015  nvaddsub4  29019  nvm1  29027  nvdif  29028  nvmtri  29033  nvabs  29034  nvge0  29035  nvnd  29050  imsmetlem  29052  smcnlem  29059  vmcn  29061  ipval2  29069  4ipval2  29070  ipval3  29071  dipcj  29076  dip0r  29079  sspmval  29095  lno0  29118  lnosub  29121  ip0i  29187  ipdirilem  29191  ipasslem2  29194  ipasslem10  29201  dipsubdir  29210  hvsubf  29377  hvsubcl  29379  hvsubid  29388  hv2neg  29390  hvm1neg  29394  hvaddsubval  29395  hvsub4  29399  hvaddsub12  29400  hvpncan  29401  hvaddsubass  29403  hvsubass  29406  hvsubdistr1  29411  hvsubdistr2  29412  hvsubsub4i  29421  hvnegdii  29424  hvsubeq0i  29425  hvsubcan2i  29426  hvaddcani  29427  hvsubaddi  29428  hvaddeq0  29431  hvsubcan  29436  hvsubcan2  29437  hvsub0  29438  his2sub  29454  hisubcomi  29466  normlem0  29471  normlem9  29480  normsubi  29503  norm3difi  29509  normpar2i  29518  hilablo  29522  shsubcl  29582  hhssabloilem  29623  shsel3  29677  pjsubii  30040  pjssmii  30043  honegsubi  30158  honegneg  30168  hosubneg  30169  hosubdi  30170  honegdi  30171  honegsubdi  30172  honegsubdi2  30173  hosub4  30175  hosubsub4  30180  hosubeq0i  30188  nmopnegi  30327  lnopsubi  30336  lnophdi  30364  lnophmlem2  30379  lnfnsubi  30408  bdophdi  30459  nmoptri2i  30461  superpos  30716  cdj1i  30795  cdj3lem1  30796  psgnid  31364  psgnfzto1st  31372  cnmsgn0g  31413  altgnsg  31416  qqhval2lem  31931  sgnmul  32509  signswch  32540  signlem0  32566  subfacval2  33149  subfaclim  33150  quad3  33628  fwddifn0  34466  fwddifnp1  34467  lcmineqlem1  40037  lcmineqlem2  40038  lcmineqlem8  40044  2xp3dxp2ge1d  40162  negexpidd  40504  rmym1  40757  proot1ex  41026  sqrtcval2  41250  expgrowth  41953  climneg  43151  dirkertrigeqlem1  43639  dirkertrigeqlem3  43641  fourierdlem24  43672  sqwvfourb  43770  fourierswlem  43771  fouriersw  43772  2pwp1prm  45041  3exp4mod41  45068  41prothprmlem2  45070  m1expevenALTV  45099  m1expoddALTV  45100  0nodd  45364  altgsumbc  45688  altgsumbcALT  45689