Theorem neg1cn 12144

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 11096	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11462	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 11036  1c1 11039  -cneg 11378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379  df-neg 11380

This theorem is referenced by:  m1expcl2  14047  m1expeven  14071  iseraltlem2  15645  iseraltlem3  15646  fsumneg  15749  incexclem  15801  incexc  15802  risefallfac  15989  fallrisefac  15990  fallfac0  15993  0risefac  16003  binomrisefac  16007  n2dvdsm1  16338  m1expo  16344  m1exp1  16345  pwp1fsum  16360  bitsfzo  16404  bezoutlem1  16508  psgnunilem4  19472  m1expaddsub  19473  psgnuni  19474  psgnpmtr  19485  psgn0fv0  19486  psgnsn  19495  psgnprfval1  19497  cnmsgnsubg  21557  cnmsgnbas  21558  cnmsgngrp  21559  psgnghm  21560  psgninv  21562  mdetralt  22573  negcncf  24889  dvmptneg  25933  dvlipcn  25961  lhop2  25982  plysubcl  26187  coesub  26222  dgrsub  26237  quotlem  26266  quotcl2  26268  quotdgr  26269  iaa  26291  dvradcnv  26386  efipi  26437  eulerid  26438  sin2pi  26439  sinmpi  26451  cosmpi  26452  sinppi  26453  cosppi  26454  efif1olem2  26507  logneg  26552  lognegb  26554  logtayl  26624  logtayl2  26626  root1id  26718  root1eq1  26719  root1cj  26720  cxpeq  26721  angneg  26767  ang180lem1  26773  1cubrlem  26805  1cubr  26806  atandm4  26843  atandmtan  26884  atantayl3  26903  leibpi  26906  log2cnv  26908  wilthlem1  27031  wilthlem2  27032  basellem2  27045  basellem5  27048  basellem9  27052  isnsqf  27098  mule1  27111  mumul  27144  musum  27154  ppiub  27167  dchrptlem1  27227  dchrptlem2  27228  lgsneg  27284  lgsdilem  27287  lgsdir2lem3  27290  lgsdir2lem4  27291  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsne0  27298  gausslemma2dlem5  27334  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem1  27347  lgsquad2lem2  27348  lgsquad3  27350  m1lgs  27351  addsqn2reu  27404  addsqrexnreu  27405  dchrisum0flblem1  27471  rpvmasum2  27475  axlowdimlem13  29023  vcm  30647  nvinvfval  30711  nvmval2  30714  nvmf  30716  nvmdi  30719  nvnegneg  30720  nvpncan2  30724  nvaddsub4  30728  nvm1  30736  nvdif  30737  nvmtri  30742  nvabs  30743  nvge0  30744  nvnd  30759  imsmetlem  30761  smcnlem  30768  vmcn  30770  ipval2  30778  4ipval2  30779  ipval3  30780  dipcj  30785  dip0r  30788  sspmval  30804  lno0  30827  lnosub  30830  ip0i  30896  ipdirilem  30900  ipasslem2  30903  ipasslem10  30910  dipsubdir  30919  hvsubf  31086  hvsubcl  31088  hvsubid  31097  hv2neg  31099  hvm1neg  31103  hvaddsubval  31104  hvsub4  31108  hvaddsub12  31109  hvpncan  31110  hvaddsubass  31112  hvsubass  31115  hvsubdistr1  31120  hvsubdistr2  31121  hvsubsub4i  31130  hvnegdii  31133  hvsubeq0i  31134  hvsubcan2i  31135  hvaddcani  31136  hvsubaddi  31137  hvaddeq0  31140  hvsubcan  31145  hvsubcan2  31146  hvsub0  31147  his2sub  31163  hisubcomi  31175  normlem0  31180  normlem9  31189  normsubi  31212  norm3difi  31218  normpar2i  31227  hilablo  31231  shsubcl  31291  hhssabloilem  31332  shsel3  31386  pjsubii  31749  pjssmii  31752  honegsubi  31867  honegneg  31877  hosubneg  31878  hosubdi  31879  honegdi  31880  honegsubdi  31881  honegsubdi2  31882  hosub4  31884  hosubsub4  31889  hosubeq0i  31897  nmopnegi  32036  lnopsubi  32045  lnophdi  32073  lnophmlem2  32088  lnfnsubi  32117  bdophdi  32168  nmoptri2i  32170  superpos  32425  cdj1i  32504  cdj3lem1  32505  quad3d  32822  sgnmul  32908  psgnid  33158  psgnfzto1st  33166  cnmsgn0g  33207  altgnsg  33210  qqhval2lem  34125  signswch  34705  signlem0  34731  subfacval2  35369  subfaclim  35370  quad3  35852  fwddifn0  36346  fwddifnp1  36347  lcmineqlem1  42468  lcmineqlem2  42469  lcmineqlem8  42475  readvrec  42794  negexpidd  43114  rmym1  43363  proot1ex  43624  sqrtcval2  44069  expgrowth  44762  climneg  46040  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  fourierdlem24  46559  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  2pwp1prm  48052  3exp4mod41  48079  41prothprmlem2  48081  m1expevenALTV  48123  m1expoddALTV  48124  0nodd  48646  altgsumbc  48828  altgsumbcALT  48829