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

Theorem neg1ne0 11970
Description: -1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
neg1ne0 -1 ≠ 0

Proof of Theorem neg1ne0
StepHypRef Expression
1 ax-1cn 10811 . 2 1 ∈ ℂ
2 ax-1ne0 10822 . 2 1 ≠ 0
31, 2negne0i 11177 1 -1 ≠ 0
Colors of variables: wff setvar class
Syntax hints:  wne 2941  0cc0 10753  1c1 10754  -cneg 11087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-ltxr 10896  df-sub 11088  df-neg 11089
This theorem is referenced by:  m1expcl2  13681  m1expeven  13706  iseraltlem2  15270  iseraltlem3  15271  iseralt  15272  m1expo  15960  m1exp1  15961  psgnunilem4  18913  m1expaddsub  18914  psgnuni  18915  cnmsgnsubg  20563  cnmsgngrp  20565  psgninv  20568  iblcnlem1  24709  itgcnlem  24711  dgrsub  25190  coseq00topi  25416  logtayl2  25574  root1eq1  25665  root1cj  25666  cxpeq  25667  angneg  25710  ang180lem1  25716  1cubrlem  25748  atantayl2  25845  basellem2  25988  isnsqf  26041  dchrfi  26160  dchrptlem1  26169  dchrptlem2  26170  lgsne0  26240  lgseisenlem1  26280  lgseisenlem2  26281  lgseisenlem4  26283  lgseisen  26284  lgsquadlem1  26285  lgsquad2lem1  26289  lgsquad3  26292  m1lgs  26293  hvsubcan  29179  hvsubcan2  29180  superpos  30459  sgnnbi  32248  signswch  32276  signstfvcl  32288  fwddifnp1  34230  proot1ex  40757  m1expevenALTV  44800  m1expoddALTV  44801
  Copyright terms: Public domain W3C validator