Theorem neg1cn 12322

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 11164	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11524	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2107  ℂcc 11104  1c1 11107  -cneg 11441

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  m1expcl2  14047  m1expeven  14071  iseraltlem2  15625  iseraltlem3  15626  fsumneg  15729  incexclem  15778  incexc  15779  risefallfac  15964  fallrisefac  15965  fallfac0  15968  0risefac  15978  binomrisefac  15982  n2dvdsm1  16308  m1expo  16314  m1exp1  16315  pwp1fsum  16330  bitsfzo  16372  bezoutlem1  16477  psgnunilem4  19358  m1expaddsub  19359  psgnuni  19360  psgnpmtr  19371  psgn0fv0  19372  psgnsn  19381  psgnprfval1  19383  cnmsgnsubg  21114  cnmsgnbas  21115  cnmsgngrp  21116  psgnghm  21117  psgninv  21119  mdetralt  22092  negcncf  24420  dvmptneg  25465  dvlipcn  25493  lhop2  25514  plysubcl  25718  coesub  25753  dgrsub  25768  quotlem  25795  quotcl2  25797  quotdgr  25798  iaa  25820  dvradcnv  25915  efipi  25965  eulerid  25966  sin2pi  25967  sinmpi  25979  cosmpi  25980  sinppi  25981  cosppi  25982  efif1olem2  26034  logneg  26078  lognegb  26080  logtayl  26150  logtayl2  26152  root1id  26242  root1eq1  26243  root1cj  26244  cxpeq  26245  angneg  26288  ang180lem1  26294  1cubrlem  26326  1cubr  26327  atandm4  26364  atandmtan  26405  atantayl3  26424  leibpi  26427  log2cnv  26429  wilthlem1  26552  wilthlem2  26553  basellem2  26566  basellem5  26569  basellem9  26573  isnsqf  26619  mule1  26632  mumul  26665  musum  26675  ppiub  26687  dchrptlem1  26747  dchrptlem2  26748  lgsneg  26804  lgsdilem  26807  lgsdir2lem3  26810  lgsdir2lem4  26811  lgsdir2  26813  lgsdir  26815  lgsdi  26817  lgsne0  26818  gausslemma2dlem5  26854  gausslemma2d  26857  lgseisenlem1  26858  lgseisenlem2  26859  lgseisenlem4  26861  lgseisen  26862  lgsquadlem1  26863  lgsquadlem2  26864  lgsquadlem3  26865  lgsquad2lem1  26867  lgsquad2lem2  26868  lgsquad3  26870  m1lgs  26871  addsqn2reu  26924  addsqrexnreu  26925  dchrisum0flblem1  26991  rpvmasum2  26995  axlowdimlem13  28192  vcm  29807  nvinvfval  29871  nvmval2  29874  nvmf  29876  nvmdi  29879  nvnegneg  29880  nvpncan2  29884  nvaddsub4  29888  nvm1  29896  nvdif  29897  nvmtri  29902  nvabs  29903  nvge0  29904  nvnd  29919  imsmetlem  29921  smcnlem  29928  vmcn  29930  ipval2  29938  4ipval2  29939  ipval3  29940  dipcj  29945  dip0r  29948  sspmval  29964  lno0  29987  lnosub  29990  ip0i  30056  ipdirilem  30060  ipasslem2  30063  ipasslem10  30070  dipsubdir  30079  hvsubf  30246  hvsubcl  30248  hvsubid  30257  hv2neg  30259  hvm1neg  30263  hvaddsubval  30264  hvsub4  30268  hvaddsub12  30269  hvpncan  30270  hvaddsubass  30272  hvsubass  30275  hvsubdistr1  30280  hvsubdistr2  30281  hvsubsub4i  30290  hvnegdii  30293  hvsubeq0i  30294  hvsubcan2i  30295  hvaddcani  30296  hvsubaddi  30297  hvaddeq0  30300  hvsubcan  30305  hvsubcan2  30306  hvsub0  30307  his2sub  30323  hisubcomi  30335  normlem0  30340  normlem9  30349  normsubi  30372  norm3difi  30378  normpar2i  30387  hilablo  30391  shsubcl  30451  hhssabloilem  30492  shsel3  30546  pjsubii  30909  pjssmii  30912  honegsubi  31027  honegneg  31037  hosubneg  31038  hosubdi  31039  honegdi  31040  honegsubdi  31041  honegsubdi2  31042  hosub4  31044  hosubsub4  31049  hosubeq0i  31057  nmopnegi  31196  lnopsubi  31205  lnophdi  31233  lnophmlem2  31248  lnfnsubi  31277  bdophdi  31328  nmoptri2i  31330  superpos  31585  cdj1i  31664  cdj3lem1  31665  psgnid  32234  psgnfzto1st  32242  cnmsgn0g  32283  altgnsg  32286  qqhval2lem  32899  sgnmul  33479  signswch  33510  signlem0  33536  subfacval2  34116  subfaclim  34117  quad3  34593  fwddifn0  35074  fwddifnp1  35075  gg-negcncf  35104  lcmineqlem1  40832  lcmineqlem2  40833  lcmineqlem8  40839  2xp3dxp2ge1d  40960  negexpidd  41353  rmym1  41607  proot1ex  41876  sqrtcval2  42326  expgrowth  43027  climneg  44261  dirkertrigeqlem1  44749  dirkertrigeqlem3  44751  fourierdlem24  44782  sqwvfourb  44880  fourierswlem  44881  fouriersw  44882  2pwp1prm  46192  3exp4mod41  46219  41prothprmlem2  46221  m1expevenALTV  46250  m1expoddALTV  46251  0nodd  46515  altgsumbc  46930  altgsumbcALT  46931