Theorem divcld 11986

Description: Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
divcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
divcld.3	⊢ (𝜑 → 𝐵 ≠ 0)

Assertion

Ref	Expression
divcld	⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Proof of Theorem divcld

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		divcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		divcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		divcl 11873	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  (class class class)co 7410  ℂcc 11093  0cc0 11095   / cdiv 11866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867

This theorem is referenced by:  dmdcan2d  12016  mulsubdivbinom2  14294  hashf1  14490  abs1m  15383  abslem2  15387  sqreulem  15407  sqreu  15408  o1fsum  15861  divrcnv  15902  divcnv  15903  geolim  15920  geolim2  15921  geo2sum  15923  geo2lim  15925  fproddiv  16011  bpolycl  16101  bpolysum  16102  bpolydiflem  16103  bpoly4  16108  eftcl  16122  efaddlem  16142  tancl  16180  tanval2  16184  qredeq  16710  pcaddlem  16943  pjthlem1  25596  iblss  25964  itgeqa  25973  iblconst  25977  iblabsr  25989  iblmulc2  25990  itgsplit  25995  dvlem  26055  dvmulbr  26098  dvcobr  26105  dvrec  26114  dvrecg  26132  dvmptdiv  26133  dvcnvlem  26135  dveflem  26138  dvsincos  26140  dvlip  26152  c1liplem1  26155  lhop1lem  26172  lhop1  26173  lhop2  26174  lhop  26175  ftc1lem4  26198  vieta1lem2  26472  vieta1  26473  elqaalem3  26482  aareccl  26489  aalioulem1  26495  taylfvallem1  26520  tayl0  26525  taylply2  26531  taylply  26532  dvtaylp  26533  taylthlem2  26537  ulmdvlem1  26563  tanregt0  26704  eff1olem  26713  argregt0  26775  argrege0  26776  argimgt0  26777  logcnlem4  26810  advlogexp  26820  logtaylsum  26826  logtayl2  26827  root1eq1  26920  logbcl  26932  cxplogb  26951  logbf  26954  angcld  26970  angrteqvd  26971  cosangneg2d  26972  angrtmuld  26973  ang180lem1  26974  ang180lem2  26975  ang180lem3  26976  ang180lem4  26977  ang180lem5  26978  lawcoslem1  26980  lawcos  26981  isosctrlem2  26984  isosctrlem3  26985  angpieqvdlem  26993  angpieqvdlem2  26994  angpieqvd  26996  dcubic1lem  27008  dcubic2  27009  dcubic1  27010  dcubic  27011  mcubic  27012  cubic2  27013  dquartlem1  27016  dquartlem2  27017  dquart  27018  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem3  27024  quartlem4  27025  quart  27026  tanatan  27084  atantayl  27102  atantayl2  27103  atantayl3  27104  log2cnv  27109  birthdaylem2  27117  efrlim  27134  dfef2  27135  cxploglim2  27143  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  ftalem4  27240  ftalem5  27241  basellem8  27252  logexprlim  27389  bposlem9  27456  2lgslem3d  27563  2sqlem3  27584  dchrmusum2  27658  dchrvmasum2lem  27660  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrvmaeq0  27668  dchrisum0re  27677  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  dchrisum0  27684  mudivsum  27694  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  selberg2  27715  selberg3lem1  27721  selberg3  27723  selberg4lem1  27724  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  colinearalg  29260  axcontlem8  29321  nrt2irr  30824  pjhthlem1  31743  eigvalcl  32313  riesz3i  32414  quad3d  33094  bcm1n  33140  divnumden2  33160  zringfrac  33844  constrrtlc1  34122  constrrtcclem  34124  constrfin  34136  constrdircl  34155  constrreinvcl  34162  constrsqrtcl  34169  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminply  34178  cos9thpinconstrlem1  34179  cos9thpinconstrlem2  34180  cos9thpinconstr  34181  oddpwdc  34744  signsplypnf  34937  signsply0  34938  itgexpif  34993  hgt750leme  35045  subfacval2  35679  divcnvlin  36225  bcprod  36230  iprodgam  36234  unbdqndv2lem1  37098  knoppndvlem2  37102  knoppndvlem7  37107  knoppndvlem9  37109  knoppndvlem10  37110  knoppndvlem16  37116  knoppndvlem17  37117  itg2addnclem  38322  iblmulc2nc  38336  ftc1cnnclem  38342  areacirclem1  38359  areacirclem4  38362  areacirc  38364  cntotbnd  38447  recbothd  42759  lcmineqlem12  42807  lcmineqlem18  42813  dvrelogpow2b  42835  aks4d1p1p2  42837  aks4d1p1p7  42841  aks6d1c2p2  42886  aks6d1c4  42891  2ap1caineq  42912  aks6d1c7lem1  42947  quadfac  42972  pellexlem2  43557  pellexlem6  43561  jm2.19  43720  jm2.27c  43734  proot1ex  43923  cvgdvgrat  45023  radcnvrat  45024  hashnzfzclim  45032  bcccl  45049  bccm1k  45052  binomcxplemrat  45060  binomcxplemfrat  45061  binomcxplemnotnn0  45066  xralrple2  46070  mccllem  46313  clim1fr1  46317  0ellimcdiv  46363  coseq0  46578  fperdvper  46633  dvdivbd  46637  dvnmptdivc  46652  dvnxpaek  46656  dvnprodlem2  46661  iblsplit  46680  itgcoscmulx  46683  itgsincmulx  46688  stoweidlem11  46725  stoweidlem26  46740  stoweidlem42  46756  wallispilem4  46782  wallispilem5  46783  wallispi  46784  wallispi2lem1  46785  wallispi2lem2  46786  wallispi2  46787  stirlinglem1  46788  stirlinglem3  46790  stirlinglem4  46791  stirlinglem5  46792  stirlinglem6  46793  stirlinglem7  46794  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  dirkeritg  46816  dirkercncflem1  46817  dirkercncflem2  46818  fourierdlem26  46847  fourierdlem39  46860  fourierdlem56  46876  fourierdlem62  46882  fourierdlem72  46892  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem80  46900  fourierdlem103  46923  fourierdlem104  46924  fouriersw  46945  elaa2lem  46947  etransclem15  46963  etransclem20  46968  etransclem21  46969  etransclem22  46970  etransclem23  46971  etransclem24  46972  etransclem25  46973  etransclem31  46979  etransclem32  46980  etransclem33  46981  etransclem34  46982  etransclem35  46983  etransclem47  46995  etransclem48  46996  hoiqssbllem2  47337  sigardiv  47575  sharhght  47579  cndivrenred  48043  fmtnoprmfac2lem1  48318  quad1  48385  requad01  48386  requad1  48387  fdivmptf  49321  affinecomb2  49483  eenglngeehlnmlem1  49517  eenglngeehlnmlem2  49518  itscnhlc0xyqsol  49545  itschlc0xyqsol1  49546  cotcl  50530