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

Theorem redivcld 11991
Description: Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
redivcld.1 (𝜑𝐴 ∈ ℝ)
redivcld.2 (𝜑𝐵 ∈ ℝ)
redivcld.3 (𝜑𝐵 ≠ 0)
Assertion
Ref Expression
redivcld (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Proof of Theorem redivcld
StepHypRef Expression
1 redivcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 redivcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 redivcld.3 . 2 (𝜑𝐵 ≠ 0)
4 redivcl 11882 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
51, 2, 3, 4syl3anc 1372 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 2940  (class class class)co 7361  cr 11058  0cc0 11059   / cdiv 11820
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 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821
This theorem is referenced by:  recp1lt1  12061  ledivp1  12065  supmul1  12132  rimul  12152  div4p1lem1div2  12416  divelunit  13420  fldiv4p1lem1div2  13749  fldiv4lem1div2uz2  13750  quoremz  13769  intfracq  13773  fldiv  13774  modmulnn  13803  modmuladd  13827  modmuladdnn0  13829  expnbnd  14144  discr1  14151  discr  14152  sqreulem  15253  fprodle  15887  fldivndvdslt  16304  flodddiv4t2lthalf  16306  iccpnfhmeo  24331  ipcau2  24621  mbfmulc2lem  25034  i1fmulc  25091  itg1mulc  25092  itg2monolem3  25140  dvferm2lem  25373  dvcvx  25407  radcnvlem1  25795  tanord1  25916  logf1o2  26028  relogbcl  26146  ang180lem2  26183  chordthmlem2  26206  jensenlem2  26360  regamcl  26433  gausslemma2dlem0d  26730  gausslemma2dlem3  26739  gausslemma2dlem4  26740  gausslemma2dlem5  26742  2lgslem1a2  26761  2lgslem1  26765  2lgslem2  26766  2lgsoddprmlem2  26780  selberg3lem1  26928  selberg4lem1  26931  ostth2  27008  ttgcontlem1  27882  colinearalg  27908  axsegconlem8  27922  axpaschlem  27938  axeuclidlem  27960  nmophmi  31022  unitdivcld  32546  dya2icoseg  32941  dya2iocucvr  32948  signsply0  33227  logdivsqrle  33327  hgt750lem  33328  hgt750leme  33335  tgoldbachgtde  33337  sinccvglem  34324  circum  34326  knoppndvlem1  35028  knoppndvlem14  35041  knoppndvlem15  35042  knoppndvlem17  35044  knoppndvlem18  35045  knoppndvlem19  35046  knoppndvlem21  35048  poimirlem31  36159  itg2addnclem  36179  itg2addnclem2  36180  areacirclem1  36216  areacirclem4  36219  lcmineqlem15  40550  3lexlogpow5ineq2  40562  3lexlogpow5ineq4  40563  3lexlogpow2ineq1  40565  3lexlogpow2ineq2  40566  3lexlogpow5ineq5  40567  dvrelog2  40571  dvrelog3  40572  dvrelog2b  40573  dvrelogpow2b  40575  aks4d1p1p4  40578  aks4d1p1p6  40580  aks4d1p1p7  40581  aks4d1p1p5  40582  aks4d1p5  40587  aks4d1p8  40594  2ap1caineq  40603  pellexlem1  41199  pellexlem6  41204  reglogcl  41260  modabsdifz  41357  areaquad  41597  imo72b2  42537  hashnzfzclim  42694  sineq0ALT  43311  suplesup  43664  reclt0d  43712  xrralrecnnge  43715  ltdiv23neg  43719  iooiinioc  43884  0ellimcdiv  43980  dvdivbd  44254  ioodvbdlimc1lem1  44262  ioodvbdlimc1lem2  44263  ioodvbdlimc2lem  44265  stoweidlem1  44332  stoweidlem13  44344  stoweidlem26  44357  stoweidlem34  44365  stoweidlem36  44367  stoweidlem51  44382  stoweidlem60  44391  wallispilem4  44399  wallispilem5  44400  stirlingr  44421  dirker2re  44423  dirkerval2  44425  dirkerre  44426  dirkertrigeq  44432  dirkeritg  44433  dirkercncflem1  44434  dirkercncflem4  44437  fourierdlem4  44442  fourierdlem7  44445  fourierdlem9  44447  fourierdlem16  44454  fourierdlem19  44457  fourierdlem21  44459  fourierdlem22  44460  fourierdlem24  44462  fourierdlem26  44464  fourierdlem30  44468  fourierdlem39  44477  fourierdlem41  44479  fourierdlem42  44480  fourierdlem43  44481  fourierdlem47  44484  fourierdlem48  44485  fourierdlem49  44486  fourierdlem51  44488  fourierdlem56  44493  fourierdlem57  44494  fourierdlem58  44495  fourierdlem59  44496  fourierdlem63  44500  fourierdlem64  44501  fourierdlem66  44503  fourierdlem71  44508  fourierdlem72  44509  fourierdlem78  44515  fourierdlem83  44520  fourierdlem87  44524  fourierdlem89  44526  fourierdlem90  44527  fourierdlem91  44528  fourierdlem95  44532  fourierdlem103  44540  fourierdlem104  44541  etransclem48  44613  qndenserrnbllem  44625  sge0rpcpnf  44752  sge0ad2en  44762  ovnsubaddlem1  44901  hoidmvlelem3  44928  ovolval5lem1  44983  ovolval5lem2  44984  vonioolem2  45012  vonicclem2  45015  pimrecltneg  45055  smfrec  45120  smfdiv  45128  sigardiv  45192  lighneallem2  45888  requad01  45903  requad1  45904  requad2  45905  modn0mul  46696  refdivmptf  46718  fldivexpfllog2  46741  dignnld  46779  dig2nn1st  46781  dig2bits  46790  dignn0flhalflem2  46792  affinecomb1  46878  eenglngeehlnmlem1  46913  eenglngeehlnmlem2  46914  rrx2vlinest  46917  line2ylem  46927  line2  46928  line2xlem  46929  itsclc0lem1  46932  itsclc0lem2  46933  itscnhlc0yqe  46935  itsclquadb  46952
  Copyright terms: Public domain W3C validator