Theorem divcan2d 11966

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  (class class class)co 7389  ℂcc 11072  0cc0 11074   · cmul 11079   / cdiv 11841

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 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-div 11842

This theorem is referenced by:  nneo  12624  zeo2  12627  intfracq  13827  discr  14211  hashf1  14428  caurcvgr  15646  iseralt  15657  mertenslem1  15856  fprodle  15968  bpoly4  16031  tanadd  16141  divconjdvds  16291  mod2eq1n2dvds  16323  bitsmod  16412  mulgcd  16524  qredeq  16633  qredeu  16634  prmind2  16661  isprm5  16683  pythagtriplem19  16810  pcprendvds2  16818  pcpremul  16820  pcadd  16866  prmreclem1  16893  4sqlem19  16940  ablfac1lem  20006  pgpfac1lem3  20015  prmirredlem  21388  znrrg  21481  metnrmlem3  24756  lebnumlem3  24868  pcoass  24930  ipcau2  25140  4cphipval2  25148  minveclem3  25335  sca2rab  25419  ovolscalem1  25420  uniioombllem4  25493  uniioombl  25496  itg1mulc  25611  itg2const2  25648  dvrec  25865  dveflem  25889  lhop1  25925  vieta1  26226  elqaalem3  26235  abelthlem8  26355  tangtx  26420  tanregt0  26454  eff1olem  26463  eflogeq  26517  argregt0  26525  argrege0  26526  argimgt0  26527  cxpeq  26673  ang180lem5  26729  lawcoslem1  26731  isosctrlem2  26735  isosctrlem3  26736  heron  26754  dcubic1lem  26759  dcubic2  26760  dcubic1  26761  mcubic  26763  dquartlem1  26767  dquart  26769  quart1lem  26771  quart1  26772  quart  26777  atantayl2  26854  birthdaylem2  26868  ftalem5  26993  basellem3  26999  basellem4  27000  fsumdvdsdiaglem  27099  logexprlim  27142  mersenne  27144  perfectlem2  27147  perfect  27148  bposlem9  27209  lgsqrlem2  27264  lgseisenlem1  27292  lgseisenlem3  27294  lgsquadlem1  27297  lgsquad2lem1  27301  m1lgs  27305  2sqlem8  27343  rplogsumlem1  27401  dchrvmasumiflem2  27419  dchrisum0flblem2  27426  dchrisum0fno1  27428  dchrisum0lem1  27433  mulog2sumlem3  27453  selberglem2  27463  selberg3lem1  27474  selberg4lem1  27477  selberg3r  27486  selberg4r  27487  pntrlog2bndlem2  27495  pntlemg  27515  axsegconlem10  28859  axeuclidlem  28895  quad3d  32679  constrinvcl  33769  cos9thpiminplylem3  33780  oddpwdc  34351  subfacval2  35174  circum  35661  faclimlem1  35725  nn0prpwlem  36305  knoppndvlem19  36513  areacirclem1  37697  areacirclem4  37700  cntotbnd  37785  lcmineqlem23  42034  aks6d1c1p3  42093  aks6d1c2p2  42102  aks6d1c3  42106  aks6d1c2lem4  42110  unitscyglem2  42179  unitscyglem4  42181  oddnumth  42294  sumcubes  42296  zdivgd  42320  dffltz  42615  irrapxlem5  42807  pellexlem2  42811  jm2.22  42977  jm2.20nn  42979  sqrtcval  43623  nzss  44299  binomcxplemnotnn0  44338  oddfl  45269  xralrple3  45363  sumnnodd  45621  limclner  45642  stoweidlem62  46053  stirlinglem1  46065  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  fourierdlem66  46163  fourierdlem73  46170  fourierdlem87  46184  qndenserrnbllem  46285  hoiqssbllem2  46614  2tceilhalfelfzo1  47323  fmtnoprmfac2lem1  47557  sfprmdvdsmersenne  47594  dfeven4  47629  oddflALTV  47654  nn0onn0exALTV  47690  perfectALTVlem2  47713  perfectALTV  47714  nn0onn0ex  48502  affinecomb2  48682  line2ylem  48730  line2xlem  48732  itscnhlc0yqe  48738  itsclquadb  48755