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

Theorem divcld 11408
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 11296 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
51, 2, 3, 4syl3anc 1365 1 (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 3014  (class class class)co 7148  cc 10527  0cc0 10529   / cdiv 11289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  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 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290
This theorem is referenced by:  dmdcan2d  11438  mulsubdivbinom2  13614  hashf1  13807  abs1m  14687  abslem2  14691  sqreulem  14711  sqreu  14712  o1fsum  15160  divrcnv  15199  divcnv  15200  geolim  15218  geolim2  15219  geo2sum  15221  geo2lim  15223  fproddiv  15307  bpolycl  15398  bpolysum  15399  bpolydiflem  15400  bpoly4  15405  eftcl  15419  efaddlem  15438  tancl  15474  tanval2  15478  qredeq  15993  pcaddlem  16216  pjthlem1  24032  iblss  24397  itgeqa  24406  iblconst  24410  iblabsr  24422  iblmulc2  24423  itgsplit  24428  dvlem  24486  dvmulbr  24528  dvcobr  24535  dvrec  24544  dvrecg  24562  dvmptdiv  24563  dvcnvlem  24565  dveflem  24568  dvsincos  24570  dvlip  24582  c1liplem1  24585  lhop1lem  24602  lhop1  24603  lhop2  24604  lhop  24605  ftc1lem4  24628  vieta1lem2  24892  vieta1  24893  elqaalem3  24902  aareccl  24907  aalioulem1  24913  taylfvallem1  24937  tayl0  24942  taylply2  24948  taylply  24949  dvtaylp  24950  taylthlem2  24954  ulmdvlem1  24980  tanregt0  25115  eff1olem  25124  argregt0  25185  argrege0  25186  argimgt0  25187  logcnlem4  25220  advlogexp  25230  logtaylsum  25236  logtayl2  25237  root1eq1  25328  logbcl  25337  cxplogb  25356  logbf  25359  angcld  25375  angrteqvd  25376  cosangneg2d  25377  angrtmuld  25378  ang180lem1  25379  ang180lem2  25380  ang180lem3  25381  ang180lem4  25382  ang180lem5  25383  lawcoslem1  25385  lawcos  25386  isosctrlem2  25389  isosctrlem3  25390  angpieqvdlem  25398  angpieqvdlem2  25399  angpieqvd  25401  dcubic1lem  25413  dcubic2  25414  dcubic1  25415  dcubic  25416  mcubic  25417  cubic2  25418  dquartlem1  25421  dquartlem2  25422  dquart  25423  quart1cl  25424  quart1lem  25425  quart1  25426  quartlem3  25429  quartlem4  25430  quart  25431  tanatan  25489  atantayl  25507  atantayl2  25508  atantayl3  25509  log2cnv  25514  birthdaylem2  25522  efrlim  25539  dfef2  25540  cxploglim2  25548  fsumharmonic  25581  lgamgulmlem2  25599  lgamgulmlem3  25600  lgamgulmlem4  25601  lgamgulmlem5  25602  lgamgulmlem6  25603  lgamgulm2  25605  lgamcvg2  25624  gamcvg  25625  gamcvg2lem  25628  ftalem4  25645  ftalem5  25646  basellem8  25657  logexprlim  25793  bposlem9  25860  2lgslem3d  25967  2sqlem3  25988  dchrmusum2  26062  dchrvmasum2lem  26064  dchrvmasumiflem1  26069  dchrvmasumiflem2  26070  dchrvmaeq0  26072  dchrisum0re  26081  dchrisum0lem1b  26083  dchrisum0lem1  26084  dchrisum0lem2a  26085  dchrisum0lem2  26086  dchrisum0lem3  26087  dchrisum0  26088  mudivsum  26098  vmalogdivsum2  26106  vmalogdivsum  26107  2vmadivsumlem  26108  selberg2  26119  selberg3lem1  26125  selberg3  26127  selberg4lem1  26128  selbergr  26136  selberg3r  26137  selberg4r  26138  selberg34r  26139  pntrlog2bndlem1  26145  pntrlog2bndlem2  26146  pntrlog2bndlem3  26147  pntrlog2bndlem4  26148  pntrlog2bndlem5  26149  colinearalg  26688  axcontlem8  26749  pjhthlem1  29160  eigvalcl  29730  riesz3i  29831  bcm1n  30510  divnumden2  30526  oddpwdc  31605  signsplypnf  31813  signsply0  31814  itgexpif  31870  hgt750leme  31922  subfacval2  32427  divcnvlin  32957  bcprod  32963  iprodgam  32967  unbdqndv2lem1  33841  knoppndvlem2  33845  knoppndvlem7  33850  knoppndvlem9  33852  knoppndvlem10  33853  knoppndvlem16  33859  knoppndvlem17  33860  itg2addnclem  34935  iblmulc2nc  34949  ftc1cnnclem  34957  areacirclem1  34974  areacirclem4  34977  areacirc  34979  cntotbnd  35066  pellexlem2  39417  pellexlem6  39421  jm2.19  39580  jm2.27c  39594  proot1ex  39791  cvgdvgrat  40635  radcnvrat  40636  hashnzfzclim  40644  bcccl  40661  bccm1k  40664  binomcxplemrat  40672  binomcxplemfrat  40673  binomcxplemnotnn0  40678  xralrple2  41611  mccllem  41867  clim1fr1  41871  0ellimcdiv  41919  coseq0  42134  fperdvper  42192  dvdivbd  42197  dvnmptdivc  42212  dvnxpaek  42216  dvnprodlem2  42221  iblsplit  42240  itgcoscmulx  42243  itgsincmulx  42248  stoweidlem11  42286  stoweidlem26  42301  stoweidlem42  42317  wallispilem4  42343  wallispilem5  42344  wallispi  42345  wallispi2lem1  42346  wallispi2lem2  42347  wallispi2  42348  stirlinglem1  42349  stirlinglem3  42351  stirlinglem4  42352  stirlinglem5  42353  stirlinglem6  42354  stirlinglem7  42355  stirlinglem13  42361  stirlinglem14  42362  stirlinglem15  42363  dirkeritg  42377  dirkercncflem1  42378  dirkercncflem2  42379  fourierdlem26  42408  fourierdlem39  42421  fourierdlem56  42437  fourierdlem62  42443  fourierdlem72  42453  fourierdlem74  42455  fourierdlem75  42456  fourierdlem76  42457  fourierdlem80  42461  fourierdlem103  42484  fourierdlem104  42485  fouriersw  42506  elaa2lem  42508  etransclem15  42524  etransclem20  42529  etransclem21  42530  etransclem22  42531  etransclem23  42532  etransclem24  42533  etransclem25  42534  etransclem31  42540  etransclem32  42541  etransclem33  42542  etransclem34  42543  etransclem35  42544  etransclem47  42556  etransclem48  42557  hoiqssbllem2  42895  sigardiv  43108  sharhght  43112  cndivrenred  43496  fmtnoprmfac2lem1  43718  quad1  43775  requad01  43776  requad1  43777  fdivmptf  44591  affinecomb2  44680  eenglngeehlnmlem1  44714  eenglngeehlnmlem2  44715  itscnhlc0xyqsol  44742  itschlc0xyqsol1  44743  cotcl  44841
  Copyright terms: Public domain W3C validator