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

Theorem divrecd 11413
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 11308 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
51, 2, 3, 4syl3anc 1368 1 (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  wne 3014  (class class class)co 7146  cc 10529  0cc0 10531  1c1 10532   · cmul 10536   / cdiv 11291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-po 5462  df-so 5463  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292
This theorem is referenced by:  prodgt0  11481  ltdiv1  11498  ltrec  11516  lediv12a  11527  expsub  13480  expdiv  13483  rlimdiv  15000  isumdivc  15117  fsumdivc  15139  trirecip  15216  geo2sum  15227  geo2lim  15229  prodfdiv  15250  ege2le3  15441  eftlub  15460  eirrlem  15555  prmreclem4  16251  m1expaddsub  18624  abvdiv  19603  cnsubrg  20600  nmdvr  23274  nmoi2  23334  cphdivcl  23785  ipcau2  23836  divcncf  24049  ovolsca  24117  dvmptdiv  24575  dvsincos  24582  plyeq0lem  24805  plydivlem4  24890  aalioulem4  24929  geolim3  24933  aaliou3lem8  24939  taylthlem2  24967  advlogexp  25244  cxpsub  25271  divcxp  25276  dvcxp1  25327  dvcncxp1  25330  relogbdiv  25363  lawcoslem1  25399  dvatan  25519  leibpi  25526  log2tlbnd  25529  fsumharmonic  25595  lgamgulmlem2  25613  lgamgulmlem3  25614  lgamgulmlem4  25615  basellem8  25671  chebbnd1  26054  rplogsumlem2  26067  rpvmasumlem  26069  dchrmusumlema  26075  dchrisum0lema  26096  dchrisum0lem1  26098  dchrisum0lem2a  26099  dchrisum0lem2  26100  dchrmusumlem  26104  mulogsumlem  26113  mulogsum  26114  logdivsum  26115  mulog2sumlem1  26116  vmalogdivsum2  26120  2vmadivsumlem  26122  log2sumbnd  26126  logdivbnd  26138  selberg4lem1  26142  selberg34r  26153  pntrlog2bndlem2  26160  pntrlog2bndlem4  26162  pntrlog2bndlem6  26165  pntpbnd2  26169  smcnlem  28478  ipasslem5  28616  omssubadd  31585  logdivsqrle  31948  knoppndvlem14  33891  dvtan  35019  areacirclem1  35057  areacirclem4  35060  lcmineqlem5  39229  lcmineqlem16  39240  irrapxlem5  39623  pell14qrdivcl  39662  hashnzfzclim  40886  binomcxplemnotnn0  40920  ltdiv23neg  41896  climdivf  42120  divlimc  42164  ioodvbdlimc1lem2  42440  ioodvbdlimc2lem  42442  dvnxpaek  42450  stoweidlem36  42544  wallispi  42578  stirlinglem7  42588  dirkercncflem2  42612  dirkercncflem4  42614  fourierdlem39  42654  fourierdlem40  42655  fourierdlem56  42670  fourierdlem62  42676  fourierdlem78  42692  fourierdlem83  42697  fourierdlem95  42709  smfdiv  43295  dignn0flhalflem1  44894  amgmlemALT  45185  young2d  45187
  Copyright terms: Public domain W3C validator