Theorem divcan1d 12052

Description: A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
divcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
divcld.3	⊢ (𝜑 → 𝐵 ≠ 0)

Assertion

Ref	Expression
divcan1d	⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)

Proof of Theorem divcan1d

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcan1 11939	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
5	1, 2, 3, 4	syl3anc 1368	1 ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100   ≠ wne 2933  (class class class)co 7430  ℂcc 11163  0cc0 11165   · cmul 11170   / cdiv 11928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-po 5598  df-so 5599  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7386  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-div 11929

This theorem is referenced by:  ldiv  12109  ltdiv23  12167  lediv23  12168  recp1lt1  12174  ledivp1  12178  subhalfhalf  12508  xp1d2m1eqxm1d2  12528  div4p1lem1div2  12529  qmulz  12997  iccf1o  13537  ltdifltdiv  13865  bcpasc  14350  sqrtdiv  15291  geo2sum  15898  sqrt2irrlem  16271  dvdsval2  16280  flodddiv4t2lthalf  16439  bitsres  16494  bitsuz  16495  dvdsgcdidd  16559  mulgcddvds  16677  qredeq  16679  isprm6  16736  qmuldeneqnum  16770  hashgcdlem  16811  pcqdiv  16880  pockthlem  16928  prmreclem3  16941  4sqlem5  16965  4sqlem12  16979  4sqlem15  16982  sylow3lem4  19650  odadd1  19868  odadd2  19869  gexexlem  19872  pgpfac1lem3a  20098  pgpfac1lem3  20099  znidomb  21581  znrrg  21585  nmoleub2lem  25155  nmoleub3  25160  i1fmullem  25737  mbfi1fseqlem3  25761  mbfi1fseqlem4  25762  mbfi1fseqlem5  25763  dvcnp2  25963  dvcnp2OLD  25964  dvlip  26040  plydivlem4  26347  cosne0  26579  advlogexp  26705  root1id  26805  cxplogb  26837  ang180lem1  26860  ang180lem3  26862  angpieqvd  26882  chordthmlem  26883  dcubic2  26895  dcubic  26897  dquartlem2  26903  cxploglim2  27030  fsumdvdsdiaglem  27234  logexprlim  27277  bposlem3  27338  lgslem1  27349  gausslemma2dlem1a  27417  lgsquadlem1  27432  2lgslem1a1  27441  log2sumbnd  27596  chpdifbndlem1  27605  selberg4lem1  27612  pntrlog2bndlem3  27631  pntibndlem2  27643  pntlemr  27654  ostth2lem3  27687  ostth2  27689  ostth3  27690  axcontlem7  28927  blocnilem  30760  zringfrac  33460  constrrtcclem  33632  qqhval2lem  33834  cndprobin  34306  itgexpif  34490  faclimlem1  35612  faclimlem3  35614  nn0prpwlem  36082  itg2addnclem3  37421  bfplem1  37570  rrncmslem  37580  rrnequiv  37583  nnproddivdvdsd  41746  lcmineqlem12  41786  3lexlogpow5ineq2  41801  3lexlogpow2ineq1  41804  aks4d1p8  41833  unitscyglem2  41942  pellexlem6  42562  jm2.19  42722  jm2.27c  42736  binomcxplemnotnn0  44101  sineq0ALT  44684  xralrple2  45039  ltdiv23neg  45079  stoweidlem42  45733  stirlinglem3  45767  dirkertrigeq  45792  dirkercncflem2  45795  dirkercncflem4  45797  fourierdlem4  45802  fourierdlem63  45860  fourierdlem65  45862  fourierdlem83  45880  fourierdlem89  45886  fourierdlem90  45887  fourierdlem91  45888  etransclem38  45963  smfmullem1  46482  sigarcol  46555  sharhght  46556  proththd  47256  mod0mul  47988  nn0sumshdiglemA  48088  rrx2vlinest  48210