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

Theorem divcld 11932
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 11820 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ)
51, 2, 3, 4syl3anc 1372 1 (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 2944  (class class class)co 7358  cc 11050  0cc0 11052   / cdiv 11813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814
This theorem is referenced by:  dmdcan2d  11962  mulsubdivbinom2  14163  hashf1  14357  abs1m  15221  abslem2  15225  sqreulem  15245  sqreu  15246  o1fsum  15699  divrcnv  15738  divcnv  15739  geolim  15756  geolim2  15757  geo2sum  15759  geo2lim  15761  fproddiv  15845  bpolycl  15936  bpolysum  15937  bpolydiflem  15938  bpoly4  15943  eftcl  15957  efaddlem  15976  tancl  16012  tanval2  16016  qredeq  16534  pcaddlem  16761  pjthlem1  24804  iblss  25172  itgeqa  25181  iblconst  25185  iblabsr  25197  iblmulc2  25198  itgsplit  25203  dvlem  25263  dvmulbr  25306  dvcobr  25313  dvrec  25322  dvrecg  25340  dvmptdiv  25341  dvcnvlem  25343  dveflem  25346  dvsincos  25348  dvlip  25360  c1liplem1  25363  lhop1lem  25380  lhop1  25381  lhop2  25382  lhop  25383  ftc1lem4  25406  vieta1lem2  25674  vieta1  25675  elqaalem3  25684  aareccl  25689  aalioulem1  25695  taylfvallem1  25719  tayl0  25724  taylply2  25730  taylply  25731  dvtaylp  25732  taylthlem2  25736  ulmdvlem1  25762  tanregt0  25898  eff1olem  25907  argregt0  25968  argrege0  25969  argimgt0  25970  logcnlem4  26003  advlogexp  26013  logtaylsum  26019  logtayl2  26020  root1eq1  26111  logbcl  26120  cxplogb  26139  logbf  26142  angcld  26158  angrteqvd  26159  cosangneg2d  26160  angrtmuld  26161  ang180lem1  26162  ang180lem2  26163  ang180lem3  26164  ang180lem4  26165  ang180lem5  26166  lawcoslem1  26168  lawcos  26169  isosctrlem2  26172  isosctrlem3  26173  angpieqvdlem  26181  angpieqvdlem2  26182  angpieqvd  26184  dcubic1lem  26196  dcubic2  26197  dcubic1  26198  dcubic  26199  mcubic  26200  cubic2  26201  dquartlem1  26204  dquartlem2  26205  dquart  26206  quart1cl  26207  quart1lem  26208  quart1  26209  quartlem3  26212  quartlem4  26213  quart  26214  tanatan  26272  atantayl  26290  atantayl2  26291  atantayl3  26292  log2cnv  26297  birthdaylem2  26305  efrlim  26322  dfef2  26323  cxploglim2  26331  fsumharmonic  26364  lgamgulmlem2  26382  lgamgulmlem3  26383  lgamgulmlem4  26384  lgamgulmlem5  26385  lgamgulmlem6  26386  lgamgulm2  26388  lgamcvg2  26407  gamcvg  26408  gamcvg2lem  26411  ftalem4  26428  ftalem5  26429  basellem8  26440  logexprlim  26576  bposlem9  26643  2lgslem3d  26750  2sqlem3  26771  dchrmusum2  26845  dchrvmasum2lem  26847  dchrvmasumiflem1  26852  dchrvmasumiflem2  26853  dchrvmaeq0  26855  dchrisum0re  26864  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0lem2a  26868  dchrisum0lem2  26869  dchrisum0lem3  26870  dchrisum0  26871  mudivsum  26881  vmalogdivsum2  26889  vmalogdivsum  26890  2vmadivsumlem  26891  selberg2  26902  selberg3lem1  26908  selberg3  26910  selberg4lem1  26911  selbergr  26919  selberg3r  26920  selberg4r  26921  selberg34r  26922  pntrlog2bndlem1  26928  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  colinearalg  27862  axcontlem8  27923  pjhthlem1  30336  eigvalcl  30906  riesz3i  31007  bcm1n  31701  divnumden2  31717  oddpwdc  32957  signsplypnf  33165  signsply0  33166  itgexpif  33222  hgt750leme  33274  subfacval2  33784  divcnvlin  34308  bcprod  34314  iprodgam  34318  unbdqndv2lem1  34975  knoppndvlem2  34979  knoppndvlem7  34984  knoppndvlem9  34986  knoppndvlem10  34987  knoppndvlem16  34993  knoppndvlem17  34994  itg2addnclem  36132  iblmulc2nc  36146  ftc1cnnclem  36152  areacirclem1  36169  areacirclem4  36172  areacirc  36174  cntotbnd  36258  recbothd  40453  lcmineqlem12  40500  lcmineqlem18  40506  dvrelogpow2b  40528  aks4d1p1p2  40530  aks4d1p1p7  40534  aks6d1c2p2  40552  2ap1caineq  40556  pellexlem2  41156  pellexlem6  41160  jm2.19  41320  jm2.27c  41334  proot1ex  41531  cvgdvgrat  42600  radcnvrat  42601  hashnzfzclim  42609  bcccl  42626  bccm1k  42629  binomcxplemrat  42637  binomcxplemfrat  42638  binomcxplemnotnn0  42643  xralrple2  43595  mccllem  43845  clim1fr1  43849  0ellimcdiv  43897  coseq0  44112  fperdvper  44167  dvdivbd  44171  dvnmptdivc  44186  dvnxpaek  44190  dvnprodlem2  44195  iblsplit  44214  itgcoscmulx  44217  itgsincmulx  44222  stoweidlem11  44259  stoweidlem26  44274  stoweidlem42  44290  wallispilem4  44316  wallispilem5  44317  wallispi  44318  wallispi2lem1  44319  wallispi2lem2  44320  wallispi2  44321  stirlinglem1  44322  stirlinglem3  44324  stirlinglem4  44325  stirlinglem5  44326  stirlinglem6  44327  stirlinglem7  44328  stirlinglem13  44334  stirlinglem14  44335  stirlinglem15  44336  dirkeritg  44350  dirkercncflem1  44351  dirkercncflem2  44352  fourierdlem26  44381  fourierdlem39  44394  fourierdlem56  44410  fourierdlem62  44416  fourierdlem72  44426  fourierdlem74  44428  fourierdlem75  44429  fourierdlem76  44430  fourierdlem80  44434  fourierdlem103  44457  fourierdlem104  44458  fouriersw  44479  elaa2lem  44481  etransclem15  44497  etransclem20  44502  etransclem21  44503  etransclem22  44504  etransclem23  44505  etransclem24  44506  etransclem25  44507  etransclem31  44513  etransclem32  44514  etransclem33  44515  etransclem34  44516  etransclem35  44517  etransclem47  44529  etransclem48  44530  hoiqssbllem2  44871  sigardiv  45109  sharhght  45113  cndivrenred  45545  fmtnoprmfac2lem1  45765  quad1  45819  requad01  45820  requad1  45821  fdivmptf  46634  affinecomb2  46796  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  itscnhlc0xyqsol  46858  itschlc0xyqsol1  46859  cotcl  47204
  Copyright terms: Public domain W3C validator