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

Theorem divcld 11404
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
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 divcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 divcld.3 . 2 (𝜑𝐵 ≠ 0)
4 divcl 11292 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
51, 2, 3, 4syl3anc 1363 1 (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3013  (class class class)co 7145  cc 10523  0cc0 10525   / cdiv 11285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286
This theorem is referenced by:  dmdcan2d  11434  mulsubdivbinom2  13610  hashf1  13803  abs1m  14683  abslem2  14687  sqreulem  14707  sqreu  14708  o1fsum  15156  divrcnv  15195  divcnv  15196  geolim  15214  geolim2  15215  geo2sum  15217  geo2lim  15219  fproddiv  15303  bpolycl  15394  bpolysum  15395  bpolydiflem  15396  bpoly4  15401  eftcl  15415  efaddlem  15434  tancl  15470  tanval2  15474  qredeq  15989  pcaddlem  16212  pjthlem1  23967  iblss  24332  itgeqa  24341  iblconst  24345  iblabsr  24357  iblmulc2  24358  itgsplit  24363  dvlem  24421  dvmulbr  24463  dvcobr  24470  dvrec  24479  dvrecg  24497  dvmptdiv  24498  dvcnvlem  24500  dveflem  24503  dvsincos  24505  dvlip  24517  c1liplem1  24520  lhop1lem  24537  lhop1  24538  lhop2  24539  lhop  24540  ftc1lem4  24563  vieta1lem2  24827  vieta1  24828  elqaalem3  24837  aareccl  24842  aalioulem1  24848  taylfvallem1  24872  tayl0  24877  taylply2  24883  taylply  24884  dvtaylp  24885  taylthlem2  24889  ulmdvlem1  24915  tanregt0  25050  eff1olem  25059  argregt0  25120  argrege0  25121  argimgt0  25122  logcnlem4  25155  advlogexp  25165  logtaylsum  25171  logtayl2  25172  root1eq1  25263  logbcl  25272  cxplogb  25291  logbf  25294  angcld  25310  angrteqvd  25311  cosangneg2d  25312  angrtmuld  25313  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  ang180lem4  25317  ang180lem5  25318  lawcoslem1  25320  lawcos  25321  isosctrlem2  25324  isosctrlem3  25325  angpieqvdlem  25333  angpieqvdlem2  25334  angpieqvd  25336  dcubic1lem  25348  dcubic2  25349  dcubic1  25350  dcubic  25351  mcubic  25352  cubic2  25353  dquartlem1  25356  dquartlem2  25357  dquart  25358  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem3  25364  quartlem4  25365  quart  25366  tanatan  25424  atantayl  25442  atantayl2  25443  atantayl3  25444  log2cnv  25449  birthdaylem2  25457  efrlim  25474  dfef2  25475  cxploglim2  25483  fsumharmonic  25516  lgamgulmlem2  25534  lgamgulmlem3  25535  lgamgulmlem4  25536  lgamgulmlem5  25537  lgamgulmlem6  25538  lgamgulm2  25540  lgamcvg2  25559  gamcvg  25560  gamcvg2lem  25563  ftalem4  25580  ftalem5  25581  basellem8  25592  logexprlim  25728  bposlem9  25795  2lgslem3d  25902  2sqlem3  25923  dchrmusum2  25997  dchrvmasum2lem  25999  dchrvmasumiflem1  26004  dchrvmasumiflem2  26005  dchrvmaeq0  26007  dchrisum0re  26016  dchrisum0lem1b  26018  dchrisum0lem1  26019  dchrisum0lem2a  26020  dchrisum0lem2  26021  dchrisum0lem3  26022  dchrisum0  26023  mudivsum  26033  vmalogdivsum2  26041  vmalogdivsum  26042  2vmadivsumlem  26043  selberg2  26054  selberg3lem1  26060  selberg3  26062  selberg4lem1  26063  selbergr  26071  selberg3r  26072  selberg4r  26073  selberg34r  26074  pntrlog2bndlem1  26080  pntrlog2bndlem2  26081  pntrlog2bndlem3  26082  pntrlog2bndlem4  26083  pntrlog2bndlem5  26084  colinearalg  26623  axcontlem8  26684  pjhthlem1  29095  eigvalcl  29665  riesz3i  29766  bcm1n  30444  divnumden2  30460  oddpwdc  31511  signsplypnf  31719  signsply0  31720  itgexpif  31776  hgt750leme  31828  subfacval2  32331  divcnvlin  32861  bcprod  32867  iprodgam  32871  unbdqndv2lem1  33745  knoppndvlem2  33749  knoppndvlem7  33754  knoppndvlem9  33756  knoppndvlem10  33757  knoppndvlem16  33763  knoppndvlem17  33764  itg2addnclem  34824  iblmulc2nc  34838  ftc1cnnclem  34846  areacirclem1  34863  areacirclem4  34866  areacirc  34868  cntotbnd  34955  pellexlem2  39305  pellexlem6  39309  jm2.19  39468  jm2.27c  39482  proot1ex  39679  cvgdvgrat  40522  radcnvrat  40523  hashnzfzclim  40531  bcccl  40548  bccm1k  40551  binomcxplemrat  40559  binomcxplemfrat  40560  binomcxplemnotnn0  40565  xralrple2  41498  mccllem  41754  clim1fr1  41758  0ellimcdiv  41806  coseq0  42021  fperdvper  42079  dvdivbd  42084  dvnmptdivc  42099  dvnxpaek  42103  dvnprodlem2  42108  iblsplit  42127  itgcoscmulx  42130  itgsincmulx  42135  stoweidlem11  42173  stoweidlem26  42188  stoweidlem42  42204  wallispilem4  42230  wallispilem5  42231  wallispi  42232  wallispi2lem1  42233  wallispi2lem2  42234  wallispi2  42235  stirlinglem1  42236  stirlinglem3  42238  stirlinglem4  42239  stirlinglem5  42240  stirlinglem6  42241  stirlinglem7  42242  stirlinglem13  42248  stirlinglem14  42249  stirlinglem15  42250  dirkeritg  42264  dirkercncflem1  42265  dirkercncflem2  42266  fourierdlem26  42295  fourierdlem39  42308  fourierdlem56  42324  fourierdlem62  42330  fourierdlem72  42340  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem80  42348  fourierdlem103  42371  fourierdlem104  42372  fouriersw  42393  elaa2lem  42395  etransclem15  42411  etransclem20  42416  etransclem21  42417  etransclem22  42418  etransclem23  42419  etransclem24  42420  etransclem25  42421  etransclem31  42427  etransclem32  42428  etransclem33  42429  etransclem34  42430  etransclem35  42431  etransclem47  42443  etransclem48  42444  hoiqssbllem2  42782  sigardiv  42995  sharhght  42999  cndivrenred  43383  fmtnoprmfac2lem1  43605  quad1  43662  requad01  43663  requad1  43664  fdivmptf  44529  affinecomb2  44618  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  itscnhlc0xyqsol  44680  itschlc0xyqsol1  44681  cotcl  44779
  Copyright terms: Public domain W3C validator