Theorem divcld 11996

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

Syntax hints:   → wi 4   ∈ wcel 2104   ≠ wne 2938  (class class class)co 7413  ℂcc 11112  0cc0 11114   / cdiv 11877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-div 11878

This theorem is referenced by:  dmdcan2d  12026  mulsubdivbinom2  14228  hashf1  14424  abs1m  15288  abslem2  15292  sqreulem  15312  sqreu  15313  o1fsum  15765  divrcnv  15804  divcnv  15805  geolim  15822  geolim2  15823  geo2sum  15825  geo2lim  15827  fproddiv  15911  bpolycl  16002  bpolysum  16003  bpolydiflem  16004  bpoly4  16009  eftcl  16023  efaddlem  16042  tancl  16078  tanval2  16082  qredeq  16600  pcaddlem  16827  pjthlem1  25187  iblss  25556  itgeqa  25565  iblconst  25569  iblabsr  25581  iblmulc2  25582  itgsplit  25587  dvlem  25647  dvmulbr  25690  dvcobr  25697  dvrec  25706  dvrecg  25724  dvmptdiv  25725  dvcnvlem  25727  dveflem  25730  dvsincos  25732  dvlip  25744  c1liplem1  25747  lhop1lem  25764  lhop1  25765  lhop2  25766  lhop  25767  ftc1lem4  25790  vieta1lem2  26058  vieta1  26059  elqaalem3  26068  aareccl  26073  aalioulem1  26079  taylfvallem1  26103  tayl0  26108  taylply2  26114  taylply  26115  dvtaylp  26116  taylthlem2  26120  ulmdvlem1  26146  tanregt0  26282  eff1olem  26291  argregt0  26352  argrege0  26353  argimgt0  26354  logcnlem4  26387  advlogexp  26397  logtaylsum  26403  logtayl2  26404  root1eq1  26497  logbcl  26506  cxplogb  26525  logbf  26528  angcld  26544  angrteqvd  26545  cosangneg2d  26546  angrtmuld  26547  ang180lem1  26548  ang180lem2  26549  ang180lem3  26550  ang180lem4  26551  ang180lem5  26552  lawcoslem1  26554  lawcos  26555  isosctrlem2  26558  isosctrlem3  26559  angpieqvdlem  26567  angpieqvdlem2  26568  angpieqvd  26570  dcubic1lem  26582  dcubic2  26583  dcubic1  26584  dcubic  26585  mcubic  26586  cubic2  26587  dquartlem1  26590  dquartlem2  26591  dquart  26592  quart1cl  26593  quart1lem  26594  quart1  26595  quartlem3  26598  quartlem4  26599  quart  26600  tanatan  26658  atantayl  26676  atantayl2  26677  atantayl3  26678  log2cnv  26683  birthdaylem2  26691  efrlim  26708  dfef2  26709  cxploglim2  26717  fsumharmonic  26750  lgamgulmlem2  26768  lgamgulmlem3  26769  lgamgulmlem4  26770  lgamgulmlem5  26771  lgamgulmlem6  26772  lgamgulm2  26774  lgamcvg2  26793  gamcvg  26794  gamcvg2lem  26797  ftalem4  26814  ftalem5  26815  basellem8  26826  logexprlim  26962  bposlem9  27029  2lgslem3d  27136  2sqlem3  27157  dchrmusum2  27231  dchrvmasum2lem  27233  dchrvmasumiflem1  27238  dchrvmasumiflem2  27239  dchrvmaeq0  27241  dchrisum0re  27250  dchrisum0lem1b  27252  dchrisum0lem1  27253  dchrisum0lem2a  27254  dchrisum0lem2  27255  dchrisum0lem3  27256  dchrisum0  27257  mudivsum  27267  vmalogdivsum2  27275  vmalogdivsum  27276  2vmadivsumlem  27277  selberg2  27288  selberg3lem1  27294  selberg3  27296  selberg4lem1  27297  selbergr  27305  selberg3r  27306  selberg4r  27307  selberg34r  27308  pntrlog2bndlem1  27314  pntrlog2bndlem2  27315  pntrlog2bndlem3  27316  pntrlog2bndlem4  27317  pntrlog2bndlem5  27318  colinearalg  28433  axcontlem8  28494  nrt2irr  29991  pjhthlem1  30909  eigvalcl  31479  riesz3i  31580  bcm1n  32271  divnumden2  32289  oddpwdc  33649  signsplypnf  33857  signsply0  33858  itgexpif  33914  hgt750leme  33966  subfacval2  34474  divcnvlin  35004  bcprod  35010  iprodgam  35014  gg-dvmulbr  35463  gg-dvcobr  35464  unbdqndv2lem1  35690  knoppndvlem2  35694  knoppndvlem7  35699  knoppndvlem9  35701  knoppndvlem10  35702  knoppndvlem16  35708  knoppndvlem17  35709  itg2addnclem  36844  iblmulc2nc  36858  ftc1cnnclem  36864  areacirclem1  36881  areacirclem4  36884  areacirc  36886  cntotbnd  36969  recbothd  41166  lcmineqlem12  41213  lcmineqlem18  41219  dvrelogpow2b  41241  aks4d1p1p2  41243  aks4d1p1p7  41247  aks6d1c2p2  41265  2ap1caineq  41269  pellexlem2  41872  pellexlem6  41876  jm2.19  42036  jm2.27c  42050  proot1ex  42247  cvgdvgrat  43376  radcnvrat  43377  hashnzfzclim  43385  bcccl  43402  bccm1k  43405  binomcxplemrat  43413  binomcxplemfrat  43414  binomcxplemnotnn0  43419  xralrple2  44364  mccllem  44613  clim1fr1  44617  0ellimcdiv  44665  coseq0  44880  fperdvper  44935  dvdivbd  44939  dvnmptdivc  44954  dvnxpaek  44958  dvnprodlem2  44963  iblsplit  44982  itgcoscmulx  44985  itgsincmulx  44990  stoweidlem11  45027  stoweidlem26  45042  stoweidlem42  45058  wallispilem4  45084  wallispilem5  45085  wallispi  45086  wallispi2lem1  45087  wallispi2lem2  45088  wallispi2  45089  stirlinglem1  45090  stirlinglem3  45092  stirlinglem4  45093  stirlinglem5  45094  stirlinglem6  45095  stirlinglem7  45096  stirlinglem13  45102  stirlinglem14  45103  stirlinglem15  45104  dirkeritg  45118  dirkercncflem1  45119  dirkercncflem2  45120  fourierdlem26  45149  fourierdlem39  45162  fourierdlem56  45178  fourierdlem62  45184  fourierdlem72  45194  fourierdlem74  45196  fourierdlem75  45197  fourierdlem76  45198  fourierdlem80  45202  fourierdlem103  45225  fourierdlem104  45226  fouriersw  45247  elaa2lem  45249  etransclem15  45265  etransclem20  45270  etransclem21  45271  etransclem22  45272  etransclem23  45273  etransclem24  45274  etransclem25  45275  etransclem31  45281  etransclem32  45282  etransclem33  45283  etransclem34  45284  etransclem35  45285  etransclem47  45297  etransclem48  45298  hoiqssbllem2  45639  sigardiv  45877  sharhght  45881  cndivrenred  46314  fmtnoprmfac2lem1  46534  quad1  46588  requad01  46589  requad1  46590  fdivmptf  47316  affinecomb2  47478  eenglngeehlnmlem1  47512  eenglngeehlnmlem2  47513  itscnhlc0xyqsol  47540  itschlc0xyqsol1  47541  cotcl  47886