Theorem divcan1d 11411

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
divcan1d	⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)

Proof of Theorem divcan1d

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcan1 11301	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  (class class class)co 7150  ℂcc 10529  0cc0 10531   · cmul 10536   / cdiv 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292

This theorem is referenced by:  ldiv  11468  ltdiv23  11525  lediv23  11526  recp1lt1  11532  ledivp1  11536  subhalfhalf  11865  xp1d2m1eqxm1d2  11885  div4p1lem1div2  11886  qmulz  12345  iccf1o  12876  ltdifltdiv  13198  bcpasc  13675  sqrtdiv  14619  geo2sum  15223  sqrt2irrlem  15595  dvdsval2  15604  flodddiv4t2lthalf  15761  bitsres  15816  bitsuz  15817  dvdsgcdidd  15879  mulgcddvds  15993  qredeq  15995  isprm6  16052  qmuldeneqnum  16081  hashgcdlem  16119  pcqdiv  16188  pockthlem  16235  prmreclem3  16248  4sqlem5  16272  4sqlem12  16286  4sqlem15  16289  sylow3lem4  18749  odadd1  18962  odadd2  18963  gexexlem  18966  pgpfac1lem3a  19192  pgpfac1lem3  19193  znidomb  20702  znrrg  20706  nmoleub2lem  23712  nmoleub3  23717  i1fmullem  24289  mbfi1fseqlem3  24312  mbfi1fseqlem4  24313  mbfi1fseqlem5  24314  dvcnp2  24511  dvlip  24584  plydivlem4  24879  cosne0  25108  advlogexp  25232  root1id  25329  cxplogb  25358  ang180lem1  25381  ang180lem3  25383  angpieqvd  25403  chordthmlem  25404  dcubic2  25416  dcubic  25418  dquartlem2  25424  cxploglim2  25550  fsumdvdsdiaglem  25754  logexprlim  25795  bposlem3  25856  lgslem1  25867  gausslemma2dlem1a  25935  lgsquadlem1  25950  2lgslem1a1  25959  log2sumbnd  26114  chpdifbndlem1  26123  selberg4lem1  26130  pntrlog2bndlem3  26149  pntibndlem2  26161  pntlemr  26172  ostth2lem3  26205  ostth2  26207  ostth3  26208  axcontlem7  26750  blocnilem  28575  qqhval2lem  31217  cndprobin  31687  itgexpif  31872  faclimlem1  32970  faclimlem3  32972  nn0prpwlem  33665  itg2addnclem3  34939  bfplem1  35094  rrncmslem  35104  rrnequiv  35107  pellexlem6  39424  jm2.19  39583  jm2.27c  39597  binomcxplemnotnn0  40681  sineq0ALT  41264  xralrple2  41615  ltdiv23neg  41659  stoweidlem42  42321  stirlinglem3  42355  dirkertrigeq  42380  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem4  42390  fourierdlem63  42448  fourierdlem65  42450  fourierdlem83  42468  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  etransclem38  42551  smfmullem1  43060  sigarcol  43115  sharhght  43116  proththd  43773  mod0mul  44573  nn0sumshdiglemA  44673  rrx2vlinest  44722