MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divcan2d Unicode version

Theorem divcan2d 9726
Description: A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1  |-  ( ph  ->  A  e.  CC )
divcld.2  |-  ( ph  ->  B  e.  CC )
divcld.3  |-  ( ph  ->  B  =/=  0 )
Assertion
Ref Expression
divcan2d  |-  ( ph  ->  ( B  x.  ( A  /  B ) )  =  A )

Proof of Theorem divcan2d
StepHypRef Expression
1 div1d.1 . 2  |-  ( ph  ->  A  e.  CC )
2 divcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 divcld.3 . 2  |-  ( ph  ->  B  =/=  0 )
4 divcan2 9620 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( B  x.  ( A  /  B ) )  =  A )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( B  x.  ( A  /  B ) )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717    =/= wne 2552  (class class class)co 6022   CCcc 8923   0cc0 8925    x. cmul 8930    / cdiv 9611
This theorem is referenced by:  nneo  10287  zeo2  10290  intfracq  11169  discr  11445  hashf1  11635  caurcvgr  12396  iseralt  12407  mertenslem1  12590  tanadd  12697  bitsmod  12877  mulgcd  12975  prmind2  13019  qredeq  13035  qredeu  13036  isprm5  13041  pythagtriplem19  13136  pcprendvds2  13144  pcpremul  13146  pcadd  13187  prmreclem1  13213  4sqlem19  13260  ablfac1lem  15555  pgpfac1lem3  15564  prmirredlem  16698  znrrg  16771  metnrmlem3  18764  lebnumlem3  18861  pcoass  18922  ipcau2  19064  minveclem3  19199  sca2rab  19277  ovolscalem1  19278  uniioombllem4  19347  uniioombl  19350  itg1mulc  19465  itg2const2  19502  dvrec  19710  dveflem  19732  lhop1  19767  vieta1  20098  elqaalem3  20107  abelthlem8  20224  tangtx  20282  tanregt0  20310  eff1olem  20319  eflogeq  20365  argregt0  20374  argrege0  20375  argimgt0  20376  cxpeq  20510  ang180lem5  20524  lawcoslem1  20526  isosctrlem2  20532  isosctrlem3  20533  dcubic1lem  20552  dcubic2  20553  dcubic1  20554  mcubic  20556  dquartlem1  20560  dquart  20562  quart1lem  20564  quart1  20565  quart  20570  atantayl2  20647  birthdaylem2  20660  ftalem5  20728  basellem3  20734  basellem4  20735  dvdsdivcl  20835  fsumdvdsdiaglem  20837  logexprlim  20878  mersenne  20880  perfectlem2  20883  perfect  20884  bposlem9  20945  lgsqrlem2  20995  lgseisenlem1  21002  lgseisenlem3  21004  lgsquadlem1  21007  lgsquad2lem1  21011  m1lgs  21015  2sqlem8  21025  rplogsumlem1  21047  dchrvmasumiflem2  21065  dchrisum0flblem2  21072  dchrisum0fno1  21074  dchrisum0lem1  21079  mulog2sumlem3  21099  selberglem2  21109  selberg3lem1  21120  selberg4lem1  21123  selberg3r  21132  selberg4r  21133  pntrlog2bndlem2  21141  pntlemg  21161  subfacval2  24654  circum  24892  faclimlem1  25122  axsegconlem10  25581  axeuclidlem  25617  bpoly4  25821  areacirclem2  25984  areacirclem5  25988  nn0prpwlem  26018  cntotbnd  26198  irrapxlem5  26582  pellexlem2  26586  jm2.22  26759  jm2.20nn  26761  stoweidlem62  27481  stirlinglem1  27493
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-po 4446  df-so 4447  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-riota 6487  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612
  Copyright terms: Public domain W3C validator