Theorem neg1cn 10746

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 9628	. 2 |- 1 e. CC
2	1	negcli 9973	1 |- -u 1 e. CC

Syntax hints:   e. wcel 1898   CCcc 9568   1c1 9571   -ucneg 9892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-po 4777  df-so 4778  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-ltxr 9711  df-sub 9893  df-neg 9894

This theorem is referenced by:  m1expcl2  12332  m1expeven  12357  iseraltlem2  13804  iseraltlem3  13805  fsumneg  13903  incexclem  13949  incexc  13950  risefallfac  14132  fallrisefac  14133  fallfac0  14136  0risefac  14146  binomrisefac  14150  bitsfzo  14464  bezoutlem1  14558  psgnunilem4  17193  m1expaddsub  17194  psgnuni  17195  psgnpmtr  17206  psgn0fv0  17207  psgnsn  17216  psgnprfval1  17218  cnmsgnsubg  19200  cnmsgnbas  19201  cnmsgngrp  19202  psgnghm  19203  psgninv  19205  mdetralt  19688  negcncf  22005  dvmptneg  22976  dvlipcn  23002  lhop2  23023  plysubcl  23232  coesub  23267  dgrsub  23282  quotlem  23309  quotcl2  23311  quotdgr  23312  iaa  23337  dvradcnv  23432  efipi  23484  eulerid  23485  sin2pi  23486  sinmpi  23498  cosmpi  23499  sinppi  23500  cosppi  23501  efif1olem2  23548  logneg  23593  lognegb  23595  logtayl  23661  logtayl2  23663  root1id  23750  root1eq1  23751  root1cj  23752  cxpeq  23753  angneg  23788  ang180lem1  23794  1cubrlem  23823  1cubr  23824  atandm4  23861  atandmtan  23902  atantayl3  23921  leibpi  23924  log2cnv  23926  wilthlem1  24049  wilthlem2  24050  basellem2  24064  basellem5  24067  basellem9  24071  isnsqf  24118  mule1  24131  mumul  24164  musum  24176  ppiub  24188  dchrptlem1  24248  dchrptlem2  24249  lgsneg  24303  lgsdilem  24306  lgsdir2lem3  24309  lgsdir2lem4  24310  lgsdir2  24312  lgsdir  24314  lgsdi  24316  lgsne0  24317  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem4  24336  lgseisen  24337  lgsquadlem1  24338  lgsquadlem2  24339  lgsquadlem3  24340  lgsquad2lem1  24342  lgsquad2lem2  24343  lgsquad3  24345  m1lgs  24346  dchrisum0flblem1  24402  rpvmasum2  24406  axlowdimlem13  25040  vcsubdir  26231  vcm  26246  vcnegneg  26249  vcnegsubdi2  26250  vcsub4  26251  nvinvfval  26317  nvmval2  26320  nvzs  26322  nvmf  26323  nvmdi  26327  nvnegneg  26328  nvsubadd  26332  nvpncan2  26333  nvaddsub4  26338  nvnncan  26340  nvm1  26349  nvdif  26350  nvmtri  26356  nvabs  26358  nvge0  26359  nvnd  26376  imsmetlem  26378  smcnlem  26389  vmcn  26391  ipval2  26399  4ipval2  26400  ipval3  26401  dipcj  26409  dip0r  26412  sspmval  26428  lno0  26453  lnosub  26456  ip0i  26522  ipdirilem  26526  ipasslem2  26529  ipasslem10  26536  dipsubdir  26545  hvsubf  26724  hvsubcl  26726  hvsubid  26735  hv2neg  26737  hvm1neg  26741  hvaddsubval  26742  hvsub4  26746  hvaddsub12  26747  hvpncan  26748  hvaddsubass  26750  hvsubass  26753  hvsubdistr1  26758  hvsubdistr2  26759  hvsubsub4i  26768  hvnegdii  26771  hvsubeq0i  26772  hvsubcan2i  26773  hvaddcani  26774  hvsubaddi  26775  hvaddeq0  26778  hvsubcan  26783  hvsubcan2  26784  hvsub0  26785  his2sub  26801  hisubcomi  26813  normlem0  26818  normlem9  26827  normsubi  26850  norm3difi  26856  normpar2i  26865  hilablo  26869  shsubcl  26929  hhssabloi  26969  shsel3  27024  pjsubii  27387  pjssmii  27390  honegsubi  27505  honegneg  27515  hosubneg  27516  hosubdi  27517  honegdi  27518  honegsubdi  27519  honegsubdi2  27520  hosub4  27522  hosubsub4  27527  hosubeq0i  27535  nmopnegi  27674  lnopsubi  27683  lnophdi  27711  lnophmlem2  27726  lnfnsubi  27755  bdophdi  27806  nmoptri2i  27808  superpos  28063  cdj1i  28142  cdj3lem1  28143  psgnfzto1st  28669  qqhval2lem  28836  sgnmul  29463  signswch  29500  signlem0  29526  subfacval2  29960  subfaclim  29961  quad3  30352  fwddifn0  30981  fwddifnp1  30982  rmym1  35829  proot1ex  36124  expgrowth  36729  m1expevenOLD  37756  climneg  37775  dirkertrigeqlem1  38061  dirkertrigeqlem3  38063  fourierdlem24  38094  sqwvfourb  38194  fourierswlem  38195  fouriersw  38196  m1expevenALTV  38912  m1expoddALTV  38913  3exp4mod41  39051  41prothprmlem2  39053  0nodd  40179  altgsumbc  40502  altgsumbcALT  40503