Theorem divcan2d 11924

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
divcan2d	⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)

Proof of Theorem divcan2d

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7361  ℂcc 11029  0cc0 11031   · cmul 11036   / cdiv 11799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-mulcom 11095  ax-addass 11096  ax-mulass 11097  ax-distr 11098  ax-i2m1 11099  ax-1ne0 11100  ax-1rid 11101  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104  ax-pre-lttri 11105  ax-pre-lttrn 11106  ax-pre-ltadd 11107  ax-pre-mulgt0 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177  df-sub 11371  df-neg 11372  df-div 11800

This theorem is referenced by:  nneo  12581  zeo2  12584  intfracq  13784  discr  14168  hashf1  14385  caurcvgr  15602  iseralt  15613  mertenslem1  15812  fprodle  15924  bpoly4  15987  tanadd  16097  divconjdvds  16247  mod2eq1n2dvds  16279  bitsmod  16368  mulgcd  16480  qredeq  16589  qredeu  16590  prmind2  16617  isprm5  16639  pythagtriplem19  16766  pcprendvds2  16774  pcpremul  16776  pcadd  16822  prmreclem1  16849  4sqlem19  16896  ablfac1lem  20004  pgpfac1lem3  20013  prmirredlem  21432  znrrg  21525  metnrmlem3  24811  lebnumlem3  24923  pcoass  24985  ipcau2  25195  4cphipval2  25203  minveclem3  25390  sca2rab  25474  ovolscalem1  25475  uniioombllem4  25548  uniioombl  25551  itg1mulc  25666  itg2const2  25703  dvrec  25920  dveflem  25944  lhop1  25980  vieta1  26281  elqaalem3  26290  abelthlem8  26410  tangtx  26475  tanregt0  26509  eff1olem  26518  eflogeq  26572  argregt0  26580  argrege0  26581  argimgt0  26582  cxpeq  26728  ang180lem5  26784  lawcoslem1  26786  isosctrlem2  26790  isosctrlem3  26791  heron  26809  dcubic1lem  26814  dcubic2  26815  dcubic1  26816  mcubic  26818  dquartlem1  26822  dquart  26824  quart1lem  26826  quart1  26827  quart  26832  atantayl2  26909  birthdaylem2  26923  ftalem5  27048  basellem3  27054  basellem4  27055  fsumdvdsdiaglem  27154  logexprlim  27197  mersenne  27199  perfectlem2  27202  perfect  27203  bposlem9  27264  lgsqrlem2  27319  lgseisenlem1  27347  lgseisenlem3  27349  lgsquadlem1  27352  lgsquad2lem1  27356  m1lgs  27360  2sqlem8  27398  rplogsumlem1  27456  dchrvmasumiflem2  27474  dchrisum0flblem2  27481  dchrisum0fno1  27483  dchrisum0lem1  27488  mulog2sumlem3  27508  selberglem2  27518  selberg3lem1  27529  selberg4lem1  27532  selberg3r  27541  selberg4r  27542  pntrlog2bndlem2  27550  pntlemg  27570  axsegconlem10  29004  axeuclidlem  29040  quad3d  32832  constrinvcl  33943  cos9thpiminplylem3  33954  oddpwdc  34524  subfacval2  35394  circum  35881  faclimlem1  35950  nn0prpwlem  36529  knoppndvlem19  36743  areacirclem1  37922  areacirclem4  37925  cntotbnd  38010  lcmineqlem23  42384  aks6d1c1p3  42443  aks6d1c2p2  42452  aks6d1c3  42456  aks6d1c2lem4  42460  unitscyglem2  42529  unitscyglem4  42531  oddnumth  42644  sumcubes  42646  zdivgd  42670  dffltz  42955  irrapxlem5  43146  pellexlem2  43150  jm2.22  43315  jm2.20nn  43317  sqrtcval  43960  nzss  44636  binomcxplemnotnn0  44675  oddfl  45603  xralrple3  45695  sumnnodd  45953  limclner  45972  stoweidlem62  46383  stirlinglem1  46395  dirkertrigeqlem2  46420  dirkertrigeqlem3  46421  fourierdlem66  46493  fourierdlem73  46500  fourierdlem87  46514  qndenserrnbllem  46615  hoiqssbllem2  46944  2tceilhalfelfzo1  47655  fmtnoprmfac2lem1  47889  sfprmdvdsmersenne  47926  dfeven4  47961  oddflALTV  47986  nn0onn0exALTV  48022  perfectALTVlem2  48045  perfectALTV  48046  nn0onn0ex  48846  affinecomb2  49026  line2ylem  49074  line2xlem  49076  itscnhlc0yqe  49082  itsclquadb  49099