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

Theorem subne0d 10999
Description: Two unequal numbers have nonzero difference. (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
negidd.1 (𝜑𝐴 ∈ ℂ)
pncand.2 (𝜑𝐵 ∈ ℂ)
subne0d.3 (𝜑𝐴𝐵)
Assertion
Ref Expression
subne0d (𝜑 → (𝐴𝐵) ≠ 0)

Proof of Theorem subne0d
StepHypRef Expression
1 subne0d.3 . 2 (𝜑𝐴𝐵)
2 negidd.1 . . . 4 (𝜑𝐴 ∈ ℂ)
3 pncand.2 . . . 4 (𝜑𝐵 ∈ ℂ)
4 subeq0 10905 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴𝐵) = 0 ↔ 𝐴 = 𝐵))
52, 3, 4syl2anc 587 . . 3 (𝜑 → ((𝐴𝐵) = 0 ↔ 𝐴 = 𝐵))
65necon3bid 3034 . 2 (𝜑 → ((𝐴𝐵) ≠ 0 ↔ 𝐴𝐵))
71, 6mpbird 260 1 (𝜑 → (𝐴𝐵) ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2112  wne 2990  (class class class)co 7139  cc 10528  0cc0 10530  cmin 10863
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-ltxr 10673  df-sub 10865
This theorem is referenced by:  modsumfzodifsn  13311  abssubne0  14672  rlimuni  14903  climuni  14905  pwm1geoserOLD  15221  evth  23568  dvlem  24503  dvconst  24524  dvid  24525  dvcnp2  24527  dvaddbr  24545  dvmulbr  24546  dvcobr  24553  dvcjbr  24556  dvrec  24562  dvcnvlem  24583  dvferm2lem  24593  taylthlem2  24973  ulmdvlem1  24999  ang180lem4  25402  ang180lem5  25403  ang180  25404  isosctrlem3  25410  isosctr  25411  ssscongptld  25412  affineequivne  25417  angpieqvdlem  25418  angpieqvdlem2  25419  angpined  25420  angpieqvd  25421  chordthmlem  25422  chordthmlem2  25423  heron  25428  asinlem  25458  lgamgulmlem2  25619  lgamgulmlem3  25620  2sqmod  26024  ttgcontlem1  26683  brbtwn2  26703  axcontlem8  26769  subne0nn  30567  signsvtn0  31954  unbdqndv2lem2  33963  bj-bary1lem  34725  bj-bary1lem1  34726  bj-bary1  34727  lcmineqlem11  39326  pellexlem6  39772  jm2.26lem3  39939  areaquad  40163  bcc0  41041  bccm1k  41043  abssubrp  41903  lptre2pt  42279  limclner  42290  climxrre  42389  cnrefiisplem  42468  fperdvper  42558  stoweidlem23  42662  wallispilem4  42707  wallispi  42709  wallispi2lem1  42710  wallispi2lem2  42711  wallispi2  42712  stirlinglem5  42717  fourierdlem4  42750  fourierdlem42  42788  fourierdlem74  42819  fourierdlem75  42820  fouriersw  42870  sigardiv  43472  sigarcol  43475  sharhght  43476  affinecomb1  45113  affinecomb2  45114  1subrec1sub  45116  eenglngeehlnmlem1  45148  eenglngeehlnmlem2  45149  rrx2vlinest  45152  rrx2linest  45153  2itscp  45192  itscnhlinecirc02plem1  45193  itscnhlinecirc02p  45196
  Copyright terms: Public domain W3C validator