Theorem divcan2d 10682

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  (class class class)co 6549  ℂcc 9813  0cc0 9815   · cmul 9820   / cdiv 10563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564

This theorem is referenced by:  nneo  11337  zeo2  11340  intfracq  12520  discr  12863  hashf1  13098  caurcvgr  14252  iseralt  14263  mertenslem1  14455  fprodle  14566  bpoly4  14629  tanadd  14736  divconjdvds  14875  mod2eq1n2dvds  14909  bitsmod  14996  mulgcd  15103  qredeq  15209  qredeu  15210  prmind2  15236  isprm5  15257  pythagtriplem19  15376  pcprendvds2  15384  pcpremul  15386  pcadd  15431  prmreclem1  15458  4sqlem19  15505  ablfac1lem  18290  pgpfac1lem3  18299  prmirredlem  19660  znrrg  19733  metnrmlem3  22472  lebnumlem3  22570  pcoass  22632  ipcau2  22841  4cphipval2  22849  minveclem3  23008  sca2rab  23087  ovolscalem1  23088  uniioombllem4  23160  uniioombl  23163  itg1mulc  23277  itg2const2  23314  dvrec  23524  dveflem  23546  lhop1  23581  vieta1  23871  elqaalem3  23880  abelthlem8  23997  tangtx  24061  tanregt0  24089  eff1olem  24098  eflogeq  24152  argregt0  24160  argrege0  24161  argimgt0  24162  cxpeq  24298  ang180lem5  24343  lawcoslem1  24345  isosctrlem2  24349  isosctrlem3  24350  heron  24365  dcubic1lem  24370  dcubic2  24371  dcubic1  24372  mcubic  24374  dquartlem1  24378  dquart  24380  quart1lem  24382  quart1  24383  quart  24388  atantayl2  24465  birthdaylem2  24479  ftalem5  24603  basellem3  24609  basellem4  24610  fsumdvdsdiaglem  24709  logexprlim  24750  mersenne  24752  perfectlem2  24755  perfect  24756  bposlem9  24817  lgsqrlem2  24872  lgseisenlem1  24900  lgseisenlem3  24902  lgsquadlem1  24905  lgsquad2lem1  24909  m1lgs  24913  2sqlem8  24951  rplogsumlem1  24973  dchrvmasumiflem2  24991  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0lem1  25005  mulog2sumlem3  25025  selberglem2  25035  selberg3lem1  25046  selberg4lem1  25049  selberg3r  25058  selberg4r  25059  pntrlog2bndlem2  25067  pntlemg  25087  axsegconlem10  25606  axeuclidlem  25642  oddpwdc  29743  subfacval2  30423  circum  30822  faclimlem1  30882  nn0prpwlem  31487  knoppndvlem19  31691  areacirclem1  32670  areacirclem4  32673  cntotbnd  32765  irrapxlem5  36408  pellexlem2  36412  jm2.22  36580  jm2.20nn  36582  nzss  37538  binomcxplemnotnn0  37577  oddfl  38430  xralrple3  38531  sumnnodd  38697  limclner  38718  stoweidlem62  38955  stirlinglem1  38967  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  fourierdlem66  39065  fourierdlem73  39072  fourierdlem87  39086  qndenserrnbllem  39190  hoiqssbllem2  39513  fmtnoprmfac2lem1  40016  sfprmdvdsmersenne  40058  dfeven4  40089  oddflALTV  40113  nn0onn0exALTV  40147  perfectALTVlem2  40165  perfectALTV  40166  nn0onn0ex  42112