Theorem neg1cn 11472

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 10310	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 10670	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2164  ℂcc 10250  1c1 10253  -cneg 10586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-po 5263  df-so 5264  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-ltxr 10396  df-sub 10587  df-neg 10588

This theorem is referenced by:  m1expcl2  13176  m1expeven  13201  iseraltlem2  14790  iseraltlem3  14791  fsumneg  14893  incexclem  14942  incexc  14943  risefallfac  15127  fallrisefac  15128  fallfac0  15131  0risefac  15141  binomrisefac  15145  m1expo  15466  m1exp1  15467  n2dvdsm1  15479  pwp1fsum  15488  bitsfzo  15530  bezoutlem1  15629  psgnunilem4  18268  m1expaddsub  18269  psgnuni  18270  psgnpmtr  18281  psgn0fv0  18282  psgnsn  18291  psgnprfval1  18293  cnmsgnsubg  20282  cnmsgnbas  20283  cnmsgngrp  20284  psgnghm  20285  psgninv  20287  mdetralt  20782  negcncf  23091  dvmptneg  24128  dvlipcn  24156  lhop2  24177  plysubcl  24377  coesub  24412  dgrsub  24427  quotlem  24454  quotcl2  24456  quotdgr  24457  iaa  24479  dvradcnv  24574  efipi  24625  eulerid  24626  sin2pi  24627  sinmpi  24639  cosmpi  24640  sinppi  24641  cosppi  24642  efif1olem2  24689  logneg  24733  lognegb  24735  logtayl  24805  logtayl2  24807  root1id  24897  root1eq1  24898  root1cj  24899  cxpeq  24900  angneg  24943  ang180lem1  24949  1cubrlem  24981  1cubr  24982  atandm4  25019  atandmtan  25060  atantayl3  25079  leibpi  25082  log2cnv  25084  wilthlem1  25207  wilthlem2  25208  basellem2  25221  basellem5  25224  basellem9  25228  isnsqf  25274  mule1  25287  mumul  25320  musum  25330  ppiub  25342  dchrptlem1  25402  dchrptlem2  25403  lgsneg  25459  lgsdilem  25462  lgsdir2lem3  25465  lgsdir2lem4  25466  lgsdir2  25468  lgsdir  25470  lgsdi  25472  lgsne0  25473  gausslemma2dlem5  25509  gausslemma2d  25512  lgseisenlem1  25513  lgseisenlem2  25514  lgseisenlem4  25516  lgseisen  25517  lgsquadlem1  25518  lgsquadlem2  25519  lgsquadlem3  25520  lgsquad2lem1  25522  lgsquad2lem2  25523  lgsquad3  25525  m1lgs  25526  dchrisum0flblem1  25610  rpvmasum2  25614  axlowdimlem13  26253  vcm  27975  nvinvfval  28039  nvmval2  28042  nvmf  28044  nvmdi  28047  nvnegneg  28048  nvpncan2  28052  nvaddsub4  28056  nvm1  28064  nvdif  28065  nvmtri  28070  nvabs  28071  nvge0  28072  nvnd  28087  imsmetlem  28089  smcnlem  28096  vmcn  28098  ipval2  28106  4ipval2  28107  ipval3  28108  dipcj  28113  dip0r  28116  sspmval  28132  lno0  28155  lnosub  28158  ip0i  28224  ipdirilem  28228  ipasslem2  28231  ipasslem10  28238  dipsubdir  28247  hvsubf  28416  hvsubcl  28418  hvsubid  28427  hv2neg  28429  hvm1neg  28433  hvaddsubval  28434  hvsub4  28438  hvaddsub12  28439  hvpncan  28440  hvaddsubass  28442  hvsubass  28445  hvsubdistr1  28450  hvsubdistr2  28451  hvsubsub4i  28460  hvnegdii  28463  hvsubeq0i  28464  hvsubcan2i  28465  hvaddcani  28466  hvsubaddi  28467  hvaddeq0  28470  hvsubcan  28475  hvsubcan2  28476  hvsub0  28477  his2sub  28493  hisubcomi  28505  normlem0  28510  normlem9  28519  normsubi  28542  norm3difi  28548  normpar2i  28557  hilablo  28561  shsubcl  28621  hhssabloilem  28662  shsel3  28718  pjsubii  29081  pjssmii  29084  honegsubi  29199  honegneg  29209  hosubneg  29210  hosubdi  29211  honegdi  29212  honegsubdi  29213  honegsubdi2  29214  hosub4  29216  hosubsub4  29221  hosubeq0i  29229  nmopnegi  29368  lnopsubi  29377  lnophdi  29405  lnophmlem2  29420  lnfnsubi  29449  bdophdi  29500  nmoptri2i  29502  superpos  29757  cdj1i  29836  cdj3lem1  29837  psgnfzto1st  30389  qqhval2lem  30559  sgnmul  31139  signswch  31174  signlem0  31202  subfacval2  31704  subfaclim  31705  quad3  32097  fwddifn0  32799  fwddifnp1  32800  rmym1  38336  proot1ex  38615  expgrowth  39367  climneg  40630  dirkertrigeqlem1  41102  dirkertrigeqlem3  41104  fourierdlem24  41135  sqwvfourb  41233  fourierswlem  41234  fouriersw  41235  2pwp1prm  42326  3exp4mod41  42356  41prothprmlem2  42358  m1expevenALTV  42383  m1expoddALTV  42384  0nodd  42650  altgsumbc  42970  altgsumbcALT  42971