Theorem divrecd 11932

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 11823	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
5	1, 2, 3, 4	syl3anc 1379	1 ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ≠ wne 2935  (class class class)co 7363  ℂcc 11034  0cc0 11036  1c1 11037   · cmul 11041   / cdiv 11805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-div 11806

This theorem is referenced by:  prodgt0  12000  ltdiv1  12018  ltrec  12036  lediv12a  12047  expsub  14070  expdiv  14073  rlimdiv  15606  isumdivc  15724  fsumdivc  15746  trirecip  15826  geo2sum  15836  geo2lim  15838  prodfdiv  15859  ege2le3  16053  eftlub  16074  eirrlem  16169  prmreclem4  16888  m1expaddsub  19471  abvdiv  20808  cnsubrg  21409  nmdvr  24660  nmoi2  24720  cphdivcl  25174  ipcau2  25226  divcncf  25439  ovolsca  25507  dvmptdiv  25966  dvsincos  25973  plyeq0lem  26200  plydivlem4  26287  aalioulem4  26326  geolim3  26330  aaliou3lem8  26336  taylthlem2  26364  advlogexp  26644  cxpsub  26671  divcxp  26676  dvcxp1  26729  dvcncxp1  26732  relogbdiv  26768  lawcoslem1  26804  dvatan  26924  leibpi  26931  log2tlbnd  26934  fsumharmonic  27000  lgamgulmlem2  27018  lgamgulmlem3  27019  lgamgulmlem4  27020  basellem8  27076  chebbnd1  27460  rplogsumlem2  27473  rpvmasumlem  27475  dchrmusumlema  27481  dchrisum0lema  27502  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrmusumlem  27510  mulogsumlem  27519  mulogsum  27520  logdivsum  27521  mulog2sumlem1  27522  vmalogdivsum2  27526  2vmadivsumlem  27528  log2sumbnd  27532  logdivbnd  27544  selberg4lem1  27548  selberg34r  27559  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem6  27571  pntpbnd2  27575  smcnlem  30793  ipasslem5  30931  constrresqrtcl  33968  cos9thpiminplylem2  33974  omssubadd  34491  logdivsqrle  34841  knoppndvlem14  36838  dvtan  38044  areacirclem1  38082  areacirclem4  38085  lcmineqlem5  42525  lcmineqlem16  42536  dvrelogpow2b  42560  irrapxlem5  43278  pell14qrdivcl  43317  hashnzfzclim  44773  binomcxplemnotnn0  44807  ltdiv23neg  45845  climdivf  46064  divlimc  46106  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  stoweidlem36  46486  wallispi  46520  stirlinglem7  46530  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem39  46596  fourierdlem40  46597  fourierdlem56  46612  fourierdlem62  46618  fourierdlem78  46634  fourierdlem83  46639  fourierdlem95  46651  smfdiv  47247  dignn0flhalflem1  49113  amgmlemALT  50300  young2d  50302