Theorem divcan1d 11993

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  (class class class)co 7412  ℂcc 11099  0cc0 11101   · cmul 11106   / cdiv 11872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  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 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-div 11873

This theorem is referenced by:  ldiv  12050  ltdiv23  12107  lediv23  12108  recp1lt1  12114  ledivp1  12118  subhalfhalf  12479  xp1d2m1eqxm1d2  12499  div4p1lem1div2  12500  qmulz  12976  iccf1o  13524  ltdifltdiv  13869  bcpasc  14359  sqrtdiv  15318  geo2sum  15929  sqrt2irrlem  16305  dvdsval2  16314  flodddiv4t2lthalf  16477  bitsres  16532  bitsuz  16533  dvdsgcdidd  16596  mulgcddvds  16714  qredeq  16716  isprm6  16774  qmuldeneqnum  16807  hashgcdlem  16848  pcqdiv  16918  pockthlem  16966  prmreclem3  16979  4sqlem5  17003  4sqlem12  17017  4sqlem15  17020  sylow3lem4  19701  odadd1  19919  odadd2  19920  gexexlem  19923  pgpfac1lem3a  20149  pgpfac1lem3  20150  znidomb  21692  znrrg  21696  nmoleub2lem  25254  nmoleub3  25259  i1fmullem  25834  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  dvcnp2  26060  dvlip  26133  plydivlem4  26438  cosne0  26675  advlogexp  26801  root1id  26900  cxplogb  26932  ang180lem1  26955  ang180lem3  26957  angpieqvd  26977  chordthmlem  26978  dcubic2  26990  dcubic  26992  dquartlem2  26998  cxploglim2  27124  fsumdvdsdiaglem  27328  logexprlim  27370  bposlem3  27431  lgslem1  27442  gausslemma2dlem1a  27510  lgsquadlem1  27525  2lgslem1a1  27534  log2sumbnd  27689  chpdifbndlem1  27698  selberg4lem1  27705  pntrlog2bndlem3  27724  pntibndlem2  27736  pntlemr  27747  ostth2lem3  27780  ostth2  27782  ostth3  27783  axcontlem7  29301  blocnilem  31137  zringfrac  33825  constrrtcclem  34105  cos9thpiminplylem2  34154  qqhval2lem  34352  cndprobin  34805  itgexpif  34974  faclimlem1  36216  faclimlem3  36218  nn0prpwlem  36814  itg2addnclem3  38305  bfplem1  38454  rrncmslem  38464  rrnequiv  38467  nnproddivdvdsd  42748  lcmineqlem12  42788  3lexlogpow5ineq2  42803  3lexlogpow2ineq1  42806  aks4d1p8  42835  unitscyglem2  42944  readvrec2  43103  pellexlem6  43544  jm2.19  43703  jm2.27c  43717  binomcxplemnotnn0  45049  sineq0ALT  45628  xralrple2  46053  ltdiv23neg  46092  stoweidlem42  46739  stirlinglem3  46773  dirkertrigeq  46798  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem4  46808  fourierdlem63  46866  fourierdlem65  46868  fourierdlem83  46886  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  etransclem38  46969  smfmullem1  47488  sigarcol  47561  sharhght  47562  mod0mul  48082  proththd  48349  nn0sumshdiglemA  49382  rrx2vlinest  49504