MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neg1cn Structured version   Visualization version   GIF version

Theorem neg1cn 11743
Description: -1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
neg1cn -1 ∈ ℂ

Proof of Theorem neg1cn
StepHypRef Expression
1 ax-1cn 10587 . 2 1 ∈ ℂ
21negcli 10946 1 -1 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  cc 10527  1c1 10530  -cneg 10863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-sub 10864  df-neg 10865
This theorem is referenced by:  m1expcl2  13443  m1expeven  13468  iseraltlem2  15031  iseraltlem3  15032  fsumneg  15134  incexclem  15183  incexc  15184  risefallfac  15370  fallrisefac  15371  fallfac0  15374  0risefac  15384  binomrisefac  15388  n2dvdsm1  15711  m1expo  15718  m1exp1  15719  pwp1fsum  15734  bitsfzo  15776  bezoutlem1  15879  psgnunilem4  18617  m1expaddsub  18618  psgnuni  18619  psgnpmtr  18630  psgn0fv0  18631  psgnsn  18640  psgnprfval1  18642  cnmsgnsubg  20713  cnmsgnbas  20714  cnmsgngrp  20715  psgnghm  20716  psgninv  20718  mdetralt  21209  negcncf  23518  dvmptneg  24555  dvlipcn  24583  lhop2  24604  plysubcl  24804  coesub  24839  dgrsub  24854  quotlem  24881  quotcl2  24883  quotdgr  24884  iaa  24906  dvradcnv  25001  efipi  25051  eulerid  25052  sin2pi  25053  sinmpi  25065  cosmpi  25066  sinppi  25067  cosppi  25068  efif1olem2  25119  logneg  25163  lognegb  25165  logtayl  25235  logtayl2  25237  root1id  25327  root1eq1  25328  root1cj  25329  cxpeq  25330  angneg  25373  ang180lem1  25379  1cubrlem  25411  1cubr  25412  atandm4  25449  atandmtan  25490  atantayl3  25509  leibpi  25512  log2cnv  25514  wilthlem1  25637  wilthlem2  25638  basellem2  25651  basellem5  25654  basellem9  25658  isnsqf  25704  mule1  25717  mumul  25750  musum  25760  ppiub  25772  dchrptlem1  25832  dchrptlem2  25833  lgsneg  25889  lgsdilem  25892  lgsdir2lem3  25895  lgsdir2lem4  25896  lgsdir2  25898  lgsdir  25900  lgsdi  25902  lgsne0  25903  gausslemma2dlem5  25939  gausslemma2d  25942  lgseisenlem1  25943  lgseisenlem2  25944  lgseisenlem4  25946  lgseisen  25947  lgsquadlem1  25948  lgsquadlem2  25949  lgsquadlem3  25950  lgsquad2lem1  25952  lgsquad2lem2  25953  lgsquad3  25955  m1lgs  25956  addsqn2reu  26009  addsqrexnreu  26010  dchrisum0flblem1  26076  rpvmasum2  26080  axlowdimlem13  26732  vcm  28345  nvinvfval  28409  nvmval2  28412  nvmf  28414  nvmdi  28417  nvnegneg  28418  nvpncan2  28422  nvaddsub4  28426  nvm1  28434  nvdif  28435  nvmtri  28440  nvabs  28441  nvge0  28442  nvnd  28457  imsmetlem  28459  smcnlem  28466  vmcn  28468  ipval2  28476  4ipval2  28477  ipval3  28478  dipcj  28483  dip0r  28486  sspmval  28502  lno0  28525  lnosub  28528  ip0i  28594  ipdirilem  28598  ipasslem2  28601  ipasslem10  28608  dipsubdir  28617  hvsubf  28784  hvsubcl  28786  hvsubid  28795  hv2neg  28797  hvm1neg  28801  hvaddsubval  28802  hvsub4  28806  hvaddsub12  28807  hvpncan  28808  hvaddsubass  28810  hvsubass  28813  hvsubdistr1  28818  hvsubdistr2  28819  hvsubsub4i  28828  hvnegdii  28831  hvsubeq0i  28832  hvsubcan2i  28833  hvaddcani  28834  hvsubaddi  28835  hvaddeq0  28838  hvsubcan  28843  hvsubcan2  28844  hvsub0  28845  his2sub  28861  hisubcomi  28873  normlem0  28878  normlem9  28887  normsubi  28910  norm3difi  28916  normpar2i  28925  hilablo  28929  shsubcl  28989  hhssabloilem  29030  shsel3  29084  pjsubii  29447  pjssmii  29450  honegsubi  29565  honegneg  29575  hosubneg  29576  hosubdi  29577  honegdi  29578  honegsubdi  29579  honegsubdi2  29580  hosub4  29582  hosubsub4  29587  hosubeq0i  29595  nmopnegi  29734  lnopsubi  29743  lnophdi  29771  lnophmlem2  29786  lnfnsubi  29815  bdophdi  29866  nmoptri2i  29868  superpos  30123  cdj1i  30202  cdj3lem1  30203  psgnid  30732  psgnfzto1st  30740  cnmsgn0g  30781  altgnsg  30784  qqhval2lem  31215  sgnmul  31793  signswch  31824  signlem0  31850  subfacval2  32427  subfaclim  32428  quad3  32906  fwddifn0  33618  fwddifnp1  33619  negexpidd  39269  rmym1  39522  proot1ex  39791  expgrowth  40657  climneg  41880  dirkertrigeqlem1  42373  dirkertrigeqlem3  42375  fourierdlem24  42406  sqwvfourb  42504  fourierswlem  42505  fouriersw  42506  2pwp1prm  43741  3exp4mod41  43771  41prothprmlem2  43773  m1expevenALTV  43802  m1expoddALTV  43803  0nodd  44067  altgsumbc  44390  altgsumbcALT  44391
  Copyright terms: Public domain W3C validator