Theorem divcld 11892

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  (class class class)co 7341  ℂcc 10999  0cc0 11001   / cdiv 11769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-div 11770

This theorem is referenced by:  dmdcan2d  11922  mulsubdivbinom2  14164  hashf1  14359  abs1m  15238  abslem2  15242  sqreulem  15262  sqreu  15263  o1fsum  15715  divrcnv  15754  divcnv  15755  geolim  15772  geolim2  15773  geo2sum  15775  geo2lim  15777  fproddiv  15863  bpolycl  15954  bpolysum  15955  bpolydiflem  15956  bpoly4  15961  eftcl  15975  efaddlem  15995  tancl  16033  tanval2  16037  qredeq  16563  pcaddlem  16795  pjthlem1  25359  iblss  25728  itgeqa  25737  iblconst  25741  iblabsr  25753  iblmulc2  25754  itgsplit  25759  dvlem  25819  dvmulbr  25863  dvmulbrOLD  25864  dvcobr  25871  dvcobrOLD  25872  dvrec  25881  dvrecg  25899  dvmptdiv  25900  dvcnvlem  25902  dveflem  25905  dvsincos  25907  dvlip  25920  c1liplem1  25923  lhop1lem  25940  lhop1  25941  lhop2  25942  lhop  25943  ftc1lem4  25968  vieta1lem2  26241  vieta1  26242  elqaalem3  26251  aareccl  26256  aalioulem1  26262  taylfvallem1  26286  tayl0  26291  taylply2  26297  taylply2OLD  26298  taylply  26299  dvtaylp  26300  taylthlem2  26304  taylthlem2OLD  26305  ulmdvlem1  26331  tanregt0  26470  eff1olem  26479  argregt0  26541  argrege0  26542  argimgt0  26543  logcnlem4  26576  advlogexp  26586  logtaylsum  26592  logtayl2  26593  root1eq1  26687  logbcl  26699  cxplogb  26718  logbf  26721  angcld  26737  angrteqvd  26738  cosangneg2d  26739  angrtmuld  26740  ang180lem1  26741  ang180lem2  26742  ang180lem3  26743  ang180lem4  26744  ang180lem5  26745  lawcoslem1  26747  lawcos  26748  isosctrlem2  26751  isosctrlem3  26752  angpieqvdlem  26760  angpieqvdlem2  26761  angpieqvd  26763  dcubic1lem  26775  dcubic2  26776  dcubic1  26777  dcubic  26778  mcubic  26779  cubic2  26780  dquartlem1  26783  dquartlem2  26784  dquart  26785  quart1cl  26786  quart1lem  26787  quart1  26788  quartlem3  26791  quartlem4  26792  quart  26793  tanatan  26851  atantayl  26869  atantayl2  26870  atantayl3  26871  log2cnv  26876  birthdaylem2  26884  efrlim  26901  efrlimOLD  26902  dfef2  26903  cxploglim2  26911  fsumharmonic  26944  lgamgulmlem2  26962  lgamgulmlem3  26963  lgamgulmlem4  26964  lgamgulmlem5  26965  lgamgulmlem6  26966  lgamgulm2  26968  lgamcvg2  26987  gamcvg  26988  gamcvg2lem  26991  ftalem4  27008  ftalem5  27009  basellem8  27020  logexprlim  27158  bposlem9  27225  2lgslem3d  27332  2sqlem3  27353  dchrmusum2  27427  dchrvmasum2lem  27429  dchrvmasumiflem1  27434  dchrvmasumiflem2  27435  dchrvmaeq0  27437  dchrisum0re  27446  dchrisum0lem1b  27448  dchrisum0lem1  27449  dchrisum0lem2a  27450  dchrisum0lem2  27451  dchrisum0lem3  27452  dchrisum0  27453  mudivsum  27463  vmalogdivsum2  27471  vmalogdivsum  27472  2vmadivsumlem  27473  selberg2  27484  selberg3lem1  27490  selberg3  27492  selberg4lem1  27493  selbergr  27501  selberg3r  27502  selberg4r  27503  selberg34r  27504  pntrlog2bndlem1  27510  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  colinearalg  28883  axcontlem8  28944  nrt2irr  30445  pjhthlem1  31363  eigvalcl  31933  riesz3i  32034  quad3d  32725  bcm1n  32769  divnumden2  32790  zringfrac  33511  constrrtlc1  33737  constrrtcclem  33739  constrfin  33751  constrdircl  33770  constrreinvcl  33777  constrsqrtcl  33784  cos9thpiminplylem2  33788  cos9thpiminplylem3  33789  cos9thpiminply  33793  cos9thpinconstrlem1  33794  cos9thpinconstrlem2  33795  cos9thpinconstr  33796  oddpwdc  34359  signsplypnf  34555  signsply0  34556  itgexpif  34611  hgt750leme  34663  subfacval2  35223  divcnvlin  35769  bcprod  35774  iprodgam  35778  unbdqndv2lem1  36543  knoppndvlem2  36547  knoppndvlem7  36552  knoppndvlem9  36554  knoppndvlem10  36555  knoppndvlem16  36561  knoppndvlem17  36562  itg2addnclem  37711  iblmulc2nc  37725  ftc1cnnclem  37731  areacirclem1  37748  areacirclem4  37751  areacirc  37753  cntotbnd  37836  recbothd  42025  lcmineqlem12  42073  lcmineqlem18  42079  dvrelogpow2b  42101  aks4d1p1p2  42103  aks4d1p1p7  42107  aks6d1c2p2  42152  aks6d1c4  42157  2ap1caineq  42178  aks6d1c7lem1  42213  pellexlem2  42863  pellexlem6  42867  jm2.19  43026  jm2.27c  43040  proot1ex  43229  cvgdvgrat  44346  radcnvrat  44347  hashnzfzclim  44355  bcccl  44372  bccm1k  44375  binomcxplemrat  44383  binomcxplemfrat  44384  binomcxplemnotnn0  44389  xralrple2  45393  mccllem  45637  clim1fr1  45641  0ellimcdiv  45687  coseq0  45902  fperdvper  45957  dvdivbd  45961  dvnmptdivc  45976  dvnxpaek  45980  dvnprodlem2  45985  iblsplit  46004  itgcoscmulx  46007  itgsincmulx  46012  stoweidlem11  46049  stoweidlem26  46064  stoweidlem42  46080  wallispilem4  46106  wallispilem5  46107  wallispi  46108  wallispi2lem1  46109  wallispi2lem2  46110  wallispi2  46111  stirlinglem1  46112  stirlinglem3  46114  stirlinglem4  46115  stirlinglem5  46116  stirlinglem6  46117  stirlinglem7  46118  stirlinglem13  46124  stirlinglem14  46125  stirlinglem15  46126  dirkeritg  46140  dirkercncflem1  46141  dirkercncflem2  46142  fourierdlem26  46171  fourierdlem39  46184  fourierdlem56  46200  fourierdlem62  46206  fourierdlem72  46216  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem80  46224  fourierdlem103  46247  fourierdlem104  46248  fouriersw  46269  elaa2lem  46271  etransclem15  46287  etransclem20  46292  etransclem21  46293  etransclem22  46294  etransclem23  46295  etransclem24  46296  etransclem25  46297  etransclem31  46303  etransclem32  46304  etransclem33  46305  etransclem34  46306  etransclem35  46307  etransclem47  46319  etransclem48  46320  hoiqssbllem2  46661  sigardiv  46899  sharhght  46903  cndivrenred  47337  fmtnoprmfac2lem1  47597  quad1  47651  requad01  47652  requad1  47653  fdivmptf  48573  affinecomb2  48735  eenglngeehlnmlem1  48769  eenglngeehlnmlem2  48770  itscnhlc0xyqsol  48797  itschlc0xyqsol1  48798  cotcl  49784