Theorem neg1cn 10664

Description: -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
neg1cn

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 9571	. 2
2	1	negcli 9910	1

Syntax hints:  e.wcel 1818  cc 9511  1c1 9514  -ucneg 9829

This theorem is referenced by:  m1expcl2  12188  iseraltlem2  13505  iseraltlem3  13506  fsumneg  13602  incexclem  13648  incexc  13649  bitsfzo  14085  bezoutlem1  14176  psgnunilem4  16522  m1expaddsub  16523  psgnuni  16524  psgnpmtr  16535  psgn0fv0  16536  psgnsn  16545  psgnprfval1  16547  cnmsgnsubg  18613  cnmsgnbas  18614  cnmsgngrp  18615  psgnghm  18616  psgninv  18618  mdetralt  19110  negcncf  21422  dvmptneg  22369  dvlipcn  22395  lhop2  22416  plysubcl  22619  coesub  22654  dgrsub  22669  quotlem  22696  quotcl2  22698  quotdgr  22699  iaa  22721  dvradcnv  22816  efipi  22866  eulerid  22867  sin2pi  22868  sinmpi  22880  cosmpi  22881  sinppi  22882  cosppi  22883  efif1olem2  22930  logneg  22972  lognegb  22974  logtayl  23041  logtayl2  23043  root1id  23128  root1eq1  23129  root1cj  23130  cxpeq  23131  angneg  23135  ang180lem1  23141  1cubrlem  23172  1cubr  23173  atandm4  23210  atandmtan  23251  atantayl3  23270  leibpi  23273  log2cnv  23275  wilthlem1  23342  wilthlem2  23343  basellem2  23355  basellem5  23358  basellem9  23362  isnsqf  23409  mule1  23422  mumul  23455  musum  23467  ppiub  23479  dchrptlem1  23539  dchrptlem2  23540  lgsneg  23594  lgsdilem  23597  lgsdir2lem3  23600  lgsdir2lem4  23601  lgsdir2  23603  lgsdir  23605  lgsdi  23607  lgsne0  23608  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem4  23627  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad2lem1  23633  lgsquad2lem2  23634  lgsquad3  23636  m1lgs  23637  dchrisum0flblem1  23693  rpvmasum2  23697  axlowdimlem13  24257  vcsubdir  25449  vcm  25464  vcnegneg  25467  vcnegsubdi2  25468  vcsub4  25469  nvinvfval  25535  nvmval2  25538  nvzs  25540  nvmf  25541  nvmdi  25545  nvnegneg  25546  nvsubadd  25550  nvpncan2  25551  nvaddsub4  25556  nvnncan  25558  nvm1  25567  nvdif  25568  nvmtri  25574  nvabs  25576  nvge0  25577  nvnd  25594  imsmetlem  25596  smcnlem  25607  vmcn  25609  ipval2  25617  4ipval2  25618  ipval3  25619  dipcj  25627  dip0r  25630  sspmval  25646  lno0  25671  lnosub  25674  ip0i  25740  ipdirilem  25744  ipasslem2  25747  ipasslem10  25754  dipsubdir  25763  hvsubf  25932  hvsubcl  25934  hvsubid  25943  hv2neg  25945  hvm1neg  25949  hvaddsubval  25950  hvsub4  25954  hvaddsub12  25955  hvpncan  25956  hvaddsubass  25958  hvsubass  25961  hvsubdistr1  25966  hvsubdistr2  25967  hvsubsub4i  25976  hvnegdii  25979  hvsubeq0i  25980  hvsubcan2i  25981  hvaddcani  25982  hvsubaddi  25983  hvaddeq0  25986  hvsubcan  25991  hvsubcan2  25992  hvsub0  25993  his2sub  26009  hisubcomi  26021  normlem0  26026  normlem9  26035  normsubi  26058  norm3difi  26064  normpar2i  26073  hilablo  26077  shsubcl  26138  hhssabloi  26178  shsel3  26233  pjsubii  26596  pjssmii  26599  honegsubi  26715  honegneg  26725  hosubneg  26726  hosubdi  26727  honegdi  26728  honegsubdi  26729  honegsubdi2  26730  hosub4  26732  hosubsub4  26737  hosubeq0i  26745  nmopnegi  26884  lnopsubi  26893  lnophdi  26921  lnophmlem2  26936  lnfnsubi  26965  bdophdi  27016  nmoptri2i  27018  superpos  27273  cdj1i  27352  cdj3lem1  27353  qqhval2lem  27962  sgnmul  28481  signswch  28518  signlem0  28544  subfacval2  28631  subfaclim  28632  m1expevenALT  28663  quad3  29024  risefallfac  29146  fallrisefac  29147  fallfac0  29150  0risefac  29160  binomrisefac  29164  rmym1  30871  proot1ex  31161  expgrowth  31240  m1expeven  31585  climneg  31616  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  fourierdlem24  31913  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  0nodd  32498  altgsumbc  32941  altgsumbcALT  32942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654  df-sub 9830  df-neg 9831