Theorem subne0d 11503

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 11409	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
5	2, 3, 4	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵))
6	5	necon3bid 2969	. 2 ⊢ (𝜑 → ((𝐴 − 𝐵) ≠ 0 ↔ 𝐴 ≠ 𝐵))
7	1, 6	mpbird 257	1 ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7353  ℂcc 11026  0cc0 11028   − cmin 11366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11368

This theorem is referenced by:  modsumfzodifsn  13870  abssubne0  15243  rlimuni  15476  climuni  15478  evth  24875  dvlem  25814  dvconst  25835  dvid  25836  dvcnp2  25838  dvcnp2OLD  25839  dvaddbr  25857  dvmulbr  25858  dvmulbrOLD  25859  dvcobr  25866  dvcobrOLD  25867  dvcjbr  25870  dvrec  25876  dvcnvlem  25897  dvferm2lem  25907  taylthlem2  26299  taylthlem2OLD  26300  ulmdvlem1  26326  ang180lem4  26739  ang180lem5  26740  ang180  26741  isosctrlem3  26747  isosctr  26748  ssscongptld  26749  affineequivne  26754  angpieqvdlem  26755  angpieqvdlem2  26756  angpined  26757  angpieqvd  26758  chordthmlem  26759  chordthmlem2  26760  heron  26765  asinlem  26795  lgamgulmlem2  26957  lgamgulmlem3  26958  2sqmod  27364  ttgcontlem1  28849  brbtwn2  28869  axcontlem8  28935  subne0nn  32785  constrrtll  33717  constrrtlc1  33718  constrrtcclem  33720  constrrtcc  33721  constrfin  33732  constrelextdg2  33733  cos9thpiminplylem3  33770  signsvtn0  34557  unbdqndv2lem2  36503  bj-bary1lem  37303  bj-bary1lem1  37304  bj-bary1  37305  lcmineqlem11  42032  pellexlem6  42827  jm2.26lem3  42994  areaquad  43209  bcc0  44333  bccm1k  44335  abssubrp  45278  lptre2pt  45641  limclner  45652  climxrre  45751  cnrefiisplem  45830  fperdvper  45920  stoweidlem23  46024  wallispilem4  46069  wallispi  46071  wallispi2lem1  46072  wallispi2lem2  46073  wallispi2  46074  stirlinglem5  46079  fourierdlem4  46112  fourierdlem42  46150  fourierdlem74  46181  fourierdlem75  46182  fouriersw  46232  sigardiv  46862  sigarcol  46865  sharhght  46866  affinecomb1  48707  affinecomb2  48708  1subrec1sub  48710  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  rrx2vlinest  48746  rrx2linest  48747  2itscp  48786  itscnhlinecirc02plem1  48787  itscnhlinecirc02p  48790