Theorem divcan2d 11891

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110   ≠ wne 2926  (class class class)co 7341  ℂcc 10996  0cc0 10998   · cmul 11003   / cdiv 11766

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074  ax-pre-mulgt0 11075

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-xr 11142  df-ltxr 11143  df-le 11144  df-sub 11338  df-neg 11339  df-div 11767

This theorem is referenced by:  nneo  12549  zeo2  12552  intfracq  13755  discr  14139  hashf1  14356  caurcvgr  15573  iseralt  15584  mertenslem1  15783  fprodle  15895  bpoly4  15958  tanadd  16068  divconjdvds  16218  mod2eq1n2dvds  16250  bitsmod  16339  mulgcd  16451  qredeq  16560  qredeu  16561  prmind2  16588  isprm5  16610  pythagtriplem19  16737  pcprendvds2  16745  pcpremul  16747  pcadd  16793  prmreclem1  16820  4sqlem19  16867  ablfac1lem  19975  pgpfac1lem3  19984  prmirredlem  21402  znrrg  21495  metnrmlem3  24770  lebnumlem3  24882  pcoass  24944  ipcau2  25154  4cphipval2  25162  minveclem3  25349  sca2rab  25433  ovolscalem1  25434  uniioombllem4  25507  uniioombl  25510  itg1mulc  25625  itg2const2  25662  dvrec  25879  dveflem  25903  lhop1  25939  vieta1  26240  elqaalem3  26249  abelthlem8  26369  tangtx  26434  tanregt0  26468  eff1olem  26477  eflogeq  26531  argregt0  26539  argrege0  26540  argimgt0  26541  cxpeq  26687  ang180lem5  26743  lawcoslem1  26745  isosctrlem2  26749  isosctrlem3  26750  heron  26768  dcubic1lem  26773  dcubic2  26774  dcubic1  26775  mcubic  26777  dquartlem1  26781  dquart  26783  quart1lem  26785  quart1  26786  quart  26791  atantayl2  26868  birthdaylem2  26882  ftalem5  27007  basellem3  27013  basellem4  27014  fsumdvdsdiaglem  27113  logexprlim  27156  mersenne  27158  perfectlem2  27161  perfect  27162  bposlem9  27223  lgsqrlem2  27278  lgseisenlem1  27306  lgseisenlem3  27308  lgsquadlem1  27311  lgsquad2lem1  27315  m1lgs  27319  2sqlem8  27357  rplogsumlem1  27415  dchrvmasumiflem2  27433  dchrisum0flblem2  27440  dchrisum0fno1  27442  dchrisum0lem1  27447  mulog2sumlem3  27467  selberglem2  27477  selberg3lem1  27488  selberg4lem1  27491  selberg3r  27500  selberg4r  27501  pntrlog2bndlem2  27509  pntlemg  27529  axsegconlem10  28897  axeuclidlem  28933  quad3d  32723  constrinvcl  33776  cos9thpiminplylem3  33787  oddpwdc  34357  subfacval2  35199  circum  35686  faclimlem1  35755  nn0prpwlem  36335  knoppndvlem19  36543  areacirclem1  37727  areacirclem4  37730  cntotbnd  37815  lcmineqlem23  42063  aks6d1c1p3  42122  aks6d1c2p2  42131  aks6d1c3  42135  aks6d1c2lem4  42139  unitscyglem2  42208  unitscyglem4  42210  oddnumth  42323  sumcubes  42325  zdivgd  42349  dffltz  42646  irrapxlem5  42838  pellexlem2  42842  jm2.22  43007  jm2.20nn  43009  sqrtcval  43653  nzss  44329  binomcxplemnotnn0  44368  oddfl  45298  xralrple3  45391  sumnnodd  45649  limclner  45668  stoweidlem62  46079  stirlinglem1  46091  dirkertrigeqlem2  46116  dirkertrigeqlem3  46117  fourierdlem66  46189  fourierdlem73  46196  fourierdlem87  46210  qndenserrnbllem  46311  hoiqssbllem2  46640  2tceilhalfelfzo1  47342  fmtnoprmfac2lem1  47576  sfprmdvdsmersenne  47613  dfeven4  47648  oddflALTV  47673  nn0onn0exALTV  47709  perfectALTVlem2  47732  perfectALTV  47733  nn0onn0ex  48534  affinecomb2  48714  line2ylem  48762  line2xlem  48764  itscnhlc0yqe  48770  itsclquadb  48787