Theorem divcld 12133

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  (class class class)co 7451  ℂcc 11237  0cc0 11239   / cdiv 12013

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014

This theorem is used by:  dmdcan2d  12163  mulsubdivbinom2  14447  hashf1  14643  abs1m  15546  abslem2  15551  sqreulem  15571  sqreu  15572  o1fsum  16024  divrcnv  16065  divcnv  16066  geolim  16083  geolim2  16084  geo2sum  16086  geo2lim  16088  fproddiv  16172  bpolycl  16262  bpolysum  16263  bpolydiflem  16264  bpoly4  16269  eftcl  16283  efaddlem  16303  tancl  16341  tanval2  16345  qredeq  16876  pcaddlem  17110  pjthlem1  25813  iblss  26180  itgeqa  26189  iblconst  26193  iblabsr  26205  iblmulc2  26206  itgsplit  26211  dvlem  26271  dvmulbr  26314  dvcobr  26321  dvrec  26330  dvrecg  26348  dvmptdiv  26349  dvcnvlem  26351  dveflem  26354  dvsincos  26356  dvlip  26368  c1liplem1  26371  lhop1lem  26388  lhop1  26389  lhop2  26390  lhop  26391  ftc1lem4  26414  vieta1lem2  26689  vieta1  26690  elqaalem3  26701  aareccl  26710  aalioulem1  26716  taylfvallem1  26741  tayl0  26746  taylply2  26752  taylply  26753  dvtaylp  26754  taylthlem2  26758  ulmdvlem1  26784  tanregt0  26924  eff1olem  26933  argregt0  26995  argrege0  26996  argimgt0  26997  logcnlem4  27030  advlogexp  27040  logtaylsum  27046  logtayl2  27047  root1eq1  27140  logbcl  27152  cxplogb  27171  logbf  27174  angcld  27190  angrteqvd  27191  cosangneg2d  27192  angrtmuld  27193  ang180lem1  27194  ang180lem2  27195  ang180lem3  27196  ang180lem4  27197  ang180lem5  27198  lawcoslem1  27200  lawcos  27201  isosctrlem2  27204  isosctrlem3  27205  angpieqvdlem  27213  angpieqvdlem2  27214  angpieqvd  27216  dcubic1lem  27228  dcubic2  27229  dcubic1  27230  dcubic  27231  mcubic  27232  cubic2  27233  dquartlem1  27236  dquartlem2  27237  dquart  27238  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem3  27244  quartlem4  27245  quart  27246  tanatan  27304  atantayl  27322  atantayl2  27323  atantayl3  27324  log2cnv  27329  birthdaylem2  27337  efrlim  27354  dfef2  27355  cxploglim2  27363  fsumharmonic  27396  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem4  27416  lgamgulmlem5  27417  lgamgulmlem6  27418  lgamgulm2  27420  lgamcvg2  27439  gamcvg  27440  gamcvg2lem  27443  ftalem4  27460  ftalem5  27461  basellem8  27472  logexprlim  27609  bposlem9  27676  2lgslem3d  27783  2sqlem3  27804  dchrmusum2  27878  dchrvmasum2lem  27880  dchrvmasumiflem1  27885  dchrvmasumiflem2  27886  dchrvmaeq0  27888  dchrisum0re  27897  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  dchrisum0lem3  27903  dchrisum0  27904  mudivsum  27914  vmalogdivsum2  27922  vmalogdivsum  27923  2vmadivsumlem  27924  selberg2  27935  selberg3lem1  27941  selberg3  27943  selberg4lem1  27944  selbergr  27952  selberg3r  27953  selberg4r  27954  selberg34r  27955  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  colinearalg  29545  axcontlem8  29606  nrt2irr  31131  pjhthlem1  32050  eigvalcl  32620  riesz3i  32721  quad3d  33437  bcm1n  33483  divnumden2  33503  zringfrac  34189  constrrtlc1  34475  constrrtcclem  34477  constrfin  34489  constrdircl  34508  constrreinvcl  34515  constrsqrtcl  34522  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cos9thpinconstr  34534  oddpwdc  35097  signsplypnf  35290  signsply0  35291  itgexpif  35346  hgt750leme  35398  subfacval2  36160  divcnvlin  36713  bcprod  36718  iprodgam  36722  unbdqndv2lem1  37590  knoppndvlem2  37594  knoppndvlem7  37599  knoppndvlem9  37601  knoppndvlem10  37602  knoppndvlem16  37608  knoppndvlem17  37609  itg2addnclem  38857  iblmulc2nc  38871  ftc1cnnclem  38877  areacirclem1  38894  areacirclem4  38897  areacirc  38899  cntotbnd  38996  recbothd  43308  lcmineqlem12  43356  lcmineqlem18  43362  dvrelogpow2b  43384  aks4d1p1p2  43386  aks4d1p1p7  43390  aks6d1c2p2  43435  aks6d1c4  43440  2ap1caineq  43461  aks6d1c7lem1  43496  quadfac  43521  pellexlem2  44103  pellexlem6  44107  jm2.19  44266  jm2.27c  44280  proot1ex  44459  cvgdvgrat  45558  radcnvrat  45559  hashnzfzclim  45567  bcccl  45584  bccm1k  45587  binomcxplemrat  45595  binomcxplemfrat  45596  binomcxplemnotnn0  45601  xralrple2  46639  mccllem  46882  clim1fr1  46886  0ellimcdiv  46932  coseq0  47147  fperdvper  47202  dvdivbd  47206  dvnmptdivc  47221  dvnxpaek  47225  dvnprodlem2  47230  iblsplit  47249  itgcoscmulx  47252  itgsincmulx  47257  stoweidlem11  47294  stoweidlem26  47309  stoweidlem42  47325  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  wallispi2  47356  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem5  47361  stirlinglem6  47362  stirlinglem7  47363  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  dirkeritg  47385  dirkercncflem1  47386  dirkercncflem2  47387  fourierdlem26  47416  fourierdlem39  47429  fourierdlem56  47445  fourierdlem62  47451  fourierdlem72  47461  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem80  47469  fourierdlem103  47492  fourierdlem104  47493  fouriersw  47514  elaa2lem  47516  etransclem15  47532  etransclem20  47537  etransclem21  47538  etransclem22  47539  etransclem23  47540  etransclem24  47541  etransclem25  47542  etransclem31  47548  etransclem32  47549  etransclem33  47550  etransclem34  47551  etransclem35  47552  etransclem47  47564  etransclem48  47565  hoiqssbllem2  47906  sigardiv  48144  sharhght  48148  cndivrenred  48649  fmtnoprmfac2lem1  48924  quad1  48991  requad01  48992  requad1  48993  brucn  49746  bruval2  49747  bruval3  49748  fdivmptf  49984  affinecomb2  50146  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  itscnhlc0xyqsol  50208  itschlc0xyqsol1  50209  sinhf  51239  tanhf  51249  coshadd  51255  cotcl  51273  dvsec  51284  dvcsc  51285  dvcot  51286