Theorem divcan2d 11920

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7353  ℂcc 11026  0cc0 11028   · cmul 11033   / cdiv 11795

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-div 11796

This theorem is referenced by:  nneo  12578  zeo2  12581  intfracq  13781  discr  14165  hashf1  14382  caurcvgr  15599  iseralt  15610  mertenslem1  15809  fprodle  15921  bpoly4  15984  tanadd  16094  divconjdvds  16244  mod2eq1n2dvds  16276  bitsmod  16365  mulgcd  16477  qredeq  16586  qredeu  16587  prmind2  16614  isprm5  16636  pythagtriplem19  16763  pcprendvds2  16771  pcpremul  16773  pcadd  16819  prmreclem1  16846  4sqlem19  16893  ablfac1lem  19967  pgpfac1lem3  19976  prmirredlem  21397  znrrg  21490  metnrmlem3  24766  lebnumlem3  24878  pcoass  24940  ipcau2  25150  4cphipval2  25158  minveclem3  25345  sca2rab  25429  ovolscalem1  25430  uniioombllem4  25503  uniioombl  25506  itg1mulc  25621  itg2const2  25658  dvrec  25875  dveflem  25899  lhop1  25935  vieta1  26236  elqaalem3  26245  abelthlem8  26365  tangtx  26430  tanregt0  26464  eff1olem  26473  eflogeq  26527  argregt0  26535  argrege0  26536  argimgt0  26537  cxpeq  26683  ang180lem5  26739  lawcoslem1  26741  isosctrlem2  26745  isosctrlem3  26746  heron  26764  dcubic1lem  26769  dcubic2  26770  dcubic1  26771  mcubic  26773  dquartlem1  26777  dquart  26779  quart1lem  26781  quart1  26782  quart  26787  atantayl2  26864  birthdaylem2  26878  ftalem5  27003  basellem3  27009  basellem4  27010  fsumdvdsdiaglem  27109  logexprlim  27152  mersenne  27154  perfectlem2  27157  perfect  27158  bposlem9  27219  lgsqrlem2  27274  lgseisenlem1  27302  lgseisenlem3  27304  lgsquadlem1  27307  lgsquad2lem1  27311  m1lgs  27315  2sqlem8  27353  rplogsumlem1  27411  dchrvmasumiflem2  27429  dchrisum0flblem2  27436  dchrisum0fno1  27438  dchrisum0lem1  27443  mulog2sumlem3  27463  selberglem2  27473  selberg3lem1  27484  selberg4lem1  27487  selberg3r  27496  selberg4r  27497  pntrlog2bndlem2  27505  pntlemg  27525  axsegconlem10  28889  axeuclidlem  28925  quad3d  32706  constrinvcl  33739  cos9thpiminplylem3  33750  oddpwdc  34321  subfacval2  35159  circum  35646  faclimlem1  35715  nn0prpwlem  36295  knoppndvlem19  36503  areacirclem1  37687  areacirclem4  37690  cntotbnd  37775  lcmineqlem23  42024  aks6d1c1p3  42083  aks6d1c2p2  42092  aks6d1c3  42096  aks6d1c2lem4  42100  unitscyglem2  42169  unitscyglem4  42171  oddnumth  42284  sumcubes  42286  zdivgd  42310  dffltz  42607  irrapxlem5  42799  pellexlem2  42803  jm2.22  42968  jm2.20nn  42970  sqrtcval  43614  nzss  44290  binomcxplemnotnn0  44329  oddfl  45260  xralrple3  45354  sumnnodd  45612  limclner  45633  stoweidlem62  46044  stirlinglem1  46056  dirkertrigeqlem2  46081  dirkertrigeqlem3  46082  fourierdlem66  46154  fourierdlem73  46161  fourierdlem87  46175  qndenserrnbllem  46276  hoiqssbllem2  46605  2tceilhalfelfzo1  47317  fmtnoprmfac2lem1  47551  sfprmdvdsmersenne  47588  dfeven4  47623  oddflALTV  47648  nn0onn0exALTV  47684  perfectALTVlem2  47707  perfectALTV  47708  nn0onn0ex  48496  affinecomb2  48676  line2ylem  48724  line2xlem  48726  itscnhlc0yqe  48732  itsclquadb  48749