MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divcld Structured version   Unicode version

Theorem divcld 10382
Description: Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
div1d.1  |-  ( ph  ->  A  e.  CC )
divcld.2  |-  ( ph  ->  B  e.  CC )
divcld.3  |-  ( ph  ->  B  =/=  0 )
Assertion
Ref Expression
divcld  |-  ( ph  ->  ( A  /  B
)  e.  CC )

Proof of Theorem divcld
StepHypRef Expression
1 div1d.1 . 2  |-  ( ph  ->  A  e.  CC )
2 divcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 divcld.3 . 2  |-  ( ph  ->  B  =/=  0 )
4 divcl 10275 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B  =/=  0 )  ->  ( A  /  B )  e.  CC )
51, 2, 3, 4syl3anc 1264 1  |-  ( ph  ->  ( A  /  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    =/= wne 2625  (class class class)co 6305   CCcc 9536   0cc0 9538    / cdiv 10268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-po 4775  df-so 4776  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269
This theorem is referenced by:  dmdcan2d  10412  hashf1  12615  abs1m  13377  abslem2  13381  sqreulem  13401  sqreu  13402  o1fsum  13851  divrcnv  13888  divcnv  13889  geolim  13904  geolim2  13905  geo2sum  13907  geo2lim  13909  fproddiv  13993  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  bpoly4  14090  eftcl  14106  efaddlem  14125  tancl  14161  tanval2  14165  qredeq  14634  pcaddlem  14796  pjthlem1  22272  iblss  22639  itgeqa  22648  iblconst  22652  iblabsr  22664  iblmulc2  22665  itgsplit  22670  dvlem  22728  dvmulbr  22770  dvcobr  22777  dvrec  22786  dvcnvlem  22805  dveflem  22808  dvsincos  22810  dvlip  22822  c1liplem1  22825  lhop1lem  22842  lhop1  22843  lhop2  22844  lhop  22845  ftc1lem4  22868  vieta1lem2  23132  vieta1  23133  elqaalem3  23142  aareccl  23147  aalioulem1  23153  taylfvallem1  23177  tayl0  23182  taylply2  23188  taylply  23189  dvtaylp  23190  taylthlem2  23194  ulmdvlem1  23220  tanregt0  23353  eff1olem  23362  argregt0  23424  argrege0  23425  argimgt0  23426  logcnlem4  23455  advlogexp  23465  logtaylsum  23471  logtayl2  23472  root1eq1  23560  logbcl  23569  cxplogb  23588  logbf  23591  angcld  23599  angrteqvd  23600  cosangneg2d  23601  angrtmuld  23602  ang180lem1  23603  ang180lem2  23604  ang180lem3  23605  ang180lem4  23606  ang180lem5  23607  lawcoslem1  23609  lawcos  23610  isosctrlem2  23613  isosctrlem3  23614  angpieqvdlem  23619  angpieqvdlem2  23620  angpieqvd  23622  dcubic1lem  23634  dcubic2  23635  dcubic1  23636  dcubic  23637  mcubic  23638  cubic2  23639  dquartlem1  23642  dquartlem2  23643  dquart  23644  quart1cl  23645  quart1lem  23646  quart1  23647  quartlem3  23650  quartlem4  23651  quart  23652  tanatan  23710  atantayl  23728  atantayl2  23729  atantayl3  23730  log2cnv  23735  birthdaylem2  23743  efrlim  23760  dfef2  23761  cxploglim2  23769  fsumharmonic  23802  lgamgulmlem2  23820  lgamgulmlem3  23821  lgamgulmlem4  23822  lgamgulmlem5  23823  lgamgulmlem6  23824  lgamgulm2  23826  lgamcvg2  23845  gamcvg  23846  gamcvg2lem  23849  ftalem4  23865  ftalem5  23866  basellem8  23877  logexprlim  24016  bposlem9  24083  2sqlem3  24157  dchrmusum2  24195  dchrvmasum2lem  24197  dchrvmasumiflem1  24202  dchrvmasumiflem2  24203  dchrvmaeq0  24205  dchrisum0re  24214  dchrisum0lem1b  24216  dchrisum0lem1  24217  dchrisum0lem2a  24218  dchrisum0lem2  24219  dchrisum0lem3  24220  dchrisum0  24221  mudivsum  24231  vmalogdivsum2  24239  vmalogdivsum  24240  2vmadivsumlem  24241  selberg2  24252  selberg3lem1  24258  selberg3  24260  selberg4lem1  24261  selbergr  24269  selberg3r  24270  selberg4r  24271  selberg34r  24272  pntrlog2bndlem1  24278  pntrlog2bndlem2  24279  pntrlog2bndlem3  24280  pntrlog2bndlem4  24281  pntrlog2bndlem5  24282  colinearalg  24786  axcontlem8  24847  pjhthlem1  26879  eigvalcl  27449  riesz3i  27550  bcm1n  28207  divnumden2  28219  oddpwdc  29013  signsplypnf  29227  signsply0  29228  subfacval2  29698  divcnvlin  30154  bcprod  30161  iprodgam  30165  itg2addnclem  31696  iblmulc2nc  31710  ftc1cnnclem  31718  areacirclem1  31735  areacirclem4  31738  areacirc  31740  cntotbnd  31831  pellexlem2  35383  pellexlem6  35387  jm2.19  35553  jm2.27c  35567  proot1ex  35776  cvgdvgrat  36298  radcnvrat  36299  hashnzfzclim  36307  bcccl  36324  bccm1k  36327  binomcxplemrat  36335  binomcxplemfrat  36336  binomcxplemnotnn0  36341  mccllem  37248  clim1fr1  37250  0ellimcdiv  37301  coseq0  37310  dvrecg  37353  dvmptdiv  37360  fperdvper  37361  dvdivbd  37366  dvnmptdivc  37381  dvnxpaek  37385  dvnprodlem2  37390  iblsplit  37411  itgcoscmulx  37414  itgsincmulx  37419  stoweidlem11  37439  stoweidlem26  37454  stoweidlem42  37471  wallispilem4  37498  wallispilem5  37499  wallispi  37500  wallispi2lem1  37501  wallispi2lem2  37502  wallispi2  37503  stirlinglem1  37504  stirlinglem3  37506  stirlinglem4  37507  stirlinglem5  37508  stirlinglem6  37509  stirlinglem7  37510  stirlinglem13  37516  stirlinglem14  37517  stirlinglem15  37518  dirkeritg  37532  dirkercncflem1  37533  dirkercncflem2  37534  fourierdlem26  37563  fourierdlem39  37576  fourierdlem56  37593  fourierdlem62  37599  fourierdlem72  37609  fourierdlem74  37611  fourierdlem75  37612  fourierdlem76  37613  fourierdlem80  37617  fourierdlem103  37640  fourierdlem104  37641  fouriersw  37662  elaa2lem  37664  etransclem15  37680  etransclem20  37685  etransclem21  37686  etransclem22  37687  etransclem23  37688  etransclem24  37689  etransclem25  37690  etransclem31  37696  etransclem32  37697  etransclem33  37698  etransclem34  37699  etransclem35  37700  etransclem47  37712  etransclem48  37713  sigardiv  37869  sharhght  37873  fdivmptf  39112  cotcl  39232
  Copyright terms: Public domain W3C validator