Theorem divcan4d 12025

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  (class class class)co 7417  ℂcc 11126  0cc0 11128   · cmul 11133   / cdiv 11899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900

This theorem is used by:  mvllmuld  12075  ldiv  12077  mulge0b  12113  ltmuldiv  12116  rimul  12237  mul2lt0rlt0  13150  mulmod0  13942  2txmodxeq0  13999  expaddzlem  14173  mulsubdivbinom2  14330  facdiv  14355  permnn  14394  cjdiv  15255  sqrtdiv  15356  absdiv  15386  sqreulem  15451  gcddiv  16647  divgcdcoprm0  16761  hashgcdlem  16885  sylow2blem3  19755  cnflddiv  21621  cnsubrg  21646  i1fmullem  25928  mbfi1fseqlem3  25951  mbfi1fseqlem6  25954  dvsincos  26215  ftc1lem4  26273  vieta1lem2  26550  aaliou3lem9  26593  root1eq1  27000  nnlogbexp  27026  relogbcxp  27030  lawcoslem1  27060  chordthmlem2  27078  chordthmlem4  27080  dcubic1lem  27088  dcubic2  27089  dquartlem1  27096  efiatan2  27162  tanatan  27164  regamcl  27305  basellem3  27327  bclbnd  27524  gausslemma2dlem3  27612  2lgslem1a2  27634  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2sqlem3  27664  vmadivsum  27726  dchrmusum2  27738  dchrmusumlem  27766  vmalogdivsum  27783  selberg3lem1  27801  pntrlog2bndlem4  27824  pntlemb  27841  nrt2irr  30961  normcan  32065  constrrtcc  34253  constrreinvcl  34290  dya2icoseg  34796  bayesth  34958  signsplypnf  35066  divsqrtid  35110  bj-bary1lem  38070  ftc1cnnclem  38448  dvasin  38461  3lexlogpow2ineq2  42933  2np3bcnp1  43018  unitscyglem2  43070  cxp112d  43224  fltnlta  43517  3cubeslem4  43542  pellexlem2  43679  pellexlem6  43683  proot1ex  44045  divcan8d  46153  wallispilem5  46905  stirlinglem3  46912  stirlinglem4  46913  stirlinglem15  46924  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  dirkercncflem4  46942  fourierdlem6  46949  fourierdlem19  46962  fourierdlem26  46969  fourierdlem39  46982  fourierdlem42  46985  fourierdlem63  47005  fourierdlem65  47007  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem103  47045  fourierdlem104  47046  ppivalnnprm  48536  ppivalnnnprmge6  48537  2zrngnmlid  49178  1subrec1sub  49643  mvlrmuld  50713