Theorem neg1cn 12139

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 11091	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11457	1 ⊢ -1 ∈ ℂ

Syntax hints:   ∈ wcel 2114  ℂcc 11031  1c1 11034  -cneg 11373

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 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-po 5534  df-so 5535  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-sub 11374  df-neg 11375

This theorem is referenced by:  m1expcl2  14042  m1expeven  14066  iseraltlem2  15640  iseraltlem3  15641  fsumneg  15744  incexclem  15796  incexc  15797  risefallfac  15984  fallrisefac  15985  fallfac0  15988  0risefac  15998  binomrisefac  16002  n2dvdsm1  16333  m1expo  16339  m1exp1  16340  pwp1fsum  16355  bitsfzo  16399  bezoutlem1  16503  psgnunilem4  19467  m1expaddsub  19468  psgnuni  19469  psgnpmtr  19480  psgn0fv0  19481  psgnsn  19490  psgnprfval1  19492  cnmsgnsubg  21571  cnmsgnbas  21572  cnmsgngrp  21573  psgnghm  21574  psgninv  21576  mdetralt  22587  negcncf  24903  dvmptneg  25947  dvlipcn  25975  lhop2  25996  plysubcl  26201  coesub  26236  dgrsub  26251  quotlem  26281  quotcl2  26283  quotdgr  26284  iaa  26306  dvradcnv  26403  efipi  26454  eulerid  26455  sin2pi  26456  sinmpi  26468  cosmpi  26469  sinppi  26470  cosppi  26471  efif1olem2  26524  logneg  26569  lognegb  26571  logtayl  26641  logtayl2  26643  root1id  26735  root1eq1  26736  root1cj  26737  cxpeq  26738  angneg  26784  ang180lem1  26790  1cubrlem  26822  1cubr  26823  atandm4  26860  atandmtan  26901  atantayl3  26920  leibpi  26923  log2cnv  26925  wilthlem1  27049  wilthlem2  27050  basellem2  27063  basellem5  27066  basellem9  27070  isnsqf  27116  mule1  27129  mumul  27162  musum  27172  ppiub  27185  dchrptlem1  27245  dchrptlem2  27246  lgsneg  27302  lgsdilem  27305  lgsdir2lem3  27308  lgsdir2lem4  27309  lgsdir2  27311  lgsdir  27313  lgsdi  27315  lgsne0  27316  gausslemma2dlem5  27352  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem4  27359  lgseisen  27360  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  lgsquad2lem1  27365  lgsquad2lem2  27366  lgsquad3  27368  m1lgs  27369  addsqn2reu  27422  addsqrexnreu  27423  dchrisum0flblem1  27489  rpvmasum2  27493  axlowdimlem13  29041  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  32841  sgnmul  32927  psgnid  33177  psgnfzto1st  33185  cnmsgn0g  33226  altgnsg  33229  qqhval2lem  34145  signswch  34725  signlem0  34751  subfacval2  35389  subfaclim  35390  quad3  35872  fwddifn0  36366  fwddifnp1  36367  lcmineqlem1  42486  lcmineqlem2  42487  lcmineqlem8  42493  readvrec  42812  negexpidd  43132  rmym1  43385  proot1ex  43646  sqrtcval2  44091  expgrowth  44784  climneg  46062  dirkertrigeqlem1  46548  dirkertrigeqlem3  46550  fourierdlem24  46581  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  2pwp1prm  48068  3exp4mod41  48095  41prothprmlem2  48097  m1expevenALTV  48139  m1expoddALTV  48140  0nodd  48662  altgsumbc  48844  altgsumbcALT  48845