Theorem divrecd 11684

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

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  (class class class)co 7255  ℂcc 10800  0cc0 10802  1c1 10803   · cmul 10807   / cdiv 11562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563

This theorem is referenced by:  prodgt0  11752  ltdiv1  11769  ltrec  11787  lediv12a  11798  expsub  13759  expdiv  13762  rlimdiv  15285  isumdivc  15404  fsumdivc  15426  trirecip  15503  geo2sum  15513  geo2lim  15515  prodfdiv  15536  ege2le3  15727  eftlub  15746  eirrlem  15841  prmreclem4  16548  m1expaddsub  19021  abvdiv  20012  cnsubrg  20570  nmdvr  23740  nmoi2  23800  cphdivcl  24251  ipcau2  24303  divcncf  24516  ovolsca  24584  dvmptdiv  25043  dvsincos  25050  plyeq0lem  25276  plydivlem4  25361  aalioulem4  25400  geolim3  25404  aaliou3lem8  25410  taylthlem2  25438  advlogexp  25715  cxpsub  25742  divcxp  25747  dvcxp1  25798  dvcncxp1  25801  relogbdiv  25834  lawcoslem1  25870  dvatan  25990  leibpi  25997  log2tlbnd  26000  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  basellem8  26142  chebbnd1  26525  rplogsumlem2  26538  rpvmasumlem  26540  dchrmusumlema  26546  dchrisum0lema  26567  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrmusumlem  26575  mulogsumlem  26584  mulogsum  26585  logdivsum  26586  mulog2sumlem1  26587  vmalogdivsum2  26591  2vmadivsumlem  26593  log2sumbnd  26597  logdivbnd  26609  selberg4lem1  26613  selberg34r  26624  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem6  26636  pntpbnd2  26640  smcnlem  28960  ipasslem5  29098  omssubadd  32167  logdivsqrle  32530  knoppndvlem14  34632  dvtan  35754  areacirclem1  35792  areacirclem4  35795  lcmineqlem5  39969  lcmineqlem16  39980  dvrelogpow2b  40004  irrapxlem5  40564  pell14qrdivcl  40603  hashnzfzclim  41829  binomcxplemnotnn0  41863  ltdiv23neg  42824  climdivf  43043  divlimc  43087  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  stoweidlem36  43467  wallispi  43501  stirlinglem7  43511  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem39  43577  fourierdlem40  43578  fourierdlem56  43593  fourierdlem62  43599  fourierdlem78  43615  fourierdlem83  43620  fourierdlem95  43632  smfdiv  44218  dignn0flhalflem1  45849  amgmlemALT  46393  young2d  46395