Theorem neg1cn 12207

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

Assertion

Ref	Expression
neg1cn	⊢ -1 ∈ ℂ

Proof of Theorem neg1cn

Step	Hyp	Ref	Expression
1		ax-1cn 11162	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11530	1 ⊢ -1 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2143  ℂcc 11102  1c1 11105  -cneg 11446

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-sub 11447  df-neg 11448

This theorem is used by:  m1expcl2  14126  m1expeven  14150  sgnmul  15149  iseraltlem2  15739  iseraltlem3  15740  fsumneg  15843  incexclem  15895  incexc  15896  risefallfac  16083  fallrisefac  16084  fallfac0  16086  0risefac  16096  binomrisefac  16100  n2dvdsm1  16431  m1expo  16437  m1exp1  16438  pwp1fsum  16453  bitsfzo  16497  bezoutlem1  16601  psgnunilem4  19571  m1expaddsub  19572  psgnuni  19573  psgnpmtr  19584  psgn0fv0  19585  psgnsn  19594  psgnprfval1  19596  cnmsgnsubg  21736  cnmsgnbas  21737  cnmsgngrp  21738  psgnghm  21739  psgninv  21741  mdetralt  22774  negcncf  25090  dvmptneg  26134  dvlipcn  26162  lhop2  26183  plysubcl  26388  coesub  26423  dgrsub  26438  quotlem  26470  quotcl2  26472  quotdgr  26473  iaa  26497  dvradcnv  26593  efipi  26647  eulerid  26648  sin2pi  26649  sinmpi  26661  cosmpi  26662  sinppi  26663  cosppi  26664  efif1olem2  26717  logneg  26762  lognegb  26764  logtayl  26834  logtayl2  26836  root1id  26928  root1eq1  26929  root1cj  26930  cxpeq  26931  angneg  26977  ang180lem1  26983  1cubrlem  27015  1cubr  27016  atandm4  27053  atandmtan  27094  atantayl3  27113  leibpi  27116  log2cnv  27118  wilthlem1  27241  wilthlem2  27242  basellem2  27255  basellem5  27258  basellem9  27262  isnsqf  27308  mule1  27321  mumul  27354  musum  27364  ppiub  27377  dchrptlem1  27437  dchrptlem2  27438  lgsneg  27494  lgsdilem  27497  lgsdir2lem3  27500  lgsdir2lem4  27501  lgsdir2  27503  lgsdir  27505  lgsdi  27507  lgsne0  27508  gausslemma2dlem5  27544  gausslemma2d  27547  lgseisenlem1  27548  lgseisenlem2  27549  lgseisenlem4  27551  lgseisen  27552  lgsquadlem1  27553  lgsquadlem2  27554  lgsquadlem3  27555  lgsquad2lem1  27557  lgsquad2lem2  27558  lgsquad3  27560  m1lgs  27561  addsqn2reu  27614  addsqrexnreu  27615  dchrisum0flblem1  27681  rpvmasum2  27685  axlowdimlem13  29313  vcm  30937  nvinvfval  31001  nvmval2  31004  nvmf  31006  nvmdi  31009  nvnegneg  31010  nvpncan2  31014  nvaddsub4  31018  nvm1  31026  nvdif  31027  nvmtri  31032  nvabs  31033  nvge0  31034  nvnd  31049  imsmetlem  31051  smcnlem  31058  vmcn  31060  ipval2  31068  4ipval2  31069  ipval3  31070  dipcj  31075  dip0r  31078  sspmval  31094  lno0  31117  lnosub  31120  ip0i  31186  ipdirilem  31190  ipasslem2  31193  ipasslem10  31200  dipsubdir  31209  hvsubf  31376  hvsubcl  31378  hvsubid  31387  hv2neg  31389  hvm1neg  31393  hvaddsubval  31394  hvsub4  31398  hvaddsub12  31399  hvpncan  31400  hvaddsubass  31402  hvsubass  31405  hvsubdistr1  31410  hvsubdistr2  31411  hvsubsub4i  31420  hvnegdii  31423  hvsubeq0i  31424  hvsubcan2i  31425  hvaddcani  31426  hvsubaddi  31427  hvaddeq0  31430  hvsubcan  31435  hvsubcan2  31436  hvsub0  31437  his2sub  31453  hisubcomi  31465  normlem0  31470  normlem9  31479  normsubi  31502  norm3difi  31508  normpar2i  31517  hilablo  31521  shsubcl  31581  hhssabloilem  31622  shsel3  31676  pjsubii  32039  pjssmii  32042  honegsubi  32157  honegneg  32167  hosubneg  32168  hosubdi  32169  honegdi  32170  honegsubdi  32171  honegsubdi2  32172  hosub4  32174  hosubsub4  32179  hosubeq0i  32187  nmopnegi  32326  lnopsubi  32335  lnophdi  32363  lnophmlem2  32378  lnfnsubi  32407  bdophdi  32458  nmoptri2i  32460  superpos  32715  cdj1i  32794  cdj3lem1  32795  quad3d  33103  psgnid  33426  psgnfzto1st  33434  cnmsgn0g  33475  altgnsg  33478  qqhval2lem  34380  signswch  34957  signlem0  34983  subfacval2  35687  subfaclim  35688  quad3  36170  fwddifn0  36664  fwddifnp1  36665  lcmineqlem1  42824  lcmineqlem2  42825  lcmineqlem8  42831  readvrec  43151  negexpidd  43441  rmym1  43690  proot1ex  43951  sqrtcval2  44396  expgrowth  45073  climneg  46354  dirkertrigeqlem1  46840  dirkertrigeqlem3  46842  fourierdlem24  46873  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  2pwp1prm  48369  3exp4mod41  48396  41prothprmlem2  48398  m1expevenALTV  48440  m1expoddALTV  48441  0nodd  48963  altgsumbc  49160  altgsumbcALT  49161