Theorem divcld 11760

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2944  (class class class)co 7284  ℂcc 10878  0cc0 10880   / cdiv 11641

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

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 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  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 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642

This theorem is referenced by:  dmdcan2d  11790  mulsubdivbinom2  13985  hashf1  14180  abs1m  15056  abslem2  15060  sqreulem  15080  sqreu  15081  o1fsum  15534  divrcnv  15573  divcnv  15574  geolim  15591  geolim2  15592  geo2sum  15594  geo2lim  15596  fproddiv  15680  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  bpoly4  15778  eftcl  15792  efaddlem  15811  tancl  15847  tanval2  15851  qredeq  16371  pcaddlem  16598  pjthlem1  24610  iblss  24978  itgeqa  24987  iblconst  24991  iblabsr  25003  iblmulc2  25004  itgsplit  25009  dvlem  25069  dvmulbr  25112  dvcobr  25119  dvrec  25128  dvrecg  25146  dvmptdiv  25147  dvcnvlem  25149  dveflem  25152  dvsincos  25154  dvlip  25166  c1liplem1  25169  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  ftc1lem4  25212  vieta1lem2  25480  vieta1  25481  elqaalem3  25490  aareccl  25495  aalioulem1  25501  taylfvallem1  25525  tayl0  25530  taylply2  25536  taylply  25537  dvtaylp  25538  taylthlem2  25542  ulmdvlem1  25568  tanregt0  25704  eff1olem  25713  argregt0  25774  argrege0  25775  argimgt0  25776  logcnlem4  25809  advlogexp  25819  logtaylsum  25825  logtayl2  25826  root1eq1  25917  logbcl  25926  cxplogb  25945  logbf  25948  angcld  25964  angrteqvd  25965  cosangneg2d  25966  angrtmuld  25967  ang180lem1  25968  ang180lem2  25969  ang180lem3  25970  ang180lem4  25971  ang180lem5  25972  lawcoslem1  25974  lawcos  25975  isosctrlem2  25978  isosctrlem3  25979  angpieqvdlem  25987  angpieqvdlem2  25988  angpieqvd  25990  dcubic1lem  26002  dcubic2  26003  dcubic1  26004  dcubic  26005  mcubic  26006  cubic2  26007  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem3  26018  quartlem4  26019  quart  26020  tanatan  26078  atantayl  26096  atantayl2  26097  atantayl3  26098  log2cnv  26103  birthdaylem2  26111  efrlim  26128  dfef2  26129  cxploglim2  26137  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  ftalem4  26234  ftalem5  26235  basellem8  26246  logexprlim  26382  bposlem9  26449  2lgslem3d  26556  2sqlem3  26577  dchrmusum2  26651  dchrvmasum2lem  26653  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  dchrvmaeq0  26661  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrisum0  26677  mudivsum  26687  vmalogdivsum2  26695  vmalogdivsum  26696  2vmadivsumlem  26697  selberg2  26708  selberg3lem1  26714  selberg3  26716  selberg4lem1  26717  selbergr  26725  selberg3r  26726  selberg4r  26727  selberg34r  26728  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  colinearalg  27287  axcontlem8  27348  pjhthlem1  29762  eigvalcl  30332  riesz3i  30433  bcm1n  31125  divnumden2  31141  oddpwdc  32330  signsplypnf  32538  signsply0  32539  itgexpif  32595  hgt750leme  32647  subfacval2  33158  divcnvlin  33707  bcprod  33713  iprodgam  33717  unbdqndv2lem1  34698  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem9  34709  knoppndvlem10  34710  knoppndvlem16  34716  knoppndvlem17  34717  itg2addnclem  35837  iblmulc2nc  35851  ftc1cnnclem  35857  areacirclem1  35874  areacirclem4  35877  areacirc  35879  cntotbnd  35963  recbothd  40008  lcmineqlem12  40055  lcmineqlem18  40061  dvrelogpow2b  40083  aks4d1p1p2  40085  aks4d1p1p7  40089  2ap1caineq  40108  pellexlem2  40659  pellexlem6  40663  jm2.19  40822  jm2.27c  40836  proot1ex  41033  cvgdvgrat  41938  radcnvrat  41939  hashnzfzclim  41947  bcccl  41964  bccm1k  41967  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemnotnn0  41981  xralrple2  42900  mccllem  43145  clim1fr1  43149  0ellimcdiv  43197  coseq0  43412  fperdvper  43467  dvdivbd  43471  dvnmptdivc  43486  dvnxpaek  43490  dvnprodlem2  43495  iblsplit  43514  itgcoscmulx  43517  itgsincmulx  43522  stoweidlem11  43559  stoweidlem26  43574  stoweidlem42  43590  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem2  43652  fourierdlem26  43681  fourierdlem39  43694  fourierdlem56  43710  fourierdlem62  43716  fourierdlem72  43726  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  elaa2lem  43781  etransclem15  43797  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem31  43813  etransclem32  43814  etransclem33  43815  etransclem34  43816  etransclem35  43817  etransclem47  43829  etransclem48  43830  hoiqssbllem2  44168  sigardiv  44388  sharhght  44392  cndivrenred  44809  fmtnoprmfac2lem1  45029  quad1  45083  requad01  45084  requad1  45085  fdivmptf  45898  affinecomb2  46060  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  cotcl  46465