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

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

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  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 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 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-sub 11367  df-neg 11368  df-div 11796

This theorem is referenced by:  nneo  12577  zeo2  12580  intfracq  13780  discr  14164  hashf1  14381  caurcvgr  15598  iseralt  15609  mertenslem1  15808  fprodle  15920  bpoly4  15983  tanadd  16093  divconjdvds  16243  mod2eq1n2dvds  16275  bitsmod  16364  mulgcd  16476  qredeq  16585  qredeu  16586  prmind2  16613  isprm5  16635  pythagtriplem19  16762  pcprendvds2  16770  pcpremul  16772  pcadd  16818  prmreclem1  16845  4sqlem19  16892  ablfac1lem  20003  pgpfac1lem3  20012  prmirredlem  21429  znrrg  21522  metnrmlem3  24805  lebnumlem3  24908  pcoass  24969  ipcau2  25179  4cphipval2  25187  minveclem3  25374  sca2rab  25457  ovolscalem1  25458  uniioombllem4  25531  uniioombl  25534  itg1mulc  25649  itg2const2  25686  dvrec  25900  dveflem  25924  lhop1  25960  vieta1  26260  elqaalem3  26269  abelthlem8  26389  tangtx  26454  tanregt0  26488  eff1olem  26497  eflogeq  26551  argregt0  26559  argrege0  26560  argimgt0  26561  cxpeq  26707  ang180lem5  26763  lawcoslem1  26765  isosctrlem2  26769  isosctrlem3  26770  heron  26788  dcubic1lem  26793  dcubic2  26794  dcubic1  26795  mcubic  26797  dquartlem1  26801  dquart  26803  quart1lem  26805  quart1  26806  quart  26811  atantayl2  26888  birthdaylem2  26902  ftalem5  27027  basellem3  27033  basellem4  27034  fsumdvdsdiaglem  27133  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  32812  constrinvcl  33923  cos9thpiminplylem3  33934  oddpwdc  34504  subfacval2  35375  circum  35862  faclimlem1  35931  nn0prpwlem  36510  knoppndvlem19  36788  areacirclem1  38020  areacirclem4  38023  cntotbnd  38108  lcmineqlem23  42482  aks6d1c1p3  42541  aks6d1c2p2  42550  aks6d1c3  42554  aks6d1c2lem4  42558  unitscyglem2  42627  unitscyglem4  42629  oddnumth  42742  sumcubes  42744  zdivgd  42768  dffltz  43066  irrapxlem5  43257  pellexlem2  43261  jm2.22  43426  jm2.20nn  43428  sqrtcval  44071  nzss  44747  binomcxplemnotnn0  44786  oddfl  45714  xralrple3  45806  sumnnodd  46064  limclner  46083  stoweidlem62  46494  stirlinglem1  46506  dirkertrigeqlem2  46531  dirkertrigeqlem3  46532  fourierdlem66  46604  fourierdlem73  46611  fourierdlem87  46625  qndenserrnbllem  46726  hoiqssbllem2  47055  2tceilhalfelfzo1  47766  fmtnoprmfac2lem1  48000  sfprmdvdsmersenne  48037  dfeven4  48072  oddflALTV  48097  nn0onn0exALTV  48133  perfectALTVlem2  48156  perfectALTV  48157  nn0onn0ex  48957  affinecomb2  49137  line2ylem  49185  line2xlem  49187  itscnhlc0yqe  49193  itsclquadb  49210