Theorem divcan2d 12024

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  (class class class)co 7410  ℂcc 11132  0cc0 11134   · cmul 11139   / cdiv 11899

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900

This theorem is referenced by:  nneo  12682  zeo2  12685  intfracq  13881  discr  14263  hashf1  14480  caurcvgr  15695  iseralt  15706  mertenslem1  15905  fprodle  16017  bpoly4  16080  tanadd  16190  divconjdvds  16339  mod2eq1n2dvds  16371  bitsmod  16460  mulgcd  16572  qredeq  16681  qredeu  16682  prmind2  16709  isprm5  16731  pythagtriplem19  16858  pcprendvds2  16866  pcpremul  16868  pcadd  16914  prmreclem1  16941  4sqlem19  16988  ablfac1lem  20056  pgpfac1lem3  20065  prmirredlem  21438  znrrg  21531  metnrmlem3  24806  lebnumlem3  24918  pcoass  24980  ipcau2  25191  4cphipval2  25199  minveclem3  25386  sca2rab  25470  ovolscalem1  25471  uniioombllem4  25544  uniioombl  25547  itg1mulc  25662  itg2const2  25699  dvrec  25916  dveflem  25940  lhop1  25976  vieta1  26277  elqaalem3  26286  abelthlem8  26406  tangtx  26471  tanregt0  26505  eff1olem  26514  eflogeq  26568  argregt0  26576  argrege0  26577  argimgt0  26578  cxpeq  26724  ang180lem5  26780  lawcoslem1  26782  isosctrlem2  26786  isosctrlem3  26787  heron  26805  dcubic1lem  26810  dcubic2  26811  dcubic1  26812  mcubic  26814  dquartlem1  26818  dquart  26820  quart1lem  26822  quart1  26823  quart  26828  atantayl2  26905  birthdaylem2  26919  ftalem5  27044  basellem3  27050  basellem4  27051  fsumdvdsdiaglem  27150  logexprlim  27193  mersenne  27195  perfectlem2  27198  perfect  27199  bposlem9  27260  lgsqrlem2  27315  lgseisenlem1  27343  lgseisenlem3  27345  lgsquadlem1  27348  lgsquad2lem1  27352  m1lgs  27356  2sqlem8  27394  rplogsumlem1  27452  dchrvmasumiflem2  27470  dchrisum0flblem2  27477  dchrisum0fno1  27479  dchrisum0lem1  27484  mulog2sumlem3  27504  selberglem2  27514  selberg3lem1  27525  selberg4lem1  27528  selberg3r  27537  selberg4r  27538  pntrlog2bndlem2  27546  pntlemg  27566  axsegconlem10  28910  axeuclidlem  28946  quad3d  32732  constrinvcl  33812  cos9thpiminplylem3  33823  oddpwdc  34391  subfacval2  35214  circum  35701  faclimlem1  35765  nn0prpwlem  36345  knoppndvlem19  36553  areacirclem1  37737  areacirclem4  37740  cntotbnd  37825  lcmineqlem23  42069  aks6d1c1p3  42128  aks6d1c2p2  42137  aks6d1c3  42141  aks6d1c2lem4  42145  unitscyglem2  42214  unitscyglem4  42216  oddnumth  42329  sumcubes  42331  zdivgd  42355  dffltz  42632  irrapxlem5  42824  pellexlem2  42828  jm2.22  42994  jm2.20nn  42996  sqrtcval  43640  nzss  44316  binomcxplemnotnn0  44355  oddfl  45286  xralrple3  45381  sumnnodd  45639  limclner  45660  stoweidlem62  46071  stirlinglem1  46083  dirkertrigeqlem2  46108  dirkertrigeqlem3  46109  fourierdlem66  46181  fourierdlem73  46188  fourierdlem87  46202  qndenserrnbllem  46303  hoiqssbllem2  46632  2tceilhalfelfzo1  47341  fmtnoprmfac2lem1  47560  sfprmdvdsmersenne  47597  dfeven4  47632  oddflALTV  47657  nn0onn0exALTV  47693  perfectALTVlem2  47716  perfectALTV  47717  nn0onn0ex  48483  affinecomb2  48663  line2ylem  48711  line2xlem  48713  itscnhlc0yqe  48719  itsclquadb  48736