Theorem divcan2d 12095

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  (class class class)co 7420  ℂcc 11198  0cc0 11200   · cmul 11205   / cdiv 11973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974

This theorem is used by:  nneo  12783  zeo2  12786  intfracq  13999  discr  14384  hashf1  14602  caurcvgr  15841  iseralt  15852  mertenslem1  16053  fprodle  16163  bpoly4  16225  tanadd  16335  divconjdvds  16485  mod2eq1n2dvds  16517  bitsmod  16606  mulgcd  16721  qredeq  16832  qredeu  16833  prmind2  16860  isprm5  16883  pythagtriplem19  17011  pcprendvds2  17019  pcpremul  17021  pcadd  17067  prmreclem1  17094  4sqlem19  17141  ablfac1lem  20284  pgpfac1lem3  20293  prmirredlem  21778  znrrg  21871  metnrmlem3  25181  lebnumlem3  25284  pcoass  25345  ipcau2  25555  4cphipval2  25563  minveclem3  25750  sca2rab  25833  ovolscalem1  25834  uniioombllem4  25907  uniioombl  25910  itg1mulc  26025  itg2const2  26062  dvrec  26275  dveflem  26299  lhop1  26334  vieta1  26635  elqaalem3  26644  abelthlem8  26766  tangtx  26834  tanregt0  26867  eff1olem  26876  eflogeq  26930  argregt0  26938  argrege0  26939  argimgt0  26940  cxpeq  27085  ang180lem5  27141  lawcoslem1  27143  isosctrlem2  27147  isosctrlem3  27148  heron  27166  dcubic1lem  27171  dcubic2  27172  dcubic1  27173  mcubic  27175  dquartlem1  27179  dquart  27181  quart1lem  27183  quart1  27184  quart  27189  atantayl2  27266  birthdaylem2  27280  ftalem5  27404  basellem3  27410  basellem4  27411  fsumdvdsdiaglem  27510  logexprlim  27552  mersenne  27554  perfectlem2  27557  perfect  27558  bposlem9  27619  lgsqrlem2  27674  lgseisenlem1  27702  lgseisenlem3  27704  lgsquadlem1  27707  lgsquad2lem1  27711  m1lgs  27715  2sqlem8  27753  rplogsumlem1  27811  dchrvmasumiflem2  27829  dchrisum0flblem2  27836  dchrisum0fno1  27838  dchrisum0lem1  27843  mulog2sumlem3  27863  selberglem2  27873  selberg3lem1  27884  selberg4lem1  27887  selberg3r  27896  selberg4r  27897  pntrlog2bndlem2  27905  pntlemg  27925  axsegconlem10  29504  axeuclidlem  29540  quad3d  33383  constrinvcl  34447  cos9thpiminplylem3  34458  oddpwdc  35028  subfacval2  35994  circum  36481  faclimlem1  36550  nn0prpwlem  37152  knoppndvlem19  37438  areacirclem1  38669  areacirclem4  38672  cntotbnd  38773  lcmineqlem23  43144  aks6d1c1p3  43203  aks6d1c2p2  43212  aks6d1c3  43216  aks6d1c2lem4  43220  unitscyglem2  43289  unitscyglem4  43291  quadfac  43298  oddnumth  43411  sumcubes  43413  zdivgd  43431  dffltz  43713  irrapxlem5  43876  pellexlem2  43880  jm2.22  44045  jm2.20nn  44047  sqrtcval  44684  nzss  45344  binomcxplemnotnn0  45383  oddfl  46337  xralrple3  46428  sumnnodd  46685  limclner  46704  stoweidlem62  47115  stirlinglem1  47127  dirkertrigeqlem2  47152  dirkertrigeqlem3  47153  fourierdlem66  47225  fourierdlem73  47232  fourierdlem87  47246  qndenserrnbllem  47347  hoiqssbllem2  47676  2tceilhalfelfzo1  48449  fmtnoprmfac2lem1  48694  sfprmdvdsmersenne  48731  dfeven4  48779  oddflALTV  48804  nn0onn0exALTV  48840  perfectALTVlem2  48863  perfectALTV  48864  nn0onn0ex  49678  affinecomb2  49858  line2ylem  49906  line2xlem  49908  itscnhlc0yqe  49914  itsclquadb  49931