Theorem neg1cn 12318

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 11271	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11639	1 ⊢ -1 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  ℂcc 11211  1c1 11214   -cneg 11555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8731  df-en 8988  df-dom 8989  df-sdom 8990  df-pnf 11358  df-mnf 11359  df-ltxr 11361  df-sub 11556  df-neg 11557

This theorem is used by:  m1expcl2  14241  m1expeven  14265  sgnmul  15275  iseraltlem2  15865  iseraltlem3  15866  fsumneg  15968  incexclem  16020  incexc  16021  risefallfac  16206  fallrisefac  16207  fallfac0  16209  0risefac  16219  binomrisefac  16223  n2dvdsm1  16554  m1expo  16560  m1exp1  16561  pwp1fsum  16576  bitsfzo  16620  bezoutlem1  16727  psgnunilem4  19726  m1expaddsub  19727  psgnuni  19728  psgnpmtr  19739  psgn0fv0  19740  psgnsn  19749  psgnprfval1  19751  cnmsgnsubg  21898  cnmsgnbas  21899  cnmsgngrp  21900  psgnghm  21901  psgninv  21903  mdetralt  22938  negcncf  25258  dvmptneg  26301  dvlipcn  26329  lhop2  26350  plysubcl  26556  coesub  26591  dgrsub  26606  quotlem  26636  quotcl2  26638  quotdgr  26639  iaaOLD  26667  dvradcnv  26763  efipi  26817  eulerid  26818  sin2pi  26819  sinmpi  26831  cosmpi  26832  sinppi  26833  cosppi  26834  efif1olem2  26886  logneg  26931  lognegb  26933  logtayl  27003  logtayl2  27005  root1id  27097  root1eq1  27098  root1cj  27099  cxpeq  27100  angneg  27146  ang180lem1  27152  1cubrlem  27184  1cubr  27185  atandm4  27222  atandmtan  27263  atantayl3  27282  leibpi  27285  log2cnv  27287  wilthlem1  27410  wilthlem2  27411  basellem2  27424  basellem5  27427  basellem9  27431  isnsqf  27477  mule1  27490  mumul  27523  musum  27533  ppiub  27546  dchrptlem1  27606  dchrptlem2  27607  lgsneg  27663  lgsdilem  27666  lgsdir2lem3  27669  lgsdir2lem4  27670  lgsdir2  27672  lgsdir  27674  lgsdi  27676  lgsne0  27677  gausslemma2dlem5  27713  gausslemma2d  27716  lgseisenlem1  27717  lgseisenlem2  27718  lgseisenlem4  27720  lgseisen  27721  lgsquadlem1  27722  lgsquadlem2  27723  lgsquadlem3  27724  lgsquad2lem1  27726  lgsquad2lem2  27727  lgsquad3  27729  m1lgs  27730  addsqn2reu  27783  addsqrexnreu  27784  dchrisum0flblem1  27850  rpvmasum2  27854  axlowdimlem13  29547  vcm  31193  nvinvfval  31257  nvmval2  31260  nvmf  31262  nvmdi  31265  nvnegneg  31266  nvpncan2  31270  nvaddsub4  31274  nvm1  31282  nvdif  31283  nvmtri  31288  nvabs  31289  nvge0  31290  nvnd  31305  imsmetlem  31307  smcnlem  31314  vmcn  31316  ipval2  31324  4ipval2  31325  ipval3  31326  dipcj  31331  dip0r  31334  sspmval  31350  lno0  31373  lnosub  31376  ip0i  31442  ipdirilem  31446  ipasslem2  31449  ipasslem10  31456  dipsubdir  31465  hvsubf  31632  hvsubcl  31634  hvsubid  31643  hv2neg  31645  hvm1neg  31649  hvaddsubval  31650  hvsub4  31654  hvaddsub12  31655  hvpncan  31656  hvaddsubass  31658  hvsubass  31661  hvsubdistr1  31666  hvsubdistr2  31667  hvsubsub4i  31676  hvnegdii  31679  hvsubeq0i  31680  hvsubcan2i  31681  hvaddcani  31682  hvsubaddi  31683  hvaddeq0  31686  hvsubcan  31691  hvsubcan2  31692  hvsub0  31693  his2sub  31709  hisubcomi  31721  normlem0  31726  normlem9  31735  normsubi  31758  norm3difi  31764  normpar2i  31773  hilablo  31777  shsubcl  31837  hhssabloilem  31878  shsel3  31932  pjsubii  32295  pjssmii  32298  honegsubi  32413  honegneg  32423  hosubneg  32424  hosubdi  32425  honegdi  32426  honegsubdi  32427  honegsubdi2  32428  hosub4  32430  hosubsub4  32435  hosubeq0i  32443  nmopnegi  32582  lnopsubi  32591  lnophdi  32619  lnophmlem2  32634  lnfnsubi  32663  bdophdi  32714  nmoptri2i  32716  superpos  32971  cdj1i  33050  cdj3lem1  33051  quad3d  33397  psgnid  33714  psgnfzto1st  33722  cnmsgn0g  33763  altgnsg  33766  qqhval2lem  34669  signswch  35246  signlem0  35272  subfacval2  36076  subfaclim  36077  quad3  36559  fwddifn0  37059  fwddifnp1  37060  lcmineqlem1  43222  lcmineqlem2  43223  lcmineqlem8  43229  readvrec  43556  negexpidd  43835  rmym1  44085  proot1ex  44341  sqrtcval2  44785  expgrowth  45462  climneg  46764  dirkertrigeqlem1  47250  dirkertrigeqlem3  47252  fourierdlem24  47283  sqwvfourb  47381  fourierswlem  47382  fouriersw  47383  goldratval  48078  2pwp1prm  48816  3exp4mod41  48843  41prothprmlem2  48845  m1expevenALTV  48887  m1expoddALTV  48888  0nodd  49409  altgsumbc  49606  altgsumbcALT  49607