Theorem neg1cn 10680

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 9580	. 2 |- 1 e. CC
2	1	negcli 9923	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1842   CCcc 9520   1c1 9523   -ucneg 9842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-po 4744  df-so 4745  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-er 7348  df-en 7555  df-dom 7556  df-sdom 7557  df-pnf 9660  df-mnf 9661  df-ltxr 9663  df-sub 9843  df-neg 9844

This theorem is referenced by:  m1expcl2  12232  m1expeven  12257  iseraltlem2  13654  iseraltlem3  13655  fsumneg  13753  incexclem  13799  incexc  13800  risefallfac  13969  fallrisefac  13970  fallfac0  13973  0risefac  13983  binomrisefac  13987  bitsfzo  14294  bezoutlem1  14385  psgnunilem4  16846  m1expaddsub  16847  psgnuni  16848  psgnpmtr  16859  psgn0fv0  16860  psgnsn  16869  psgnprfval1  16871  cnmsgnsubg  18911  cnmsgnbas  18912  cnmsgngrp  18913  psgnghm  18914  psgninv  18916  mdetralt  19402  negcncf  21714  dvmptneg  22661  dvlipcn  22687  lhop2  22708  plysubcl  22911  coesub  22946  dgrsub  22961  quotlem  22988  quotcl2  22990  quotdgr  22991  iaa  23013  dvradcnv  23108  efipi  23158  eulerid  23159  sin2pi  23160  sinmpi  23172  cosmpi  23173  sinppi  23174  cosppi  23175  efif1olem2  23222  logneg  23267  lognegb  23269  logtayl  23335  logtayl2  23337  root1id  23424  root1eq1  23425  root1cj  23426  cxpeq  23427  angneg  23462  ang180lem1  23468  1cubrlem  23497  1cubr  23498  atandm4  23535  atandmtan  23576  atantayl3  23595  leibpi  23598  log2cnv  23600  wilthlem1  23723  wilthlem2  23724  basellem2  23736  basellem5  23739  basellem9  23743  isnsqf  23790  mule1  23803  mumul  23836  musum  23848  ppiub  23860  dchrptlem1  23920  dchrptlem2  23921  lgsneg  23975  lgsdilem  23978  lgsdir2lem3  23981  lgsdir2lem4  23982  lgsdir2  23984  lgsdir  23986  lgsdi  23988  lgsne0  23989  lgseisenlem1  24005  lgseisenlem2  24006  lgseisenlem4  24008  lgseisen  24009  lgsquadlem1  24010  lgsquadlem2  24011  lgsquadlem3  24012  lgsquad2lem1  24014  lgsquad2lem2  24015  lgsquad3  24017  m1lgs  24018  dchrisum0flblem1  24074  rpvmasum2  24078  axlowdimlem13  24674  vcsubdir  25863  vcm  25878  vcnegneg  25881  vcnegsubdi2  25882  vcsub4  25883  nvinvfval  25949  nvmval2  25952  nvzs  25954  nvmf  25955  nvmdi  25959  nvnegneg  25960  nvsubadd  25964  nvpncan2  25965  nvaddsub4  25970  nvnncan  25972  nvm1  25981  nvdif  25982  nvmtri  25988  nvabs  25990  nvge0  25991  nvnd  26008  imsmetlem  26010  smcnlem  26021  vmcn  26023  ipval2  26031  4ipval2  26032  ipval3  26033  dipcj  26041  dip0r  26044  sspmval  26060  lno0  26085  lnosub  26088  ip0i  26154  ipdirilem  26158  ipasslem2  26161  ipasslem10  26168  dipsubdir  26177  hvsubf  26346  hvsubcl  26348  hvsubid  26357  hv2neg  26359  hvm1neg  26363  hvaddsubval  26364  hvsub4  26368  hvaddsub12  26369  hvpncan  26370  hvaddsubass  26372  hvsubass  26375  hvsubdistr1  26380  hvsubdistr2  26381  hvsubsub4i  26390  hvnegdii  26393  hvsubeq0i  26394  hvsubcan2i  26395  hvaddcani  26396  hvsubaddi  26397  hvaddeq0  26400  hvsubcan  26405  hvsubcan2  26406  hvsub0  26407  his2sub  26423  hisubcomi  26435  normlem0  26440  normlem9  26449  normsubi  26472  norm3difi  26478  normpar2i  26487  hilablo  26491  shsubcl  26552  hhssabloi  26592  shsel3  26647  pjsubii  27010  pjssmii  27013  honegsubi  27128  honegneg  27138  hosubneg  27139  hosubdi  27140  honegdi  27141  honegsubdi  27142  honegsubdi2  27143  hosub4  27145  hosubsub4  27150  hosubeq0i  27158  nmopnegi  27297  lnopsubi  27306  lnophdi  27334  lnophmlem2  27349  lnfnsubi  27378  bdophdi  27429  nmoptri2i  27431  superpos  27686  cdj1i  27765  cdj3lem1  27766  qqhval2lem  28414  sgnmul  28987  signswch  29024  signlem0  29050  subfacval2  29484  subfaclim  29485  quad3  29876  fwddifn0  30502  fwddifnp1  30503  rmym1  35232  proot1ex  35525  expgrowth  36088  m1expevenOLD  36953  climneg  36984  dirkertrigeqlem1  37248  dirkertrigeqlem3  37250  fourierdlem24  37281  sqwvfourb  37380  fourierswlem  37381  fouriersw  37382  m1expevenALTV  37730  m1expoddALTV  37731  3exp4mod41  37862  41prothprmlem2  37864  0nodd  38127  altgsumbc  38452  altgsumbcALT  38453