Theorem divcld 12002

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  (class class class)co 7416  ℂcc 11109  0cc0 11111   / cdiv 11882

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-div 11883

This theorem is used by:  dmdcan2d  12032  mulsubdivbinom2  14312  hashf1  14508  abs1m  15407  abslem2  15411  sqreulem  15431  sqreu  15432  o1fsum  15884  divrcnv  15925  divcnv  15926  geolim  15943  geolim2  15944  geo2sum  15946  geo2lim  15948  fproddiv  16034  bpolycl  16124  bpolysum  16125  bpolydiflem  16126  bpoly4  16131  eftcl  16145  efaddlem  16165  tancl  16203  tanval2  16207  qredeq  16733  pcaddlem  16966  pjthlem1  25627  iblss  25995  itgeqa  26004  iblconst  26008  iblabsr  26020  iblmulc2  26021  itgsplit  26026  dvlem  26086  dvmulbr  26129  dvcobr  26136  dvrec  26145  dvrecg  26163  dvmptdiv  26164  dvcnvlem  26166  dveflem  26169  dvsincos  26171  dvlip  26183  c1liplem1  26186  lhop1lem  26203  lhop1  26204  lhop2  26205  lhop  26206  ftc1lem4  26229  vieta1lem2  26503  vieta1  26504  elqaalem3  26513  aareccl  26520  aalioulem1  26526  taylfvallem1  26551  tayl0  26556  taylply2  26562  taylply  26563  dvtaylp  26564  taylthlem2  26568  ulmdvlem1  26594  tanregt0  26735  eff1olem  26744  argregt0  26806  argrege0  26807  argimgt0  26808  logcnlem4  26841  advlogexp  26851  logtaylsum  26857  logtayl2  26858  root1eq1  26951  logbcl  26963  cxplogb  26982  logbf  26985  angcld  27001  angrteqvd  27002  cosangneg2d  27003  angrtmuld  27004  ang180lem1  27005  ang180lem2  27006  ang180lem3  27007  ang180lem4  27008  ang180lem5  27009  lawcoslem1  27011  lawcos  27012  isosctrlem2  27015  isosctrlem3  27016  angpieqvdlem  27024  angpieqvdlem2  27025  angpieqvd  27027  dcubic1lem  27039  dcubic2  27040  dcubic1  27041  dcubic  27042  mcubic  27043  cubic2  27044  dquartlem1  27047  dquartlem2  27048  dquart  27049  quart1cl  27050  quart1lem  27051  quart1  27052  quartlem3  27055  quartlem4  27056  quart  27057  tanatan  27115  atantayl  27133  atantayl2  27134  atantayl3  27135  log2cnv  27140  birthdaylem2  27148  efrlim  27165  dfef2  27166  cxploglim2  27174  fsumharmonic  27207  lgamgulmlem2  27225  lgamgulmlem3  27226  lgamgulmlem4  27227  lgamgulmlem5  27228  lgamgulmlem6  27229  lgamgulm2  27231  lgamcvg2  27250  gamcvg  27251  gamcvg2lem  27254  ftalem4  27271  ftalem5  27272  basellem8  27283  logexprlim  27420  bposlem9  27487  2lgslem3d  27594  2sqlem3  27615  dchrmusum2  27689  dchrvmasum2lem  27691  dchrvmasumiflem1  27696  dchrvmasumiflem2  27697  dchrvmaeq0  27699  dchrisum0re  27708  dchrisum0lem1b  27710  dchrisum0lem1  27711  dchrisum0lem2a  27712  dchrisum0lem2  27713  dchrisum0lem3  27714  dchrisum0  27715  mudivsum  27725  vmalogdivsum2  27733  vmalogdivsum  27734  2vmadivsumlem  27735  selberg2  27746  selberg3lem1  27752  selberg3  27754  selberg4lem1  27755  selbergr  27763  selberg3r  27764  selberg4r  27765  selberg34r  27766  pntrlog2bndlem1  27772  pntrlog2bndlem2  27773  pntrlog2bndlem3  27774  pntrlog2bndlem4  27775  pntrlog2bndlem5  27776  colinearalg  29291  axcontlem8  29352  nrt2irr  30871  pjhthlem1  31790  eigvalcl  32360  riesz3i  32461  quad3d  33140  bcm1n  33186  divnumden2  33206  zringfrac  33884  constrrtlc1  34162  constrrtcclem  34164  constrfin  34176  constrdircl  34195  constrreinvcl  34202  constrsqrtcl  34209  cos9thpiminplylem2  34213  cos9thpiminplylem3  34214  cos9thpiminply  34218  cos9thpinconstrlem1  34219  cos9thpinconstrlem2  34220  cos9thpinconstr  34221  oddpwdc  34785  signsplypnf  34978  signsply0  34979  itgexpif  35034  hgt750leme  35086  subfacval2  35692  divcnvlin  36238  bcprod  36243  iprodgam  36247  unbdqndv2lem1  37131  knoppndvlem2  37135  knoppndvlem7  37140  knoppndvlem9  37142  knoppndvlem10  37143  knoppndvlem16  37149  knoppndvlem17  37150  itg2addnclem  38355  iblmulc2nc  38369  ftc1cnnclem  38375  areacirclem1  38392  areacirclem4  38395  areacirc  38397  cntotbnd  38480  recbothd  42792  lcmineqlem12  42840  lcmineqlem18  42846  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1p7  42874  aks6d1c2p2  42919  aks6d1c4  42924  2ap1caineq  42945  aks6d1c7lem1  42980  quadfac  43005  pellexlem2  43590  pellexlem6  43594  jm2.19  43753  jm2.27c  43767  proot1ex  43956  cvgdvgrat  45056  radcnvrat  45057  hashnzfzclim  45065  bcccl  45082  bccm1k  45085  binomcxplemrat  45093  binomcxplemfrat  45094  binomcxplemnotnn0  45099  xralrple2  46103  mccllem  46346  clim1fr1  46350  0ellimcdiv  46396  coseq0  46611  fperdvper  46666  dvdivbd  46670  dvnmptdivc  46685  dvnxpaek  46689  dvnprodlem2  46694  iblsplit  46713  itgcoscmulx  46716  itgsincmulx  46721  stoweidlem11  46758  stoweidlem26  46773  stoweidlem42  46789  wallispilem4  46815  wallispilem5  46816  wallispi  46817  wallispi2lem1  46818  wallispi2lem2  46819  wallispi2  46820  stirlinglem1  46821  stirlinglem3  46823  stirlinglem4  46824  stirlinglem5  46825  stirlinglem6  46826  stirlinglem7  46827  stirlinglem13  46833  stirlinglem14  46834  stirlinglem15  46835  dirkeritg  46849  dirkercncflem1  46850  dirkercncflem2  46851  fourierdlem26  46880  fourierdlem39  46893  fourierdlem56  46909  fourierdlem62  46915  fourierdlem72  46925  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem80  46933  fourierdlem103  46956  fourierdlem104  46957  fouriersw  46978  elaa2lem  46980  etransclem15  46996  etransclem20  47001  etransclem21  47002  etransclem22  47003  etransclem23  47004  etransclem24  47005  etransclem25  47006  etransclem31  47012  etransclem32  47013  etransclem33  47014  etransclem34  47015  etransclem35  47016  etransclem47  47028  etransclem48  47029  hoiqssbllem2  47370  sigardiv  47608  sharhght  47612  cndivrenred  48076  fmtnoprmfac2lem1  48351  quad1  48418  requad01  48419  requad1  48420  fdivmptf  49354  affinecomb2  49516  eenglngeehlnmlem1  49550  eenglngeehlnmlem2  49551  itscnhlc0xyqsol  49578  itschlc0xyqsol1  49579  cotcl  50563