Theorem divcan4d 11757

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

Proof of Theorem divcan4d

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  (class class class)co 7275  ℂcc 10869  0cc0 10871   · cmul 10876   / cdiv 11632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633

This theorem is referenced by:  mvllmuld  11807  ldiv  11809  mulge0b  11845  ltmuldiv  11848  rimul  11964  mul2lt0rlt0  12832  mulmod0  13597  2txmodxeq0  13651  expaddzlem  13826  mulsubdivbinom2  13976  facdiv  14001  permnn  14040  cjdiv  14875  sqrtdiv  14977  absdiv  15007  sqreulem  15071  gcddiv  16259  divgcdcoprm0  16370  hashgcdlem  16489  sylow2blem3  19227  cnflddiv  20628  cnsubrg  20658  i1fmullem  24858  mbfi1fseqlem3  24882  mbfi1fseqlem6  24885  dvsincos  25145  ftc1lem4  25203  vieta1lem2  25471  aaliou3lem9  25510  root1eq1  25908  nnlogbexp  25931  relogbcxp  25935  lawcoslem1  25965  chordthmlem2  25983  chordthmlem4  25985  dcubic1lem  25993  dcubic2  25994  dquartlem1  26001  efiatan2  26067  tanatan  26069  regamcl  26210  basellem3  26232  bclbnd  26428  gausslemma2dlem3  26516  2lgslem1a2  26538  2lgslem3b  26545  2lgslem3c  26546  2lgslem3d  26547  2sqlem3  26568  vmadivsum  26630  dchrmusum2  26642  dchrmusumlem  26670  vmalogdivsum  26687  selberg3lem1  26705  pntrlog2bndlem4  26728  pntlemb  26745  normcan  29938  dya2icoseg  32244  bayesth  32406  signsplypnf  32529  divsqrtid  32574  bj-bary1lem  35481  ftc1cnnclem  35848  dvasin  35861  3lexlogpow2ineq2  40067  2np3bcnp1  40100  fltnlta  40500  3cubeslem4  40511  pellexlem2  40652  pellexlem6  40656  proot1ex  41026  divcan8d  42851  wallispilem5  43610  stirlinglem3  43617  stirlinglem4  43618  stirlinglem15  43629  dirkertrigeqlem1  43639  dirkertrigeqlem2  43640  dirkertrigeqlem3  43641  dirkercncflem4  43647  fourierdlem6  43654  fourierdlem19  43667  fourierdlem26  43674  fourierdlem39  43687  fourierdlem42  43690  fourierdlem63  43710  fourierdlem65  43712  fourierdlem89  43736  fourierdlem90  43737  fourierdlem91  43738  fourierdlem103  43750  fourierdlem104  43751  2zrngnmlid  45507  1subrec1sub  46051  mvlrmuld  46480