Theorem subne0d 11509

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  (class class class)co 7360  ℂcc 11031  0cc0 11033   − cmin 11372

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-sub 11374

This theorem is referenced by:  modsumfzodifsn  13901  abssubne0  15274  rlimuni  15507  climuni  15509  chnccat  18587  chnrev  18588  evth  24948  dvlem  25885  dvconst  25906  dvid  25907  dvcnp2  25909  dvaddbr  25927  dvmulbr  25928  dvcobr  25935  dvcjbr  25938  dvrec  25944  dvcnvlem  25965  dvferm2lem  25975  taylthlem2  26361  ulmdvlem1  26387  ang180lem4  26798  ang180lem5  26799  ang180  26800  isosctrlem3  26806  isosctr  26807  ssscongptld  26808  affineequivne  26813  angpieqvdlem  26814  angpieqvdlem2  26815  angpined  26816  angpieqvd  26817  chordthmlem  26818  chordthmlem2  26819  heron  26824  asinlem  26854  lgamgulmlem2  27015  lgamgulmlem3  27016  2sqmod  27421  ttgcontlem1  28975  brbtwn2  28996  axcontlem8  29062  subne0nn  32918  constrrtll  33927  constrrtlc1  33928  constrrtcclem  33930  constrrtcc  33931  constrfin  33942  constrelextdg2  33943  cos9thpiminplylem3  33980  signsvtn0  34766  unbdqndv2lem2  36831  bj-bary1lem  37685  bj-bary1lem1  37686  bj-bary1  37687  qdiff  37702  lcmineqlem11  42539  pellexlem6  43294  jm2.26lem3  43461  areaquad  43676  bcc0  44799  bccm1k  44801  abssubrp  45738  lptre2pt  46097  limclner  46108  climxrre  46207  cnrefiisplem  46286  fperdvper  46376  stoweidlem23  46480  wallispilem4  46525  wallispi  46527  wallispi2lem1  46528  wallispi2lem2  46529  wallispi2  46530  stirlinglem5  46535  fourierdlem4  46568  fourierdlem42  46606  fourierdlem74  46637  fourierdlem75  46638  fouriersw  46688  sigardiv  47318  sigarcol  47321  sharhght  47322  affinecomb1  49207  affinecomb2  49208  1subrec1sub  49210  eenglngeehlnmlem1  49242  eenglngeehlnmlem2  49243  rrx2vlinest  49246  rrx2linest  49247  2itscp  49286  itscnhlinecirc02plem1  49287  itscnhlinecirc02p  49290