MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divcan4d Structured version   Visualization version   GIF version

Theorem divcan4d 11060
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
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 divcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 divcld.3 . 2 (𝜑𝐵 ≠ 0)
4 divcan4 10965 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
51, 2, 3, 4syl3anc 1490 1 (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  wne 2936  (class class class)co 6841  cc 10186  0cc0 10188   · cmul 10193   / cdiv 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-po 5197  df-so 5198  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938
This theorem is referenced by:  mvllmuld  11110  mulge0b  11146  ltmuldiv  11149  rimul  11264  mul2lt0rlt0  12129  mulmod0  12883  2txmodxeq0  12937  expaddzlem  13109  mulsubdivbinom2  13252  facdiv  13277  permnn  13316  cjdiv  14190  sqrtdiv  14292  absdiv  14321  sqreulem  14385  gcddiv  15550  divgcdcoprm0  15660  hashgcdlem  15773  sylow2blem3  18302  cnflddiv  20048  cnsubrg  20078  i1fmullem  23751  mbfi1fseqlem3  23774  mbfi1fseqlem6  23777  dvsincos  24034  ftc1lem4  24092  vieta1lem2  24356  aaliou3lem9  24395  root1eq1  24786  nnlogbexp  24809  relogbcxp  24813  lawcoslem1  24835  chordthmlem2  24850  chordthmlem4  24852  dcubic1lem  24860  dcubic2  24861  dquartlem1  24868  efiatan2  24934  tanatan  24936  regamcl  25077  basellem3  25099  bclbnd  25295  gausslemma2dlem3  25383  2lgslem1a2  25405  2lgslem3b  25412  2lgslem3c  25413  2lgslem3d  25414  2sqlem3  25435  vmadivsum  25461  dchrmusum2  25473  dchrmusumlem  25501  vmalogdivsum  25518  selberg3lem1  25536  pntrlog2bndlem4  25559  pntlemb  25576  normcan  28825  dya2icoseg  30720  bayesth  30883  signsplypnf  31009  divsqrtid  31054  bj-ldiv  33521  bj-bary1lem  33526  ftc1cnnclem  33838  dvasin  33851  pellexlem2  38004  pellexlem6  38008  proot1ex  38388  divcan8d  40097  wallispilem5  40855  stirlinglem3  40862  stirlinglem4  40863  stirlinglem15  40874  dirkertrigeqlem1  40884  dirkertrigeqlem2  40885  dirkertrigeqlem3  40886  dirkercncflem4  40892  fourierdlem6  40899  fourierdlem19  40912  fourierdlem26  40919  fourierdlem39  40932  fourierdlem42  40935  fourierdlem63  40955  fourierdlem65  40957  fourierdlem89  40981  fourierdlem90  40982  fourierdlem91  40983  fourierdlem103  40995  fourierdlem104  40996  2zrngnmlid  42550  mvlrmuld  43126
  Copyright terms: Public domain W3C validator