Theorem neg1cn 12305

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 11258	. 2 ⊢ 1 ∈ ℂ
2	1	negcli 11626	1 ⊢ -1 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  ℂcc 11198  1c1 11201   -cneg 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  m1expcl2  14228  m1expeven  14252  sgnmul  15260  iseraltlem2  15850  iseraltlem3  15851  fsumneg  15953  incexclem  16005  incexc  16006  risefallfac  16191  fallrisefac  16192  fallfac0  16194  0risefac  16204  binomrisefac  16208  n2dvdsm1  16539  m1expo  16545  m1exp1  16546  pwp1fsum  16561  bitsfzo  16605  bezoutlem1  16712  psgnunilem4  19711  m1expaddsub  19712  psgnuni  19713  psgnpmtr  19724  psgn0fv0  19725  psgnsn  19734  psgnprfval1  19736  cnmsgnsubg  21883  cnmsgnbas  21884  cnmsgngrp  21885  psgnghm  21886  psgninv  21888  mdetralt  22923  negcncf  25243  dvmptneg  26286  dvlipcn  26314  lhop2  26335  plysubcl  26541  coesub  26576  dgrsub  26591  quotlem  26621  quotcl2  26623  quotdgr  26624  iaaOLD  26652  dvradcnv  26748  efipi  26802  eulerid  26803  sin2pi  26804  sinmpi  26816  cosmpi  26817  sinppi  26818  cosppi  26819  efif1olem2  26871  logneg  26916  lognegb  26918  logtayl  26988  logtayl2  26990  root1id  27082  root1eq1  27083  root1cj  27084  cxpeq  27085  angneg  27131  ang180lem1  27137  1cubrlem  27169  1cubr  27170  atandm4  27207  atandmtan  27248  atantayl3  27267  leibpi  27270  log2cnv  27272  wilthlem1  27395  wilthlem2  27396  basellem2  27409  basellem5  27412  basellem9  27416  isnsqf  27462  mule1  27475  mumul  27508  musum  27518  ppiub  27531  dchrptlem1  27591  dchrptlem2  27592  lgsneg  27648  lgsdilem  27651  lgsdir2lem3  27654  lgsdir2lem4  27655  lgsdir2  27657  lgsdir  27659  lgsdi  27661  lgsne0  27662  gausslemma2dlem5  27698  gausslemma2d  27701  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem4  27705  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  lgsquad2lem1  27711  lgsquad2lem2  27712  lgsquad3  27714  m1lgs  27715  addsqn2reu  27768  addsqrexnreu  27769  dchrisum0flblem1  27835  rpvmasum2  27839  axlowdimlem13  29532  vcm  31178  nvinvfval  31242  nvmval2  31245  nvmf  31247  nvmdi  31250  nvnegneg  31251  nvpncan2  31255  nvaddsub4  31259  nvm1  31267  nvdif  31268  nvmtri  31273  nvabs  31274  nvge0  31275  nvnd  31290  imsmetlem  31292  smcnlem  31299  vmcn  31301  ipval2  31309  4ipval2  31310  ipval3  31311  dipcj  31316  dip0r  31319  sspmval  31335  lno0  31358  lnosub  31361  ip0i  31427  ipdirilem  31431  ipasslem2  31434  ipasslem10  31441  dipsubdir  31450  hvsubf  31617  hvsubcl  31619  hvsubid  31628  hv2neg  31630  hvm1neg  31634  hvaddsubval  31635  hvsub4  31639  hvaddsub12  31640  hvpncan  31641  hvaddsubass  31643  hvsubass  31646  hvsubdistr1  31651  hvsubdistr2  31652  hvsubsub4i  31661  hvnegdii  31664  hvsubeq0i  31665  hvsubcan2i  31666  hvaddcani  31667  hvsubaddi  31668  hvaddeq0  31671  hvsubcan  31676  hvsubcan2  31677  hvsub0  31678  his2sub  31694  hisubcomi  31706  normlem0  31711  normlem9  31720  normsubi  31743  norm3difi  31749  normpar2i  31758  hilablo  31762  shsubcl  31822  hhssabloilem  31863  shsel3  31917  pjsubii  32280  pjssmii  32283  honegsubi  32398  honegneg  32408  hosubneg  32409  hosubdi  32410  honegdi  32411  honegsubdi  32412  honegsubdi2  32413  hosub4  32415  hosubsub4  32420  hosubeq0i  32428  nmopnegi  32567  lnopsubi  32576  lnophdi  32604  lnophmlem2  32619  lnfnsubi  32648  bdophdi  32699  nmoptri2i  32701  superpos  32956  cdj1i  33035  cdj3lem1  33036  quad3d  33341  psgnid  33658  psgnfzto1st  33666  cnmsgn0g  33707  altgnsg  33710  qqhval2lem  34613  signswch  35190  signlem0  35216  subfacval2  35952  subfaclim  35953  quad3  36435  fwddifn0  36929  fwddifnp1  36930  lcmineqlem1  43079  lcmineqlem2  43080  lcmineqlem8  43086  readvrec  43413  negexpidd  43692  rmym1  43941  proot1ex  44197  sqrtcval2  44641  expgrowth  45318  climneg  46621  dirkertrigeqlem1  47107  dirkertrigeqlem3  47109  fourierdlem24  47140  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  goldratval  47935  2pwp1prm  48673  3exp4mod41  48700  41prothprmlem2  48702  m1expevenALTV  48744  m1expoddALTV  48745  0nodd  49266  altgsumbc  49463  altgsumbcALT  49464