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 1542   ∈ wcel 2110   ≠ wne 2945  (class class class)co 7271  ℂcc 10870  0cc0 10872  1c1 10873   · cmul 10877   / cdiv 11632

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-div 11633

This theorem is referenced by:  prodgt0  11822  ltdiv1  11839  ltrec  11857  lediv12a  11868  expsub  13829  expdiv  13832  rlimdiv  15355  isumdivc  15474  fsumdivc  15496  trirecip  15573  geo2sum  15583  geo2lim  15585  prodfdiv  15606  ege2le3  15797  eftlub  15816  eirrlem  15911  prmreclem4  16618  m1expaddsub  19104  abvdiv  20095  cnsubrg  20656  nmdvr  23832  nmoi2  23892  cphdivcl  24344  ipcau2  24396  divcncf  24609  ovolsca  24677  dvmptdiv  25136  dvsincos  25143  plyeq0lem  25369  plydivlem4  25454  aalioulem4  25493  geolim3  25497  aaliou3lem8  25503  taylthlem2  25531  advlogexp  25808  cxpsub  25835  divcxp  25840  dvcxp1  25891  dvcncxp1  25894  relogbdiv  25927  lawcoslem1  25963  dvatan  26083  leibpi  26090  log2tlbnd  26093  fsumharmonic  26159  lgamgulmlem2  26177  lgamgulmlem3  26178  lgamgulmlem4  26179  basellem8  26235  chebbnd1  26618  rplogsumlem2  26631  rpvmasumlem  26633  dchrmusumlema  26639  dchrisum0lema  26660  dchrisum0lem1  26662  dchrisum0lem2a  26663  dchrisum0lem2  26664  dchrmusumlem  26668  mulogsumlem  26677  mulogsum  26678  logdivsum  26679  mulog2sumlem1  26680  vmalogdivsum2  26684  2vmadivsumlem  26686  log2sumbnd  26690  logdivbnd  26702  selberg4lem1  26706  selberg34r  26717  pntrlog2bndlem2  26724  pntrlog2bndlem4  26726  pntrlog2bndlem6  26729  pntpbnd2  26733  smcnlem  29055  ipasslem5  29193  omssubadd  32263  logdivsqrle  32626  knoppndvlem14  34701  dvtan  35823  areacirclem1  35861  areacirclem4  35864  lcmineqlem5  40038  lcmineqlem16  40049  dvrelogpow2b  40073  irrapxlem5  40645  pell14qrdivcl  40684  hashnzfzclim  41910  binomcxplemnotnn0  41944  ltdiv23neg  42905  climdivf  43124  divlimc  43168  ioodvbdlimc1lem2  43444  ioodvbdlimc2lem  43446  dvnxpaek  43454  stoweidlem36  43548  wallispi  43582  stirlinglem7  43592  dirkercncflem2  43616  dirkercncflem4  43618  fourierdlem39  43658  fourierdlem40  43659  fourierdlem56  43674  fourierdlem62  43680  fourierdlem78  43696  fourierdlem83  43701  fourierdlem95  43713  smfdiv  44299  dignn0flhalflem1  45930  amgmlemALT  46476  young2d  46478