Theorem divcan2d 11923

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7360  ℂcc 11028  0cc0 11030   · cmul 11035   / cdiv 11798

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

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 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799

This theorem is referenced by:  nneo  12580  zeo2  12583  intfracq  13783  discr  14167  hashf1  14384  caurcvgr  15601  iseralt  15612  mertenslem1  15811  fprodle  15923  bpoly4  15986  tanadd  16096  divconjdvds  16246  mod2eq1n2dvds  16278  bitsmod  16367  mulgcd  16479  qredeq  16588  qredeu  16589  prmind2  16616  isprm5  16638  pythagtriplem19  16765  pcprendvds2  16773  pcpremul  16775  pcadd  16821  prmreclem1  16848  4sqlem19  16895  ablfac1lem  20003  pgpfac1lem3  20012  prmirredlem  21431  znrrg  21524  metnrmlem3  24810  lebnumlem3  24922  pcoass  24984  ipcau2  25194  4cphipval2  25202  minveclem3  25389  sca2rab  25473  ovolscalem1  25474  uniioombllem4  25547  uniioombl  25550  itg1mulc  25665  itg2const2  25702  dvrec  25919  dveflem  25943  lhop1  25979  vieta1  26280  elqaalem3  26289  abelthlem8  26409  tangtx  26474  tanregt0  26508  eff1olem  26517  eflogeq  26571  argregt0  26579  argrege0  26580  argimgt0  26581  cxpeq  26727  ang180lem5  26783  lawcoslem1  26785  isosctrlem2  26789  isosctrlem3  26790  heron  26808  dcubic1lem  26813  dcubic2  26814  dcubic1  26815  mcubic  26817  dquartlem1  26821  dquart  26823  quart1lem  26825  quart1  26826  quart  26831  atantayl2  26908  birthdaylem2  26922  ftalem5  27047  basellem3  27053  basellem4  27054  fsumdvdsdiaglem  27153  logexprlim  27196  mersenne  27198  perfectlem2  27201  perfect  27202  bposlem9  27263  lgsqrlem2  27318  lgseisenlem1  27346  lgseisenlem3  27348  lgsquadlem1  27351  lgsquad2lem1  27355  m1lgs  27359  2sqlem8  27397  rplogsumlem1  27455  dchrvmasumiflem2  27473  dchrisum0flblem2  27480  dchrisum0fno1  27482  dchrisum0lem1  27487  mulog2sumlem3  27507  selberglem2  27517  selberg3lem1  27528  selberg4lem1  27531  selberg3r  27540  selberg4r  27541  pntrlog2bndlem2  27549  pntlemg  27569  axsegconlem10  28982  axeuclidlem  29018  quad3d  32810  constrinvcl  33911  cos9thpiminplylem3  33922  oddpwdc  34492  subfacval2  35362  circum  35849  faclimlem1  35918  nn0prpwlem  36497  knoppndvlem19  36705  areacirclem1  37880  areacirclem4  37883  cntotbnd  37968  lcmineqlem23  42342  aks6d1c1p3  42401  aks6d1c2p2  42410  aks6d1c3  42414  aks6d1c2lem4  42418  unitscyglem2  42487  unitscyglem4  42489  oddnumth  42602  sumcubes  42604  zdivgd  42628  dffltz  42913  irrapxlem5  43104  pellexlem2  43108  jm2.22  43273  jm2.20nn  43275  sqrtcval  43918  nzss  44594  binomcxplemnotnn0  44633  oddfl  45562  xralrple3  45654  sumnnodd  45912  limclner  45931  stoweidlem62  46342  stirlinglem1  46354  dirkertrigeqlem2  46379  dirkertrigeqlem3  46380  fourierdlem66  46452  fourierdlem73  46459  fourierdlem87  46473  qndenserrnbllem  46574  hoiqssbllem2  46903  2tceilhalfelfzo1  47614  fmtnoprmfac2lem1  47848  sfprmdvdsmersenne  47885  dfeven4  47920  oddflALTV  47945  nn0onn0exALTV  47981  perfectALTVlem2  48004  perfectALTV  48005  nn0onn0ex  48805  affinecomb2  48985  line2ylem  49033  line2xlem  49035  itscnhlc0yqe  49041  itsclquadb  49058