Theorem divcan4d 12102

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 12004	. 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 11201  0cc0 11203   · cmul 11208   / cdiv 11976

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 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

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 4585  df-pr 4587  df-op 4835  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 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977

This theorem is used by:  mvllmuld  12152  ldiv  12154  mulge0b  12190  ltmuldiv  12193  rimul  12314  mul2lt0rlt0  13227  mulmod0  14020  2txmodxeq0  14077  expaddzlem  14251  mulsubdivbinom2  14409  facdiv  14434  permnn  14473  cjdiv  15336  sqrtdiv  15437  absdiv  15467  sqreulem  15532  gcddiv  16729  divgcdcoprm0  16845  hashgcdlem  16970  sylow2blem3  19841  cnflddiv  21713  cnsubrg  21738  i1fmullem  26020  mbfi1fseqlem3  26043  mbfi1fseqlem6  26046  dvsincos  26306  ftc1lem4  26364  vieta1lem2  26639  aaliou3lem9  26682  root1eq1  27088  nnlogbexp  27114  relogbcxp  27118  lawcoslem1  27148  chordthmlem2  27166  chordthmlem4  27168  dcubic1lem  27176  dcubic2  27177  dquartlem1  27184  efiatan2  27250  tanatan  27252  regamcl  27393  basellem3  27415  bclbnd  27612  gausslemma2dlem3  27700  2lgslem1a2  27722  2lgslem3b  27729  2lgslem3c  27730  2lgslem3d  27731  2sqlem3  27752  vmadivsum  27814  dchrmusum2  27826  dchrmusumlem  27854  vmalogdivsum  27871  selberg3lem1  27889  pntrlog2bndlem4  27912  pntlemb  27929  nrt2irr  31079  normcan  32183  constrrtcc  34413  constrreinvcl  34450  dya2icoseg  34955  bayesth  35117  signsplypnf  35225  divsqrtid  35269  bj-bary1lem  38324  ftc1cnnclem  38702  dvasin  38715  3lexlogpow2ineq2  43202  2np3bcnp1  43287  unitscyglem2  43339  cxp112d  43485  fltnlta  43767  3cubeslem4  43792  pellexlem2  43930  pellexlem6  43934  proot1ex  44291  divcan8d  46421  wallispilem5  47172  stirlinglem3  47179  stirlinglem4  47180  stirlinglem15  47191  dirkertrigeqlem1  47201  dirkertrigeqlem2  47202  dirkertrigeqlem3  47203  dirkercncflem4  47209  fourierdlem6  47216  fourierdlem19  47229  fourierdlem26  47236  fourierdlem39  47249  fourierdlem42  47252  fourierdlem63  47272  fourierdlem65  47274  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem103  47312  fourierdlem104  47313  ppivalnnprm  48803  ppivalnnnprmge6  48804  2zrngnmlid  49445  1subrec1sub  49910  mvlrmuld  51040