Theorem neg1cn 10510

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 9425	. 2
2	1	negcli 9761	1

Syntax hints:  e.wcel 1757  cc 9365  1c1 9368  -ucneg 9681

This theorem is referenced by:  m1expcl2  11972  iseraltlem2  13246  iseraltlem3  13247  fsumneg  13340  incexclem  13385  incexc  13386  bitsfzo  13717  bezoutlem1  13808  psgnunilem4  16089  m1expaddsub  16090  psgnuni  16091  psgnpmtr  16102  psgn0fv0  16103  psgnsn  16112  psgnprfval1  16114  cnmsgnsubg  18100  cnmsgnbas  18101  cnmsgngrp  18102  psgnghm  18103  psgninv  18105  mdetralt  18514  negcncf  20594  dvmptneg  21540  dvlipcn  21566  lhop2  21587  plysubcl  21790  coesub  21824  dgrsub  21839  quotlem  21866  quotcl2  21868  quotdgr  21869  iaa  21891  dvradcnv  21986  efipi  22035  eulerid  22036  sin2pi  22037  sinmpi  22049  cosmpi  22050  sinppi  22051  cosppi  22052  efif1olem2  22099  logneg  22136  lognegb  22138  logtayl  22205  logtayl2  22207  root1id  22292  root1eq1  22293  root1cj  22294  cxpeq  22295  angneg  22299  ang180lem1  22305  1cubrlem  22336  1cubr  22337  atandm4  22374  atandmtan  22415  atantayl3  22434  leibpi  22437  log2cnv  22439  wilthlem1  22506  wilthlem2  22507  basellem2  22519  basellem5  22522  basellem9  22526  isnsqf  22573  mule1  22586  mumul  22619  musum  22631  ppiub  22643  dchrptlem1  22703  dchrptlem2  22704  lgsneg  22758  lgsdilem  22761  lgsdir2lem3  22764  lgsdir2lem4  22765  lgsdir2  22767  lgsdir  22769  lgsdi  22771  lgsne0  22772  lgseisenlem1  22788  lgseisenlem2  22789  lgseisenlem4  22791  lgseisen  22792  lgsquadlem1  22793  lgsquadlem2  22794  lgsquadlem3  22795  lgsquad2lem1  22797  lgsquad2lem2  22798  lgsquad3  22800  m1lgs  22801  dchrisum0flblem1  22857  rpvmasum2  22861  axlowdimlem13  23319  vcsubdir  24053  vcm  24068  vcnegneg  24071  vcnegsubdi2  24072  vcsub4  24073  nvinvfval  24139  nvmval2  24142  nvzs  24144  nvmf  24145  nvmdi  24149  nvnegneg  24150  nvsubadd  24154  nvpncan2  24155  nvaddsub4  24160  nvnncan  24162  nvm1  24171  nvdif  24172  nvmtri  24178  nvabs  24180  nvge0  24181  nvnd  24198  imsmetlem  24200  smcnlem  24211  vmcn  24213  ipval2  24221  4ipval2  24222  ipval3  24223  dipcj  24231  dip0r  24234  sspmval  24250  lno0  24275  lnosub  24278  ip0i  24344  ipdirilem  24348  ipasslem2  24351  ipasslem10  24358  dipsubdir  24367  hvsubf  24536  hvsubcl  24538  hvsubid  24547  hv2neg  24549  hvm1neg  24553  hvaddsubval  24554  hvsub4  24558  hvaddsub12  24559  hvpncan  24560  hvaddsubass  24562  hvsubass  24565  hvsubdistr1  24570  hvsubdistr2  24571  hvsubsub4i  24580  hvnegdii  24583  hvsubeq0i  24584  hvsubcan2i  24585  hvaddcani  24586  hvsubaddi  24587  hvaddeq0  24590  hvsubcan  24595  hvsubcan2  24596  hvsub0  24597  his2sub  24613  hisubcomi  24625  normlem0  24630  normlem9  24639  normsubi  24662  norm3difi  24668  normpar2i  24677  hilablo  24681  shsubcl  24742  hhssabloi  24782  shsel3  24837  pjsubii  25200  pjssmii  25203  honegsubi  25319  honegneg  25329  hosubneg  25330  hosubdi  25331  honegdi  25332  honegsubdi  25333  honegsubdi2  25334  hosub4  25336  hosubsub4  25341  hosubeq0i  25349  nmopnegi  25488  lnopsubi  25497  lnophdi  25525  lnophmlem2  25540  lnfnsubi  25569  bdophdi  25620  nmoptri2i  25622  superpos  25877  cdj1i  25956  cdj3lem1  25957  qqhval2lem  26528  sgnmul  27043  signswch  27080  signlem0  27106  subfacval2  27193  subfaclim  27194  m1expevenALT  27225  risefallfac  27645  fallrisefac  27646  fallfac0  27649  0risefac  27659  binomrisefac  27663  rmym1  29398  proot1ex  29691  expgrowth  29731  m1expeven  29894  climneg  29905  altgsumbc  30871  altgsumbcALT  30872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-po 4723  df-so 4724  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-pnf 9505  df-mnf 9506  df-ltxr 9508  df-sub 9682  df-neg 9683