Theorem subne0d 11584

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

Step	Hyp	Ref	Expression
1		subne0d.3	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		negidd.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pncand.2	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		subeq0 11490	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
5	2, 3, 4	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
6	5	necon3bid 2985	. 2 ⊢ (𝜑 → ((𝐴 − 𝐵) ≠ 0 ↔ 𝐴 ≠ 𝐵))
7	1, 6	mpbird 256	1 ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  (class class class)co 7411  ℂcc 11110  0cc0 11112   − cmin 11448

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450

This theorem is referenced by:  modsumfzodifsn  13913  abssubne0  15267  rlimuni  15498  climuni  15500  evth  24699  dvlem  25637  dvconst  25658  dvid  25659  dvcnp2  25661  dvaddbr  25679  dvmulbr  25680  dvcobr  25687  dvcjbr  25690  dvrec  25696  dvcnvlem  25717  dvferm2lem  25727  taylthlem2  26110  ulmdvlem1  26136  ang180lem4  26541  ang180lem5  26542  ang180  26543  isosctrlem3  26549  isosctr  26550  ssscongptld  26551  affineequivne  26556  angpieqvdlem  26557  angpieqvdlem2  26558  angpined  26559  angpieqvd  26560  chordthmlem  26561  chordthmlem2  26562  heron  26567  asinlem  26597  lgamgulmlem2  26758  lgamgulmlem3  26759  2sqmod  27163  ttgcontlem1  28397  brbtwn2  28418  axcontlem8  28484  subne0nn  32282  signsvtn0  33867  gg-dvcnp2  35460  gg-dvmulbr  35461  gg-dvcobr  35462  unbdqndv2lem2  35689  bj-bary1lem  36494  bj-bary1lem1  36495  bj-bary1  36496  lcmineqlem11  41210  pellexlem6  41874  jm2.26lem3  42042  areaquad  42267  bcc0  43401  bccm1k  43403  abssubrp  44284  lptre2pt  44655  limclner  44666  climxrre  44765  cnrefiisplem  44844  fperdvper  44934  stoweidlem23  45038  wallispilem4  45083  wallispi  45085  wallispi2lem1  45086  wallispi2lem2  45087  wallispi2  45088  stirlinglem5  45093  fourierdlem4  45126  fourierdlem42  45164  fourierdlem74  45195  fourierdlem75  45196  fouriersw  45246  sigardiv  45876  sigarcol  45879  sharhght  45880  affinecomb1  47476  affinecomb2  47477  1subrec1sub  47479  eenglngeehlnmlem1  47511  eenglngeehlnmlem2  47512  rrx2vlinest  47515  rrx2linest  47516  2itscp  47555  itscnhlinecirc02plem1  47556  itscnhlinecirc02p  47559