Theorem divcan2d 11955

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132   ≠ wne 2947  (class class class)co 7381  ℂcc 11057  0cc0 11059   · cmul 11064   / cdiv 11830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rmo 3357  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-riota 7338  df-ov 7384  df-oprab 7385  df-mpo 7386  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208  df-sub 11402  df-neg 11403  df-div 11831

This theorem is referenced by:  nneo  12643  zeo2  12646  intfracq  13855  discr  14239  hashf1  14456  caurcvgr  15673  iseralt  15684  mertenslem1  15886  fprodle  15998  bpoly4  16061  tanadd  16171  divconjdvds  16321  mod2eq1n2dvds  16353  bitsmod  16442  mulgcd  16554  qredeq  16663  qredeu  16664  prmind2  16691  isprm5  16714  pythagtriplem19  16841  pcprendvds2  16849  pcpremul  16851  pcadd  16897  prmreclem1  16924  4sqlem19  16971  ablfac1lem  20082  pgpfac1lem3  20091  prmirredlem  21493  znrrg  21586  metnrmlem3  24891  lebnumlem3  24994  pcoass  25055  ipcau2  25265  4cphipval2  25273  minveclem3  25460  sca2rab  25543  ovolscalem1  25544  uniioombllem4  25617  uniioombl  25620  itg1mulc  25735  itg2const2  25772  dvrec  25986  dveflem  26010  lhop1  26045  vieta1  26342  elqaalem3  26351  abelthlem8  26468  tangtx  26536  tanregt0  26570  eff1olem  26579  eflogeq  26633  argregt0  26641  argrege0  26642  argimgt0  26643  cxpeq  26788  ang180lem5  26844  lawcoslem1  26846  isosctrlem2  26850  isosctrlem3  26851  heron  26869  dcubic1lem  26874  dcubic2  26875  dcubic1  26876  mcubic  26878  dquartlem1  26882  dquart  26884  quart1lem  26886  quart1  26887  quart  26892  atantayl2  26969  birthdaylem2  26983  ftalem5  27107  basellem3  27113  basellem4  27114  fsumdvdsdiaglem  27213  logexprlim  27255  mersenne  27257  perfectlem2  27260  perfect  27261  bposlem9  27322  lgsqrlem2  27377  lgseisenlem1  27405  lgseisenlem3  27407  lgsquadlem1  27410  lgsquad2lem1  27414  m1lgs  27418  2sqlem8  27456  rplogsumlem1  27514  dchrvmasumiflem2  27532  dchrisum0flblem2  27539  dchrisum0fno1  27541  dchrisum0lem1  27546  mulog2sumlem3  27566  selberglem2  27576  selberg3lem1  27587  selberg4lem1  27590  selberg3r  27599  selberg4r  27600  pntrlog2bndlem2  27608  pntlemg  27628  axsegconlem10  29062  axeuclidlem  29098  quad3d  32890  constrinvcl  34014  cos9thpiminplylem3  34025  oddpwdc  34595  subfacval2  35475  circum  35962  faclimlem1  36031  nn0prpwlem  36620  knoppndvlem19  36906  areacirclem1  38145  areacirclem4  38148  cntotbnd  38233  lcmineqlem23  42606  aks6d1c1p3  42665  aks6d1c2p2  42674  aks6d1c3  42678  aks6d1c2lem4  42682  unitscyglem2  42751  unitscyglem4  42753  oddnumth  42858  sumcubes  42860  zdivgd  42884  dffltz  43154  irrapxlem5  43341  pellexlem2  43345  jm2.22  43510  jm2.20nn  43512  sqrtcval  44155  nzss  44831  binomcxplemnotnn0  44870  oddfl  45795  xralrple3  45887  sumnnodd  46144  limclner  46163  stoweidlem62  46574  stirlinglem1  46586  dirkertrigeqlem2  46611  dirkertrigeqlem3  46612  fourierdlem66  46684  fourierdlem73  46691  fourierdlem87  46705  qndenserrnbllem  46806  hoiqssbllem2  47135  2tceilhalfelfzo1  47868  fmtnoprmfac2lem1  48113  sfprmdvdsmersenne  48150  dfeven4  48198  oddflALTV  48223  nn0onn0exALTV  48259  perfectALTVlem2  48282  perfectALTV  48283  nn0onn0ex  49083  affinecomb2  49263  line2ylem  49311  line2xlem  49313  itscnhlc0yqe  49319  itsclquadb  49336