Theorem neg1cn 12113

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 11067	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11432	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2109  ℂcc 11007  1c1 11010  -cneg 11348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350

This theorem is referenced by:  m1expcl2  13992  m1expeven  14016  iseraltlem2  15590  iseraltlem3  15591  fsumneg  15694  incexclem  15743  incexc  15744  risefallfac  15931  fallrisefac  15932  fallfac0  15935  0risefac  15945  binomrisefac  15949  n2dvdsm1  16280  m1expo  16286  m1exp1  16287  pwp1fsum  16302  bitsfzo  16346  bezoutlem1  16450  psgnunilem4  19376  m1expaddsub  19377  psgnuni  19378  psgnpmtr  19389  psgn0fv0  19390  psgnsn  19399  psgnprfval1  19401  cnmsgnsubg  21484  cnmsgnbas  21485  cnmsgngrp  21486  psgnghm  21487  psgninv  21489  mdetralt  22493  negcncf  24813  negcncfOLD  24814  dvmptneg  25868  dvlipcn  25897  lhop2  25918  plysubcl  26125  coesub  26160  dgrsub  26176  quotlem  26206  quotcl2  26208  quotdgr  26209  iaa  26231  dvradcnv  26328  efipi  26380  eulerid  26381  sin2pi  26382  sinmpi  26394  cosmpi  26395  sinppi  26396  cosppi  26397  efif1olem2  26450  logneg  26495  lognegb  26497  logtayl  26567  logtayl2  26569  root1id  26662  root1eq1  26663  root1cj  26664  cxpeq  26665  angneg  26711  ang180lem1  26717  1cubrlem  26749  1cubr  26750  atandm4  26787  atandmtan  26828  atantayl3  26847  leibpi  26850  log2cnv  26852  wilthlem1  26976  wilthlem2  26977  basellem2  26990  basellem5  26993  basellem9  26997  isnsqf  27043  mule1  27056  mumul  27089  musum  27099  ppiub  27113  dchrptlem1  27173  dchrptlem2  27174  lgsneg  27230  lgsdilem  27233  lgsdir2lem3  27236  lgsdir2lem4  27237  lgsdir2  27239  lgsdir  27241  lgsdi  27243  lgsne0  27244  gausslemma2dlem5  27280  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  lgsquad2lem1  27293  lgsquad2lem2  27294  lgsquad3  27296  m1lgs  27297  addsqn2reu  27350  addsqrexnreu  27351  dchrisum0flblem1  27417  rpvmasum2  27421  axlowdimlem13  28899  vcm  30520  nvinvfval  30584  nvmval2  30587  nvmf  30589  nvmdi  30592  nvnegneg  30593  nvpncan2  30597  nvaddsub4  30601  nvm1  30609  nvdif  30610  nvmtri  30615  nvabs  30616  nvge0  30617  nvnd  30632  imsmetlem  30634  smcnlem  30641  vmcn  30643  ipval2  30651  4ipval2  30652  ipval3  30653  dipcj  30658  dip0r  30661  sspmval  30677  lno0  30700  lnosub  30703  ip0i  30769  ipdirilem  30773  ipasslem2  30776  ipasslem10  30783  dipsubdir  30792  hvsubf  30959  hvsubcl  30961  hvsubid  30970  hv2neg  30972  hvm1neg  30976  hvaddsubval  30977  hvsub4  30981  hvaddsub12  30982  hvpncan  30983  hvaddsubass  30985  hvsubass  30988  hvsubdistr1  30993  hvsubdistr2  30994  hvsubsub4i  31003  hvnegdii  31006  hvsubeq0i  31007  hvsubcan2i  31008  hvaddcani  31009  hvsubaddi  31010  hvaddeq0  31013  hvsubcan  31018  hvsubcan2  31019  hvsub0  31020  his2sub  31036  hisubcomi  31048  normlem0  31053  normlem9  31062  normsubi  31085  norm3difi  31091  normpar2i  31100  hilablo  31104  shsubcl  31164  hhssabloilem  31205  shsel3  31259  pjsubii  31622  pjssmii  31625  honegsubi  31740  honegneg  31750  hosubneg  31751  hosubdi  31752  honegdi  31753  honegsubdi  31754  honegsubdi2  31755  hosub4  31757  hosubsub4  31762  hosubeq0i  31770  nmopnegi  31909  lnopsubi  31918  lnophdi  31946  lnophmlem2  31961  lnfnsubi  31990  bdophdi  32041  nmoptri2i  32043  superpos  32298  cdj1i  32377  cdj3lem1  32378  quad3d  32694  sgnmul  32781  psgnid  33040  psgnfzto1st  33048  cnmsgn0g  33089  altgnsg  33092  qqhval2lem  33954  signswch  34535  signlem0  34561  subfacval2  35170  subfaclim  35171  quad3  35653  fwddifn0  36148  fwddifnp1  36149  lcmineqlem1  42012  lcmineqlem2  42013  lcmineqlem8  42019  readvrec  42345  negexpidd  42665  rmym1  42918  proot1ex  43179  sqrtcval2  43625  expgrowth  44318  climneg  45601  dirkertrigeqlem1  46089  dirkertrigeqlem3  46091  fourierdlem24  46122  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  2pwp1prm  47583  3exp4mod41  47610  41prothprmlem2  47612  m1expevenALTV  47641  m1expoddALTV  47642  0nodd  48164  altgsumbc  48346  altgsumbcALT  48347