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

Theorem neg1cn 11314
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 10184 . 2 1 ∈ ℂ
21negcli 10539 1 -1 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2137  cc 10124  1c1 10127  -cneg 10457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-ltxr 10269  df-sub 10458  df-neg 10459
This theorem is referenced by:  m1expcl2  13074  m1expeven  13099  iseraltlem2  14610  iseraltlem3  14611  fsumneg  14716  incexclem  14765  incexc  14766  risefallfac  14952  fallrisefac  14953  fallfac0  14956  0risefac  14966  binomrisefac  14970  m1expo  15292  m1exp1  15293  n2dvdsm1  15305  pwp1fsum  15314  bitsfzo  15357  bezoutlem1  15456  psgnunilem4  18115  m1expaddsub  18116  psgnuni  18117  psgnpmtr  18128  psgn0fv0  18129  psgnsn  18138  psgnprfval1  18140  cnmsgnsubg  20123  cnmsgnbas  20124  cnmsgngrp  20125  psgnghm  20126  psgninv  20128  mdetralt  20614  negcncf  22920  dvmptneg  23926  dvlipcn  23954  lhop2  23975  plysubcl  24175  coesub  24210  dgrsub  24225  quotlem  24252  quotcl2  24254  quotdgr  24255  iaa  24277  dvradcnv  24372  efipi  24422  eulerid  24423  sin2pi  24424  sinmpi  24436  cosmpi  24437  sinppi  24438  cosppi  24439  efif1olem2  24486  logneg  24531  lognegb  24533  logtayl  24603  logtayl2  24605  root1id  24692  root1eq1  24693  root1cj  24694  cxpeq  24695  angneg  24730  ang180lem1  24736  1cubrlem  24765  1cubr  24766  atandm4  24803  atandmtan  24844  atantayl3  24863  leibpi  24866  log2cnv  24868  wilthlem1  24991  wilthlem2  24992  basellem2  25005  basellem5  25008  basellem9  25012  isnsqf  25058  mule1  25071  mumul  25104  musum  25114  ppiub  25126  dchrptlem1  25186  dchrptlem2  25187  lgsneg  25243  lgsdilem  25246  lgsdir2lem3  25249  lgsdir2lem4  25250  lgsdir2  25252  lgsdir  25254  lgsdi  25256  lgsne0  25257  gausslemma2dlem5  25293  gausslemma2d  25296  lgseisenlem1  25297  lgseisenlem2  25298  lgseisenlem4  25300  lgseisen  25301  lgsquadlem1  25302  lgsquadlem2  25303  lgsquadlem3  25304  lgsquad2lem1  25306  lgsquad2lem2  25307  lgsquad3  25309  m1lgs  25310  dchrisum0flblem1  25394  rpvmasum2  25398  axlowdimlem13  26031  vcm  27738  nvinvfval  27802  nvmval2  27805  nvmf  27807  nvmdi  27810  nvnegneg  27811  nvpncan2  27815  nvaddsub4  27819  nvm1  27827  nvdif  27828  nvmtri  27833  nvabs  27834  nvge0  27835  nvnd  27850  imsmetlem  27852  smcnlem  27859  vmcn  27861  ipval2  27869  4ipval2  27870  ipval3  27871  dipcj  27876  dip0r  27879  sspmval  27895  lno0  27918  lnosub  27921  ip0i  27987  ipdirilem  27991  ipasslem2  27994  ipasslem10  28001  dipsubdir  28010  hvsubf  28179  hvsubcl  28181  hvsubid  28190  hv2neg  28192  hvm1neg  28196  hvaddsubval  28197  hvsub4  28201  hvaddsub12  28202  hvpncan  28203  hvaddsubass  28205  hvsubass  28208  hvsubdistr1  28213  hvsubdistr2  28214  hvsubsub4i  28223  hvnegdii  28226  hvsubeq0i  28227  hvsubcan2i  28228  hvaddcani  28229  hvsubaddi  28230  hvaddeq0  28233  hvsubcan  28238  hvsubcan2  28239  hvsub0  28240  his2sub  28256  hisubcomi  28268  normlem0  28273  normlem9  28282  normsubi  28305  norm3difi  28311  normpar2i  28320  hilablo  28324  shsubcl  28384  hhssabloilem  28425  shsel3  28481  pjsubii  28844  pjssmii  28847  honegsubi  28962  honegneg  28972  hosubneg  28973  hosubdi  28974  honegdi  28975  honegsubdi  28976  honegsubdi2  28977  hosub4  28979  hosubsub4  28984  hosubeq0i  28992  nmopnegi  29131  lnopsubi  29140  lnophdi  29168  lnophmlem2  29183  lnfnsubi  29212  bdophdi  29263  nmoptri2i  29265  superpos  29520  cdj1i  29599  cdj3lem1  29600  psgnfzto1st  30162  qqhval2lem  30332  sgnmul  30911  signswch  30945  signlem0  30971  subfacval2  31474  subfaclim  31475  quad3  31869  fwddifn0  32575  fwddifnp1  32576  rmym1  38000  proot1ex  38279  expgrowth  39034  climneg  40343  dirkertrigeqlem1  40816  dirkertrigeqlem3  40818  fourierdlem24  40849  sqwvfourb  40947  fourierswlem  40948  fouriersw  40949  2pwp1prm  42011  3exp4mod41  42041  41prothprmlem2  42043  m1expevenALTV  42068  m1expoddALTV  42069  0nodd  42318  altgsumbc  42638  altgsumbcALT  42639
  Copyright terms: Public domain W3C validator