Theorem subne0d 10614

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2140   ≠ wne 2933  (class class class)co 6815  ℂcc 10147  0cc0 10149   − cmin 10479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-po 5188  df-so 5189  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-er 7914  df-en 8125  df-dom 8126  df-sdom 8127  df-pnf 10289  df-mnf 10290  df-ltxr 10292  df-sub 10481

This theorem is referenced by:  modsumfzodifsn  12958  abssubne0  14276  rlimuni  14501  climuni  14503  pwm1geoser  14820  evth  22980  dvlem  23880  dvconst  23900  dvid  23901  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvcobr  23929  dvcjbr  23932  dvrec  23938  dvcnvlem  23959  dvferm2lem  23969  taylthlem2  24348  ulmdvlem1  24374  ang180lem4  24763  ang180lem5  24764  ang180  24765  isosctrlem3  24771  isosctr  24772  ssscongptld  24773  angpieqvdlem  24776  angpieqvdlem2  24777  angpined  24778  angpieqvd  24779  chordthmlem  24780  chordthmlem2  24781  heron  24786  asinlem  24816  lgamgulmlem2  24977  lgamgulmlem3  24978  ttgcontlem1  25986  brbtwn2  26006  axcontlem8  26072  2sqmod  29979  signsvtn0  30978  unbdqndv2lem2  32829  bj-bary1lem  33490  bj-bary1lem1  33491  bj-bary1  33492  pellexlem6  37919  jm2.26lem3  38089  areaquad  38323  bcc0  39060  bccm1k  39062  abssubrp  40005  lptre2pt  40394  limclner  40405  climxrre  40504  cnrefiisplem  40577  fperdvper  40655  stoweidlem23  40762  wallispilem4  40807  wallispi  40809  wallispi2lem1  40810  wallispi2lem2  40811  wallispi2  40812  stirlinglem5  40817  fourierdlem4  40850  fourierdlem42  40888  fourierdlem74  40919  fourierdlem75  40920  fouriersw  40970  sigardiv  41575  sigarcol  41578  sharhght  41579