Theorem divcan2d 11909

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  (class class class)co 7355  ℂcc 11014  0cc0 11016   · cmul 11021   / cdiv 11784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11073  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-addrcl 11077  ax-mulcl 11078  ax-mulrcl 11079  ax-mulcom 11080  ax-addass 11081  ax-mulass 11082  ax-distr 11083  ax-i2m1 11084  ax-1ne0 11085  ax-1rid 11086  ax-rnegex 11087  ax-rrecex 11088  ax-cnre 11089  ax-pre-lttri 11090  ax-pre-lttrn 11091  ax-pre-ltadd 11092  ax-pre-mulgt0 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-xr 11160  df-ltxr 11161  df-le 11162  df-sub 11356  df-neg 11357  df-div 11785

This theorem is referenced by:  nneo  12567  zeo2  12570  intfracq  13773  discr  14157  hashf1  14374  caurcvgr  15591  iseralt  15602  mertenslem1  15801  fprodle  15913  bpoly4  15976  tanadd  16086  divconjdvds  16236  mod2eq1n2dvds  16268  bitsmod  16357  mulgcd  16469  qredeq  16578  qredeu  16579  prmind2  16606  isprm5  16628  pythagtriplem19  16755  pcprendvds2  16763  pcpremul  16765  pcadd  16811  prmreclem1  16838  4sqlem19  16885  ablfac1lem  19992  pgpfac1lem3  20001  prmirredlem  21419  znrrg  21512  metnrmlem3  24787  lebnumlem3  24899  pcoass  24961  ipcau2  25171  4cphipval2  25179  minveclem3  25366  sca2rab  25450  ovolscalem1  25451  uniioombllem4  25524  uniioombl  25527  itg1mulc  25642  itg2const2  25679  dvrec  25896  dveflem  25920  lhop1  25956  vieta1  26257  elqaalem3  26266  abelthlem8  26386  tangtx  26451  tanregt0  26485  eff1olem  26494  eflogeq  26548  argregt0  26556  argrege0  26557  argimgt0  26558  cxpeq  26704  ang180lem5  26760  lawcoslem1  26762  isosctrlem2  26766  isosctrlem3  26767  heron  26785  dcubic1lem  26790  dcubic2  26791  dcubic1  26792  mcubic  26794  dquartlem1  26798  dquart  26800  quart1lem  26802  quart1  26803  quart  26808  atantayl2  26885  birthdaylem2  26899  ftalem5  27024  basellem3  27030  basellem4  27031  fsumdvdsdiaglem  27130  logexprlim  27173  mersenne  27175  perfectlem2  27178  perfect  27179  bposlem9  27240  lgsqrlem2  27295  lgseisenlem1  27323  lgseisenlem3  27325  lgsquadlem1  27328  lgsquad2lem1  27332  m1lgs  27336  2sqlem8  27374  rplogsumlem1  27432  dchrvmasumiflem2  27450  dchrisum0flblem2  27457  dchrisum0fno1  27459  dchrisum0lem1  27464  mulog2sumlem3  27484  selberglem2  27494  selberg3lem1  27505  selberg4lem1  27508  selberg3r  27517  selberg4r  27518  pntrlog2bndlem2  27526  pntlemg  27546  axsegconlem10  28915  axeuclidlem  28951  quad3d  32744  constrinvcl  33797  cos9thpiminplylem3  33808  oddpwdc  34378  subfacval2  35242  circum  35729  faclimlem1  35798  nn0prpwlem  36377  knoppndvlem19  36585  areacirclem1  37758  areacirclem4  37761  cntotbnd  37846  lcmineqlem23  42154  aks6d1c1p3  42213  aks6d1c2p2  42222  aks6d1c3  42226  aks6d1c2lem4  42230  unitscyglem2  42299  unitscyglem4  42301  oddnumth  42419  sumcubes  42421  zdivgd  42445  dffltz  42742  irrapxlem5  42933  pellexlem2  42937  jm2.22  43102  jm2.20nn  43104  sqrtcval  43748  nzss  44424  binomcxplemnotnn0  44463  oddfl  45393  xralrple3  45486  sumnnodd  45744  limclner  45763  stoweidlem62  46174  stirlinglem1  46186  dirkertrigeqlem2  46211  dirkertrigeqlem3  46212  fourierdlem66  46284  fourierdlem73  46291  fourierdlem87  46305  qndenserrnbllem  46406  hoiqssbllem2  46735  2tceilhalfelfzo1  47446  fmtnoprmfac2lem1  47680  sfprmdvdsmersenne  47717  dfeven4  47752  oddflALTV  47777  nn0onn0exALTV  47813  perfectALTVlem2  47836  perfectALTV  47837  nn0onn0ex  48638  affinecomb2  48818  line2ylem  48866  line2xlem  48868  itscnhlc0yqe  48874  itsclquadb  48891