Theorem divcan3d 12068

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

Proof of Theorem divcan3d

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcan3 11970	. 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 11170  0cc0 11172   · cmul 11177   / cdiv 11943

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 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248  ax-pre-mulgt0 11249

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 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-sub 11515  df-neg 11516  df-div 11944

This theorem is used by:  prodgt0  12134  mulge0b  12157  ltdivmul  12162  ledivmul  12163  zneo  12752  2tnp1ge0ge0  13938  quoremz  13964  quoremnn0ALT  13966  moddiffl  13991  zesq  14338  discr  14352  bcn1  14425  crre  15249  abslem2  15475  fallfacval4  16177  sinhval  16290  eirrlem  16340  sqrt2irrlem  16384  ltoddhalfle  16499  flodddiv4  16553  bitsp1e  16570  bitsp1o  16571  iserodd  16975  fldivp1  17037  4sqlem17  17101  smndex2dlinvh  19078  gexexlem  20028  abv1z  21043  gzrngunit  21701  cphipval2  25524  ovolunlem1a  25779  itg1mulc  25987  dvrec  26237  elqaalem3  26608  eff1olem  26840  logf1o2  26942  isosctrlem2  27111  heron  27130  dcubic2  27136  mcubic  27139  cubic2  27140  dquartlem1  27143  dquartlem2  27144  dquart  27145  cosasin  27196  efiatan2  27209  tanatan  27211  dvatan  27227  atantayl3  27231  jensen  27280  basellem3  27374  basellem5  27376  basellem8  27379  logfacrlim  27515  perfectlem2  27521  lgsquadlem1  27671  lgsquadlem2  27672  2lgslem1c  27684  2lgslem3a  27687  dchrvmasumlem1  27786  mudivsum  27821  vmalogdivsum2  27829  logsqvma  27833  selberglem2  27837  selberglem3  27838  selberg  27839  selbergr  27859  selberg3r  27860  selberg4r  27861  selberg34r  27862  pntsval2  27867  pntpbnd1a  27876  pntibndlem2  27882  axsegconlem9  29437  cdj1i  32969  quad3d  33275  constrresqrtcl  34343  subfacval2  35873  circum  36360  knoppndvlem2  37301  knoppndvlem9  37308  areacirclem1  38546  areacirclem4  38549  lcmineqlem11  43009  aks4d1p1p4  43041  unitscyglem4  43168  zdivgd  43316  cxp111d  43321  readvrec2  43340  sqrtcval  44585  hashnzfzclim  45250  dmmcand  46250  sumnnodd  46564  sinmulcos  46797  itgsinexp  46887  itgcoscmulx  46901  itgsincmulx  46906  stirlinglem7  47012  dirkertrigeqlem3  47032  dirkeritg  47034  dirkercncflem2  47036  fourierdlem79  47117  fourierdlem83  47121  fourierdlem95  47133  fouriercnp  47158  fourierswlem  47162  etransclem24  47190  etransclem41  47207  sfprmdvdsmersenne  48610  dfodd6  48657  dfeven4  48658  perfectALTVlem2  48742  line2  49786  itscnhlc0xyqsol  49799  itsclquadb  49810  sinhpcosh  50755