Theorem divcan2d 12042

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  (class class class)co 7430  ℂcc 11150  0cc0 11152   · cmul 11157   / cdiv 11917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918

This theorem is referenced by:  nneo  12699  zeo2  12702  intfracq  13895  discr  14275  hashf1  14492  caurcvgr  15706  iseralt  15717  mertenslem1  15916  fprodle  16028  bpoly4  16091  tanadd  16199  divconjdvds  16348  mod2eq1n2dvds  16380  bitsmod  16469  mulgcd  16581  qredeq  16690  qredeu  16691  prmind2  16718  isprm5  16740  pythagtriplem19  16866  pcprendvds2  16874  pcpremul  16876  pcadd  16922  prmreclem1  16949  4sqlem19  16996  ablfac1lem  20102  pgpfac1lem3  20111  prmirredlem  21500  znrrg  21601  metnrmlem3  24896  lebnumlem3  25008  pcoass  25070  ipcau2  25281  4cphipval2  25289  minveclem3  25476  sca2rab  25560  ovolscalem1  25561  uniioombllem4  25634  uniioombl  25637  itg1mulc  25753  itg2const2  25790  dvrec  26007  dveflem  26031  lhop1  26067  vieta1  26368  elqaalem3  26377  abelthlem8  26497  tangtx  26561  tanregt0  26595  eff1olem  26604  eflogeq  26658  argregt0  26666  argrege0  26667  argimgt0  26668  cxpeq  26814  ang180lem5  26870  lawcoslem1  26872  isosctrlem2  26876  isosctrlem3  26877  heron  26895  dcubic1lem  26900  dcubic2  26901  dcubic1  26902  mcubic  26904  dquartlem1  26908  dquart  26910  quart1lem  26912  quart1  26913  quart  26918  atantayl2  26995  birthdaylem2  27009  ftalem5  27134  basellem3  27140  basellem4  27141  fsumdvdsdiaglem  27240  logexprlim  27283  mersenne  27285  perfectlem2  27288  perfect  27289  bposlem9  27350  lgsqrlem2  27405  lgseisenlem1  27433  lgseisenlem3  27435  lgsquadlem1  27438  lgsquad2lem1  27442  m1lgs  27446  2sqlem8  27484  rplogsumlem1  27542  dchrvmasumiflem2  27560  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0lem1  27574  mulog2sumlem3  27594  selberglem2  27604  selberg3lem1  27615  selberg4lem1  27618  selberg3r  27627  selberg4r  27628  pntrlog2bndlem2  27636  pntlemg  27656  axsegconlem10  28955  axeuclidlem  28991  quad3d  32760  oddpwdc  34335  subfacval2  35171  circum  35658  faclimlem1  35722  nn0prpwlem  36304  knoppndvlem19  36512  areacirclem1  37694  areacirclem4  37697  cntotbnd  37782  lcmineqlem23  42032  aks6d1c1p3  42091  aks6d1c2p2  42100  aks6d1c3  42104  aks6d1c2lem4  42108  unitscyglem2  42177  unitscyglem4  42179  oddnumth  42323  sumcubes  42325  zdivgd  42350  dffltz  42620  irrapxlem5  42813  pellexlem2  42817  jm2.22  42983  jm2.20nn  42985  sqrtcval  43630  nzss  44312  binomcxplemnotnn0  44351  oddfl  45227  xralrple3  45323  sumnnodd  45585  limclner  45606  stoweidlem62  46017  stirlinglem1  46029  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  fourierdlem66  46127  fourierdlem73  46134  fourierdlem87  46148  qndenserrnbllem  46249  hoiqssbllem2  46578  fmtnoprmfac2lem1  47490  sfprmdvdsmersenne  47527  dfeven4  47562  oddflALTV  47587  nn0onn0exALTV  47623  perfectALTVlem2  47646  perfectALTV  47647  2tceilhalfelfzo1  47952  nn0onn0ex  48372  affinecomb2  48552  line2ylem  48600  line2xlem  48602  itscnhlc0yqe  48608  itsclquadb  48625