Theorem divcan2d 11753

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  (class class class)co 7275  ℂcc 10869  0cc0 10871   · cmul 10876   / cdiv 11632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633

This theorem is referenced by:  nneo  12404  zeo2  12407  intfracq  13579  discr  13955  hashf1  14171  caurcvgr  15385  iseralt  15396  mertenslem1  15596  fprodle  15706  bpoly4  15769  tanadd  15876  divconjdvds  16024  mod2eq1n2dvds  16056  bitsmod  16143  mulgcd  16256  qredeq  16362  qredeu  16363  prmind2  16390  isprm5  16412  pythagtriplem19  16534  pcprendvds2  16542  pcpremul  16544  pcadd  16590  prmreclem1  16617  4sqlem19  16664  ablfac1lem  19671  pgpfac1lem3  19680  prmirredlem  20694  znrrg  20773  metnrmlem3  24024  lebnumlem3  24126  pcoass  24187  ipcau2  24398  4cphipval2  24406  minveclem3  24593  sca2rab  24676  ovolscalem1  24677  uniioombllem4  24750  uniioombl  24753  itg1mulc  24869  itg2const2  24906  dvrec  25119  dveflem  25143  lhop1  25178  vieta1  25472  elqaalem3  25481  abelthlem8  25598  tangtx  25662  tanregt0  25695  eff1olem  25704  eflogeq  25757  argregt0  25765  argrege0  25766  argimgt0  25767  cxpeq  25910  ang180lem5  25963  lawcoslem1  25965  isosctrlem2  25969  isosctrlem3  25970  heron  25988  dcubic1lem  25993  dcubic2  25994  dcubic1  25995  mcubic  25997  dquartlem1  26001  dquart  26003  quart1lem  26005  quart1  26006  quart  26011  atantayl2  26088  birthdaylem2  26102  ftalem5  26226  basellem3  26232  basellem4  26233  fsumdvdsdiaglem  26332  logexprlim  26373  mersenne  26375  perfectlem2  26378  perfect  26379  bposlem9  26440  lgsqrlem2  26495  lgseisenlem1  26523  lgseisenlem3  26525  lgsquadlem1  26528  lgsquad2lem1  26532  m1lgs  26536  2sqlem8  26574  rplogsumlem1  26632  dchrvmasumiflem2  26650  dchrisum0flblem2  26657  dchrisum0fno1  26659  dchrisum0lem1  26664  mulog2sumlem3  26684  selberglem2  26694  selberg3lem1  26705  selberg4lem1  26708  selberg3r  26717  selberg4r  26718  pntrlog2bndlem2  26726  pntlemg  26746  axsegconlem10  27294  axeuclidlem  27330  oddpwdc  32321  subfacval2  33149  circum  33632  faclimlem1  33709  nn0prpwlem  34511  knoppndvlem19  34710  areacirclem1  35865  areacirclem4  35868  cntotbnd  35954  lcmineqlem23  40059  dffltz  40471  irrapxlem5  40648  pellexlem2  40652  jm2.22  40817  jm2.20nn  40819  sqrtcval  41249  nzss  41935  binomcxplemnotnn0  41974  oddfl  42816  xralrple3  42913  sumnnodd  43171  limclner  43192  stoweidlem62  43603  stirlinglem1  43615  dirkertrigeqlem2  43640  dirkertrigeqlem3  43641  fourierdlem66  43713  fourierdlem73  43720  fourierdlem87  43734  qndenserrnbllem  43835  hoiqssbllem2  44161  fmtnoprmfac2lem1  45018  sfprmdvdsmersenne  45055  dfeven4  45090  oddflALTV  45115  nn0onn0exALTV  45151  perfectALTVlem2  45174  perfectALTV  45175  nn0onn0ex  45869  affinecomb2  46049  line2ylem  46097  line2xlem  46099  itscnhlc0yqe  46105  itsclquadb  46122