Theorem divcan2d 11922

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2930  (class class class)co 7356  ℂcc 11025  0cc0 11027   · cmul 11032   / cdiv 11796

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rmo 3340  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797

This theorem is referenced by:  nneo  12602  zeo2  12605  intfracq  13807  discr  14191  hashf1  14408  caurcvgr  15625  iseralt  15636  mertenslem1  15838  fprodle  15950  bpoly4  16013  tanadd  16123  divconjdvds  16273  mod2eq1n2dvds  16305  bitsmod  16394  mulgcd  16506  qredeq  16615  qredeu  16616  prmind2  16643  isprm5  16666  pythagtriplem19  16793  pcprendvds2  16801  pcpremul  16803  pcadd  16849  prmreclem1  16876  4sqlem19  16923  ablfac1lem  20034  pgpfac1lem3  20043  prmirredlem  21441  znrrg  21534  metnrmlem3  24815  lebnumlem3  24918  pcoass  24979  ipcau2  25189  4cphipval2  25197  minveclem3  25384  sca2rab  25467  ovolscalem1  25468  uniioombllem4  25541  uniioombl  25544  itg1mulc  25659  itg2const2  25696  dvrec  25910  dveflem  25934  lhop1  25969  vieta1  26266  elqaalem3  26275  abelthlem8  26392  tangtx  26457  tanregt0  26491  eff1olem  26500  eflogeq  26554  argregt0  26562  argrege0  26563  argimgt0  26564  cxpeq  26709  ang180lem5  26765  lawcoslem1  26767  isosctrlem2  26771  isosctrlem3  26772  heron  26790  dcubic1lem  26795  dcubic2  26796  dcubic1  26797  mcubic  26799  dquartlem1  26803  dquart  26805  quart1lem  26807  quart1  26808  quart  26813  atantayl2  26890  birthdaylem2  26904  ftalem5  27028  basellem3  27034  basellem4  27035  fsumdvdsdiaglem  27134  logexprlim  27176  mersenne  27178  perfectlem2  27181  perfect  27182  bposlem9  27243  lgsqrlem2  27298  lgseisenlem1  27326  lgseisenlem3  27328  lgsquadlem1  27331  lgsquad2lem1  27335  m1lgs  27339  2sqlem8  27377  rplogsumlem1  27435  dchrvmasumiflem2  27453  dchrisum0flblem2  27460  dchrisum0fno1  27462  dchrisum0lem1  27467  mulog2sumlem3  27487  selberglem2  27497  selberg3lem1  27508  selberg4lem1  27511  selberg3r  27520  selberg4r  27521  pntrlog2bndlem2  27529  pntlemg  27549  axsegconlem10  28983  axeuclidlem  29019  quad3d  32810  constrinvcl  33905  cos9thpiminplylem3  33916  oddpwdc  34486  subfacval2  35357  circum  35844  faclimlem1  35913  nn0prpwlem  36492  knoppndvlem19  36778  areacirclem1  38017  areacirclem4  38020  cntotbnd  38105  lcmineqlem23  42478  aks6d1c1p3  42537  aks6d1c2p2  42546  aks6d1c3  42550  aks6d1c2lem4  42554  unitscyglem2  42623  unitscyglem4  42625  oddnumth  42731  sumcubes  42733  zdivgd  42757  dffltz  43055  irrapxlem5  43242  pellexlem2  43246  jm2.22  43411  jm2.20nn  43413  sqrtcval  44056  nzss  44732  binomcxplemnotnn0  44771  oddfl  45699  xralrple3  45791  sumnnodd  46048  limclner  46067  stoweidlem62  46478  stirlinglem1  46490  dirkertrigeqlem2  46515  dirkertrigeqlem3  46516  fourierdlem66  46588  fourierdlem73  46595  fourierdlem87  46609  qndenserrnbllem  46710  hoiqssbllem2  47039  2tceilhalfelfzo1  47772  fmtnoprmfac2lem1  48017  sfprmdvdsmersenne  48054  dfeven4  48102  oddflALTV  48127  nn0onn0exALTV  48163  perfectALTVlem2  48186  perfectALTV  48187  nn0onn0ex  48987  affinecomb2  49167  line2ylem  49215  line2xlem  49217  itscnhlc0yqe  49223  itsclquadb  49240