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

Theorem divrecd 10656
Description: Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1 (𝜑𝐴 ∈ ℂ)
divcld.2 (𝜑𝐵 ∈ ℂ)
divcld.3 (𝜑𝐵 ≠ 0)
Assertion
Ref Expression
divrecd (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))

Proof of Theorem divrecd
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 divcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 divcld.3 . 2 (𝜑𝐵 ≠ 0)
4 divrec 10553 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
51, 2, 3, 4syl3anc 1317 1 (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  wne 2779  (class class class)co 6527  cc 9791  0cc0 9793  1c1 9794   · cmul 9798   / cdiv 10536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537
This theorem is referenced by:  prodgt0  10720  ltdiv1  10739  ltrec  10757  lediv12a  10768  expsub  12728  expdiv  12731  rlimdiv  14173  isumdivc  14286  fsumdivc  14309  trirecip  14383  geo2sum  14392  geo2lim  14394  prodfdiv  14416  ege2le3  14608  eftlub  14627  eirrlem  14720  prmreclem4  15410  m1expaddsub  17690  abvdiv  18609  cnsubrg  19574  nmdvr  22232  nmoi2  22292  cphdivcl  22735  ipcau2  22786  ovolsca  23035  dvsincos  23493  plyeq0lem  23715  plydivlem4  23800  aalioulem4  23839  geolim3  23843  aaliou3lem8  23849  taylthlem2  23877  advlogexp  24146  cxpsub  24173  divcxp  24178  dvcxp1  24226  dvcncxp1  24229  relogbdiv  24262  lawcoslem1  24290  dvatan  24407  leibpi  24414  log2tlbnd  24417  fsumharmonic  24483  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamgulmlem4  24503  basellem8  24559  chebbnd1  24906  rplogsumlem2  24919  rpvmasumlem  24921  dchrmusumlema  24927  dchrisum0lema  24948  dchrisum0lem1  24950  dchrisum0lem2a  24951  dchrisum0lem2  24952  dchrmusumlem  24956  mulogsumlem  24965  mulogsum  24966  logdivsum  24967  mulog2sumlem1  24968  vmalogdivsum2  24972  2vmadivsumlem  24974  log2sumbnd  24978  logdivbnd  24990  selberg4lem1  24994  selberg34r  25005  pntrlog2bndlem2  25012  pntrlog2bndlem4  25014  pntrlog2bndlem6  25017  pntpbnd2  25021  smcnlem  26765  ipasslem5  26908  omssubadd  29523  knoppndvlem14  31520  dvtan  32454  areacirclem1  32494  areacirclem4  32497  irrapxlem5  36232  pell14qrdivcl  36271  hashnzfzclim  37367  binomcxplemnotnn0  37401  ltdiv23neg  38382  climdivf  38503  divlimc  38547  divcncf  38593  dvmptdiv  38631  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnxpaek  38656  stoweidlem36  38753  wallispi  38787  stirlinglem7  38797  dirkercncflem2  38821  dirkercncflem4  38823  fourierdlem39  38863  fourierdlem40  38864  fourierdlem56  38879  fourierdlem62  38885  fourierdlem78  38901  fourierdlem83  38906  fourierdlem95  38918  smfdiv  39506  dignn0flhalflem1  42229  amgmlemALT  42341  young2d  42343
  Copyright terms: Public domain W3C validator