Theorem neg1cn 10640

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

Assertion

Ref	Expression
neg1cn	|- -u 1 e. CC

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 9548	. 2 |- 1 e. CC
2	1	negcli 9887	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1802   CCcc 9488   1c1 9491   -ucneg 9806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-po 4786  df-so 4787  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-ltxr 9631  df-sub 9807  df-neg 9808

This theorem is referenced by:  m1expcl2  12162  iseraltlem2  13479  iseraltlem3  13480  fsumneg  13576  incexclem  13622  incexc  13623  bitsfzo  13957  bezoutlem1  14048  psgnunilem4  16391  m1expaddsub  16392  psgnuni  16393  psgnpmtr  16404  psgn0fv0  16405  psgnsn  16414  psgnprfval1  16416  cnmsgnsubg  18480  cnmsgnbas  18481  cnmsgngrp  18482  psgnghm  18483  psgninv  18485  mdetralt  18977  negcncf  21288  dvmptneg  22235  dvlipcn  22261  lhop2  22282  plysubcl  22485  coesub  22519  dgrsub  22534  quotlem  22561  quotcl2  22563  quotdgr  22564  iaa  22586  dvradcnv  22681  efipi  22731  eulerid  22732  sin2pi  22733  sinmpi  22745  cosmpi  22746  sinppi  22747  cosppi  22748  efif1olem2  22795  logneg  22837  lognegb  22839  logtayl  22906  logtayl2  22908  root1id  22993  root1eq1  22994  root1cj  22995  cxpeq  22996  angneg  23000  ang180lem1  23006  1cubrlem  23037  1cubr  23038  atandm4  23075  atandmtan  23116  atantayl3  23135  leibpi  23138  log2cnv  23140  wilthlem1  23207  wilthlem2  23208  basellem2  23220  basellem5  23223  basellem9  23227  isnsqf  23274  mule1  23287  mumul  23320  musum  23332  ppiub  23344  dchrptlem1  23404  dchrptlem2  23405  lgsneg  23459  lgsdilem  23462  lgsdir2lem3  23465  lgsdir2lem4  23466  lgsdir2  23468  lgsdir  23470  lgsdi  23472  lgsne0  23473  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem4  23492  lgseisen  23493  lgsquadlem1  23494  lgsquadlem2  23495  lgsquadlem3  23496  lgsquad2lem1  23498  lgsquad2lem2  23499  lgsquad3  23501  m1lgs  23502  dchrisum0flblem1  23558  rpvmasum2  23562  axlowdimlem13  24122  vcsubdir  25314  vcm  25329  vcnegneg  25332  vcnegsubdi2  25333  vcsub4  25334  nvinvfval  25400  nvmval2  25403  nvzs  25405  nvmf  25406  nvmdi  25410  nvnegneg  25411  nvsubadd  25415  nvpncan2  25416  nvaddsub4  25421  nvnncan  25423  nvm1  25432  nvdif  25433  nvmtri  25439  nvabs  25441  nvge0  25442  nvnd  25459  imsmetlem  25461  smcnlem  25472  vmcn  25474  ipval2  25482  4ipval2  25483  ipval3  25484  dipcj  25492  dip0r  25495  sspmval  25511  lno0  25536  lnosub  25539  ip0i  25605  ipdirilem  25609  ipasslem2  25612  ipasslem10  25619  dipsubdir  25628  hvsubf  25797  hvsubcl  25799  hvsubid  25808  hv2neg  25810  hvm1neg  25814  hvaddsubval  25815  hvsub4  25819  hvaddsub12  25820  hvpncan  25821  hvaddsubass  25823  hvsubass  25826  hvsubdistr1  25831  hvsubdistr2  25832  hvsubsub4i  25841  hvnegdii  25844  hvsubeq0i  25845  hvsubcan2i  25846  hvaddcani  25847  hvsubaddi  25848  hvaddeq0  25851  hvsubcan  25856  hvsubcan2  25857  hvsub0  25858  his2sub  25874  hisubcomi  25886  normlem0  25891  normlem9  25900  normsubi  25923  norm3difi  25929  normpar2i  25938  hilablo  25942  shsubcl  26003  hhssabloi  26043  shsel3  26098  pjsubii  26461  pjssmii  26464  honegsubi  26580  honegneg  26590  hosubneg  26591  hosubdi  26592  honegdi  26593  honegsubdi  26594  honegsubdi2  26595  hosub4  26597  hosubsub4  26602  hosubeq0i  26610  nmopnegi  26749  lnopsubi  26758  lnophdi  26786  lnophmlem2  26801  lnfnsubi  26830  bdophdi  26881  nmoptri2i  26883  superpos  27138  cdj1i  27217  cdj3lem1  27218  qqhval2lem  27828  sgnmul  28347  signswch  28384  signlem0  28410  subfacval2  28497  subfaclim  28498  m1expevenALT  28529  quad3  28890  risefallfac  29114  fallrisefac  29115  fallfac0  29118  0risefac  29128  binomrisefac  29132  rmym1  30839  proot1ex  31130  expgrowth  31209  m1expeven  31509  climneg  31520  dirkertrigeqlem1  31765  dirkertrigeqlem3  31767  fourierdlem24  31798  sqwvfourb  31897  fourierswlem  31898  fouriersw  31899  0nodd  32331  altgsumbc  32649  altgsumbcALT  32650