Theorem divcan2d 12064

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

Proof of Theorem divcan2d

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  (class class class)co 7408  ℂcc 11169  0cc0 11171   · cmul 11176   / cdiv 11942

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248

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 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-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-div 11943

This theorem is used by:  nneo  12752  zeo2  12755  intfracq  13967  discr  14351  hashf1  14569  caurcvgr  15808  iseralt  15819  mertenslem1  16020  fprodle  16130  bpoly4  16192  tanadd  16302  divconjdvds  16452  mod2eq1n2dvds  16484  bitsmod  16573  mulgcd  16685  qredeq  16794  qredeu  16795  prmind2  16822  isprm5  16845  pythagtriplem19  16972  pcprendvds2  16980  pcpremul  16982  pcadd  17028  prmreclem1  17055  4sqlem19  17102  ablfac1lem  20245  pgpfac1lem3  20254  prmirredlem  21739  znrrg  21832  metnrmlem3  25142  lebnumlem3  25245  pcoass  25306  ipcau2  25516  4cphipval2  25524  minveclem3  25711  sca2rab  25794  ovolscalem1  25795  uniioombllem4  25868  uniioombl  25871  itg1mulc  25986  itg2const2  26023  dvrec  26236  dveflem  26260  lhop1  26295  vieta1  26598  elqaalem3  26607  abelthlem8  26729  tangtx  26797  tanregt0  26830  eff1olem  26839  eflogeq  26893  argregt0  26901  argrege0  26902  argimgt0  26903  cxpeq  27048  ang180lem5  27104  lawcoslem1  27106  isosctrlem2  27110  isosctrlem3  27111  heron  27129  dcubic1lem  27134  dcubic2  27135  dcubic1  27136  mcubic  27138  dquartlem1  27142  dquart  27144  quart1lem  27146  quart1  27147  quart  27152  atantayl2  27229  birthdaylem2  27243  ftalem5  27367  basellem3  27373  basellem4  27374  fsumdvdsdiaglem  27473  logexprlim  27515  mersenne  27517  perfectlem2  27520  perfect  27521  bposlem9  27582  lgsqrlem2  27637  lgseisenlem1  27665  lgseisenlem3  27667  lgsquadlem1  27670  lgsquad2lem1  27674  m1lgs  27678  2sqlem8  27716  rplogsumlem1  27774  dchrvmasumiflem2  27792  dchrisum0flblem2  27799  dchrisum0fno1  27801  dchrisum0lem1  27806  mulog2sumlem3  27826  selberglem2  27836  selberg3lem1  27847  selberg4lem1  27850  selberg3r  27859  selberg4r  27860  pntrlog2bndlem2  27868  pntlemg  27888  axsegconlem10  29437  axeuclidlem  29473  quad3d  33274  constrinvcl  34338  cos9thpiminplylem3  34349  oddpwdc  34920  subfacval2  35873  circum  36360  faclimlem1  36429  nn0prpwlem  37032  knoppndvlem19  37318  areacirclem1  38546  areacirclem4  38549  cntotbnd  38650  lcmineqlem23  43021  aks6d1c1p3  43080  aks6d1c2p2  43089  aks6d1c3  43093  aks6d1c2lem4  43097  unitscyglem2  43166  unitscyglem4  43168  quadfac  43175  oddnumth  43290  sumcubes  43292  zdivgd  43316  dffltz  43584  irrapxlem5  43771  pellexlem2  43775  jm2.22  43940  jm2.20nn  43942  sqrtcval  44585  nzss  45245  binomcxplemnotnn0  45284  oddfl  46215  xralrple3  46307  sumnnodd  46564  limclner  46583  stoweidlem62  46994  stirlinglem1  47006  dirkertrigeqlem2  47031  dirkertrigeqlem3  47032  fourierdlem66  47104  fourierdlem73  47111  fourierdlem87  47125  qndenserrnbllem  47226  hoiqssbllem2  47555  2tceilhalfelfzo1  48328  fmtnoprmfac2lem1  48573  sfprmdvdsmersenne  48610  dfeven4  48658  oddflALTV  48683  nn0onn0exALTV  48719  perfectALTVlem2  48742  perfectALTV  48743  nn0onn0ex  49557  affinecomb2  49737  line2ylem  49785  line2xlem  49787  itscnhlc0yqe  49793  itsclquadb  49810