Theorem neg1cn 12136

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 11088	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11454	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2119  ℂcc 11028  1c1 11031  -cneg 11370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  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 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7314  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-ltxr 11176  df-sub 11371  df-neg 11372

This theorem is referenced by:  m1expcl2  14039  m1expeven  14063  iseraltlem2  15637  iseraltlem3  15638  fsumneg  15741  incexclem  15793  incexc  15794  risefallfac  15981  fallrisefac  15982  fallfac0  15985  0risefac  15995  binomrisefac  15999  n2dvdsm1  16330  m1expo  16336  m1exp1  16337  pwp1fsum  16352  bitsfzo  16396  bezoutlem1  16500  psgnunilem4  19464  m1expaddsub  19465  psgnuni  19466  psgnpmtr  19477  psgn0fv0  19478  psgnsn  19487  psgnprfval1  19489  cnmsgnsubg  21553  cnmsgnbas  21554  cnmsgngrp  21555  psgnghm  21556  psgninv  21558  mdetralt  22592  negcncf  24908  dvmptneg  25952  dvlipcn  25980  lhop2  26001  plysubcl  26206  coesub  26241  dgrsub  26256  quotlem  26285  quotcl2  26287  quotdgr  26288  iaa  26310  dvradcnv  26405  efipi  26456  eulerid  26457  sin2pi  26458  sinmpi  26470  cosmpi  26471  sinppi  26472  cosppi  26473  efif1olem2  26526  logneg  26571  lognegb  26573  logtayl  26643  logtayl2  26645  root1id  26737  root1eq1  26738  root1cj  26739  cxpeq  26740  angneg  26786  ang180lem1  26792  1cubrlem  26824  1cubr  26825  atandm4  26862  atandmtan  26903  atantayl3  26922  leibpi  26925  log2cnv  26927  wilthlem1  27050  wilthlem2  27051  basellem2  27064  basellem5  27067  basellem9  27071  isnsqf  27117  mule1  27130  mumul  27163  musum  27173  ppiub  27186  dchrptlem1  27246  dchrptlem2  27247  lgsneg  27303  lgsdilem  27306  lgsdir2lem3  27309  lgsdir2lem4  27310  lgsdir2  27312  lgsdir  27314  lgsdi  27316  lgsne0  27317  gausslemma2dlem5  27353  gausslemma2d  27356  lgseisenlem1  27357  lgseisenlem2  27358  lgseisenlem4  27360  lgseisen  27361  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  lgsquad2lem1  27366  lgsquad2lem2  27367  lgsquad3  27369  m1lgs  27370  addsqn2reu  27423  addsqrexnreu  27424  dchrisum0flblem1  27490  rpvmasum2  27494  axlowdimlem13  29042  vcm  30666  nvinvfval  30730  nvmval2  30733  nvmf  30735  nvmdi  30738  nvnegneg  30739  nvpncan2  30743  nvaddsub4  30747  nvm1  30755  nvdif  30756  nvmtri  30761  nvabs  30762  nvge0  30763  nvnd  30778  imsmetlem  30780  smcnlem  30787  vmcn  30789  ipval2  30797  4ipval2  30798  ipval3  30799  dipcj  30804  dip0r  30807  sspmval  30823  lno0  30846  lnosub  30849  ip0i  30915  ipdirilem  30919  ipasslem2  30922  ipasslem10  30929  dipsubdir  30938  hvsubf  31105  hvsubcl  31107  hvsubid  31116  hv2neg  31118  hvm1neg  31122  hvaddsubval  31123  hvsub4  31127  hvaddsub12  31128  hvpncan  31129  hvaddsubass  31131  hvsubass  31134  hvsubdistr1  31139  hvsubdistr2  31140  hvsubsub4i  31149  hvnegdii  31152  hvsubeq0i  31153  hvsubcan2i  31154  hvaddcani  31155  hvsubaddi  31156  hvaddeq0  31159  hvsubcan  31164  hvsubcan2  31165  hvsub0  31166  his2sub  31182  hisubcomi  31194  normlem0  31199  normlem9  31208  normsubi  31231  norm3difi  31237  normpar2i  31246  hilablo  31250  shsubcl  31310  hhssabloilem  31351  shsel3  31405  pjsubii  31768  pjssmii  31771  honegsubi  31886  honegneg  31896  hosubneg  31897  hosubdi  31898  honegdi  31899  honegsubdi  31900  honegsubdi2  31901  hosub4  31903  hosubsub4  31908  hosubeq0i  31916  nmopnegi  32055  lnopsubi  32064  lnophdi  32092  lnophmlem2  32107  lnfnsubi  32136  bdophdi  32187  nmoptri2i  32189  superpos  32444  cdj1i  32523  cdj3lem1  32524  quad3d  32842  sgnmul  32928  psgnid  33179  psgnfzto1st  33187  cnmsgn0g  33228  altgnsg  33231  qqhval2lem  34174  signswch  34754  signlem0  34780  subfacval2  35424  subfaclim  35425  quad3  35907  fwddifn0  36401  fwddifnp1  36402  lcmineqlem1  42523  lcmineqlem2  42524  lcmineqlem8  42530  readvrec  42848  negexpidd  43140  rmym1  43389  proot1ex  43650  sqrtcval2  44095  expgrowth  44788  climneg  46063  dirkertrigeqlem1  46549  dirkertrigeqlem3  46551  fourierdlem24  46582  sqwvfourb  46680  fourierswlem  46681  fouriersw  46682  2pwp1prm  48075  3exp4mod41  48102  41prothprmlem2  48104  m1expevenALTV  48146  m1expoddALTV  48147  0nodd  48669  altgsumbc  48851  altgsumbcALT  48852