Theorem subne0d 11287

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107   ≠ wne 2941  (class class class)co 7260  ℂcc 10816  0cc0 10818   − cmin 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-po 5499  df-so 5500  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-ltxr 10961  df-sub 11153

This theorem is referenced by:  modsumfzodifsn  13608  abssubne0  14972  rlimuni  15203  climuni  15205  evth  24066  dvlem  25003  dvconst  25024  dvid  25025  dvcnp2  25027  dvaddbr  25045  dvmulbr  25046  dvcobr  25053  dvcjbr  25056  dvrec  25062  dvcnvlem  25083  dvferm2lem  25093  taylthlem2  25476  ulmdvlem1  25502  ang180lem4  25905  ang180lem5  25906  ang180  25907  isosctrlem3  25913  isosctr  25914  ssscongptld  25915  affineequivne  25920  angpieqvdlem  25921  angpieqvdlem2  25922  angpined  25923  angpieqvd  25924  chordthmlem  25925  chordthmlem2  25926  heron  25931  asinlem  25961  lgamgulmlem2  26122  lgamgulmlem3  26123  2sqmod  26527  ttgcontlem1  27195  brbtwn2  27216  axcontlem8  27282  subne0nn  31077  signsvtn0  32491  unbdqndv2lem2  34659  bj-bary1lem  35450  bj-bary1lem1  35451  bj-bary1  35452  lcmineqlem11  40017  pellexlem6  40614  jm2.26lem3  40781  areaquad  41005  bcc0  41889  bccm1k  41891  abssubrp  42745  lptre2pt  43113  limclner  43124  climxrre  43223  cnrefiisplem  43302  fperdvper  43392  stoweidlem23  43496  wallispilem4  43541  wallispi  43543  wallispi2lem1  43544  wallispi2lem2  43545  wallispi2  43546  stirlinglem5  43551  fourierdlem4  43584  fourierdlem42  43622  fourierdlem74  43653  fourierdlem75  43654  fouriersw  43704  sigardiv  44306  sigarcol  44309  sharhght  44310  affinecomb1  45978  affinecomb2  45979  1subrec1sub  45981  eenglngeehlnmlem1  46013  eenglngeehlnmlem2  46014  rrx2vlinest  46017  rrx2linest  46018  2itscp  46057  itscnhlinecirc02plem1  46058  itscnhlinecirc02p  46061