Theorem divcan1d 11798

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 11688	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
5	1, 2, 3, 4	syl3anc 1371	1 ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   ≠ wne 2941  (class class class)co 7307  ℂcc 10915  0cc0 10917   · cmul 10922   / cdiv 11678

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993  ax-pre-mulgt0 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-po 5514  df-so 5515  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061  df-sub 11253  df-neg 11254  df-div 11679

This theorem is referenced by:  ldiv  11855  ltdiv23  11912  lediv23  11913  recp1lt1  11919  ledivp1  11923  subhalfhalf  12253  xp1d2m1eqxm1d2  12273  div4p1lem1div2  12274  qmulz  12737  iccf1o  13274  ltdifltdiv  13600  bcpasc  14081  sqrtdiv  15022  geo2sum  15630  sqrt2irrlem  16002  dvdsval2  16011  flodddiv4t2lthalf  16170  bitsres  16225  bitsuz  16226  dvdsgcdidd  16290  mulgcddvds  16405  qredeq  16407  isprm6  16464  qmuldeneqnum  16496  hashgcdlem  16534  pcqdiv  16603  pockthlem  16651  prmreclem3  16664  4sqlem5  16688  4sqlem12  16702  4sqlem15  16705  sylow3lem4  19280  odadd1  19494  odadd2  19495  gexexlem  19498  pgpfac1lem3a  19724  pgpfac1lem3  19725  znidomb  20814  znrrg  20818  nmoleub2lem  24322  nmoleub3  24327  i1fmullem  24903  mbfi1fseqlem3  24927  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  dvcnp2  25129  dvlip  25202  plydivlem4  25501  cosne0  25730  advlogexp  25855  root1id  25952  cxplogb  25981  ang180lem1  26004  ang180lem3  26006  angpieqvd  26026  chordthmlem  26027  dcubic2  26039  dcubic  26041  dquartlem2  26047  cxploglim2  26173  fsumdvdsdiaglem  26377  logexprlim  26418  bposlem3  26479  lgslem1  26490  gausslemma2dlem1a  26558  lgsquadlem1  26573  2lgslem1a1  26582  log2sumbnd  26737  chpdifbndlem1  26746  selberg4lem1  26753  pntrlog2bndlem3  26772  pntibndlem2  26784  pntlemr  26795  ostth2lem3  26828  ostth2  26830  ostth3  26831  axcontlem7  27383  blocnilem  29211  qqhval2lem  31976  cndprobin  32446  itgexpif  32631  faclimlem1  33754  faclimlem3  33756  nn0prpwlem  34556  itg2addnclem3  35874  bfplem1  36024  rrncmslem  36034  rrnequiv  36037  nnproddivdvdsd  40051  lcmineqlem12  40090  3lexlogpow5ineq2  40105  3lexlogpow2ineq1  40108  aks4d1p8  40137  pellexlem6  40693  jm2.19  40853  jm2.27c  40867  binomcxplemnotnn0  42012  sineq0ALT  42595  xralrple2  42941  ltdiv23neg  42982  stoweidlem42  43632  stirlinglem3  43666  dirkertrigeq  43691  dirkercncflem2  43694  dirkercncflem4  43696  fourierdlem4  43701  fourierdlem63  43759  fourierdlem65  43761  fourierdlem83  43779  fourierdlem89  43785  fourierdlem90  43786  fourierdlem91  43787  etransclem38  43862  smfmullem1  44379  sigarcol  44438  sharhght  44439  proththd  45124  mod0mul  45923  nn0sumshdiglemA  46023  rrx2vlinest  46145