Theorem divrecd 11754

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  (class class class)co 7275  ℂcc 10869  0cc0 10871  1c1 10872   · cmul 10876   / cdiv 11632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633

This theorem is referenced by:  prodgt0  11822  ltdiv1  11839  ltrec  11857  lediv12a  11868  expsub  13831  expdiv  13834  rlimdiv  15357  isumdivc  15476  fsumdivc  15498  trirecip  15575  geo2sum  15585  geo2lim  15587  prodfdiv  15608  ege2le3  15799  eftlub  15818  eirrlem  15913  prmreclem4  16620  m1expaddsub  19106  abvdiv  20097  cnsubrg  20658  nmdvr  23834  nmoi2  23894  cphdivcl  24346  ipcau2  24398  divcncf  24611  ovolsca  24679  dvmptdiv  25138  dvsincos  25145  plyeq0lem  25371  plydivlem4  25456  aalioulem4  25495  geolim3  25499  aaliou3lem8  25505  taylthlem2  25533  advlogexp  25810  cxpsub  25837  divcxp  25842  dvcxp1  25893  dvcncxp1  25896  relogbdiv  25929  lawcoslem1  25965  dvatan  26085  leibpi  26092  log2tlbnd  26095  fsumharmonic  26161  lgamgulmlem2  26179  lgamgulmlem3  26180  lgamgulmlem4  26181  basellem8  26237  chebbnd1  26620  rplogsumlem2  26633  rpvmasumlem  26635  dchrmusumlema  26641  dchrisum0lema  26662  dchrisum0lem1  26664  dchrisum0lem2a  26665  dchrisum0lem2  26666  dchrmusumlem  26670  mulogsumlem  26679  mulogsum  26680  logdivsum  26681  mulog2sumlem1  26682  vmalogdivsum2  26686  2vmadivsumlem  26688  log2sumbnd  26692  logdivbnd  26704  selberg4lem1  26708  selberg34r  26719  pntrlog2bndlem2  26726  pntrlog2bndlem4  26728  pntrlog2bndlem6  26731  pntpbnd2  26735  smcnlem  29059  ipasslem5  29197  omssubadd  32267  logdivsqrle  32630  knoppndvlem14  34705  dvtan  35827  areacirclem1  35865  areacirclem4  35868  lcmineqlem5  40041  lcmineqlem16  40052  dvrelogpow2b  40076  irrapxlem5  40648  pell14qrdivcl  40687  hashnzfzclim  41940  binomcxplemnotnn0  41974  ltdiv23neg  42934  climdivf  43153  divlimc  43197  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  dvnxpaek  43483  stoweidlem36  43577  wallispi  43611  stirlinglem7  43621  dirkercncflem2  43645  dirkercncflem4  43647  fourierdlem39  43687  fourierdlem40  43688  fourierdlem56  43703  fourierdlem62  43709  fourierdlem78  43725  fourierdlem83  43730  fourierdlem95  43742  smfdiv  44331  dignn0flhalflem1  45961  amgmlemALT  46507  young2d  46509