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

Theorem divcan2d 10373
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 10266 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( B  x.  ( A  /  B ) )  =  A )
51, 2, 3, 4syl3anc 1271 1  |-  ( ph  ->  ( B  x.  ( A  /  B ) )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1447    e. wcel 1890    =/= wne 2621  (class class class)co 6275   CCcc 9523   0cc0 9525    x. cmul 9530    / cdiv 10257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258
This theorem is referenced by:  nneo  11008  zeo2  11011  intfracq  12079  discr  12402  hashf1  12614  caurcvgr  13748  caurcvgrOLD  13749  iseralt  13761  mertenslem1  13950  fprodle  14060  bpoly4  14122  tanadd  14231  bitsmod  14420  mulgcd  14524  prmind2  14645  isprm5  14661  qredeq  14673  qredeu  14674  pythagtriplem19  14793  pcprendvds2  14801  pcpremul  14803  pcadd  14844  prmreclem1  14870  4sqlem19  14923  ablfac1lem  17711  pgpfac1lem3  17720  prmirredlem  19074  znrrg  19146  metnrmlem3  21888  metnrmlem3OLD  21903  lebnumlem3  22001  lebnumlem3OLD  22004  pcoass  22065  ipcau2  22218  minveclem3  22381  minveclem3OLD  22393  sca2rab  22475  ovolscalem1  22476  uniioombllem4  22555  uniioombl  22558  itg1mulc  22673  itg2const2  22710  dvrec  22920  dveflem  22942  lhop1  22977  vieta1  23276  elqaalem3  23285  elqaalem3OLD  23288  abelthlem8  23405  tangtx  23471  tanregt0  23499  eff1olem  23508  eflogeq  23562  argregt0  23570  argrege0  23571  argimgt0  23572  cxpeq  23708  ang180lem5  23753  lawcoslem1  23755  isosctrlem2  23759  isosctrlem3  23760  heron  23775  dcubic1lem  23780  dcubic2  23781  dcubic1  23782  mcubic  23784  dquartlem1  23788  dquart  23790  quart1lem  23792  quart1  23793  quart  23798  atantayl2  23875  birthdaylem2  23889  ftalem5  24012  ftalem5OLD  24014  basellem3  24020  basellem4  24021  dvdsdivcl  24121  fsumdvdsdiaglem  24123  logexprlim  24164  mersenne  24166  perfectlem2  24169  perfect  24170  bposlem9  24231  lgsqrlem2  24281  lgseisenlem1  24288  lgseisenlem3  24290  lgsquadlem1  24293  lgsquad2lem1  24297  m1lgs  24301  2sqlem8  24311  rplogsumlem1  24333  dchrvmasumiflem2  24351  dchrisum0flblem2  24358  dchrisum0fno1  24360  dchrisum0lem1  24365  mulog2sumlem3  24385  selberglem2  24395  selberg3lem1  24406  selberg4lem1  24409  selberg3r  24418  selberg4r  24419  pntrlog2bndlem2  24427  pntlemg  24447  axsegconlem10  24967  axeuclidlem  25003  oddpwdc  29192  subfacval2  29915  circum  30323  faclimlem1  30384  nn0prpwlem  30983  areacirclem1  32033  areacirclem4  32036  cntotbnd  32129  irrapxlem5  35671  pellexlem2  35675  jm2.22  35851  jm2.20nn  35853  nzss  36666  binomcxplemnotnn0  36705  oddfl  37517  sumnnodd  37751  limclner  37773  stoweidlem62  37979  stoweidlem62OLD  37980  stirlinglem1  37992  dirkertrigeqlem2  38017  dirkertrigeqlem3  38018  fourierdlem66  38092  fourierdlem73  38099  fourierdlem87  38113  qndenserrnbllem  38219  hoiqssbllem2  38507  mod2eq1n2dvds  38815  elmod2OLD  38816  dfeven4  38858  oddflALTV  38882  nn0onn0exALTV  38917  perfectALTVlem2  38934  perfectALTV  38935  nn0onn0ex  40655
  Copyright terms: Public domain W3C validator