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

Theorem redivcld 11045
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 10936 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
51, 2, 3, 4syl3anc 1477 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wne 2932  (class class class)co 6813  cr 10127  0cc0 10128   / cdiv 10876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877
This theorem is referenced by:  recp1lt1  11113  ledivp1  11117  supmul1  11184  rimul  11203  div4p1lem1div2  11479  divelunit  12507  fldiv4p1lem1div2  12830  fldiv4lem1div2uz2  12831  quoremz  12848  intfracq  12852  fldiv  12853  modmulnn  12882  modmuladd  12906  modmuladdnn0  12908  expnbnd  13187  discr1  13194  discr  13195  sqreulem  14298  fprodle  14926  fldivndvdslt  15340  flodddiv4t2lthalf  15342  iccpnfhmeo  22945  ipcau2  23233  mbfmulc2lem  23613  i1fmulc  23669  itg1mulc  23670  itg2monolem3  23718  dvferm2lem  23948  dvcvx  23982  radcnvlem1  24366  tanord1  24482  logf1o2  24595  relogbcl  24710  ang180lem2  24739  chordthmlem2  24759  jensenlem2  24913  regamcl  24986  gausslemma2dlem0d  25283  gausslemma2dlem3  25292  gausslemma2dlem4  25293  gausslemma2dlem5  25295  2lgslem1a2  25314  2lgslem1  25318  2lgslem2  25319  2lgsoddprmlem2  25333  selberg3lem1  25445  selberg4lem1  25448  ostth2  25525  ttgcontlem1  25964  colinearalg  25989  axsegconlem8  26003  axpaschlem  26019  axeuclidlem  26041  nmophmi  29199  unitdivcld  30256  dya2icoseg  30648  dya2iocucvr  30655  signsply0  30937  logdivsqrle  31037  hgt750lem  31038  hgt750leme  31045  tgoldbachgtde  31047  sinccvglem  31873  circum  31875  knoppndvlem1  32809  knoppndvlem14  32822  knoppndvlem15  32823  knoppndvlem17  32825  knoppndvlem18  32826  knoppndvlem19  32827  knoppndvlem21  32829  poimirlem31  33753  itg2addnclem  33774  itg2addnclem2  33775  areacirclem1  33813  areacirclem4  33816  pellexlem1  37895  pellexlem6  37900  reglogcl  37956  modabsdifz  38055  areaquad  38304  imo72b2  38977  hashnzfzclim  39023  sineq0ALT  39672  suplesup  40053  reclt0d  40105  xrralrecnnge  40111  ltdiv23neg  40115  iooiinioc  40286  0ellimcdiv  40384  dvdivbd  40641  ioodvbdlimc1lem1  40649  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  stoweidlem1  40721  stoweidlem13  40733  stoweidlem26  40746  stoweidlem34  40754  stoweidlem36  40756  stoweidlem51  40771  stoweidlem60  40780  wallispilem4  40788  wallispilem5  40789  stirlingr  40810  dirker2re  40812  dirkerval2  40814  dirkerre  40815  dirkertrigeq  40821  dirkeritg  40822  dirkercncflem1  40823  dirkercncflem4  40826  fourierdlem4  40831  fourierdlem7  40834  fourierdlem9  40836  fourierdlem16  40843  fourierdlem19  40846  fourierdlem21  40848  fourierdlem22  40849  fourierdlem24  40851  fourierdlem26  40853  fourierdlem30  40857  fourierdlem39  40866  fourierdlem41  40868  fourierdlem42  40869  fourierdlem43  40870  fourierdlem47  40873  fourierdlem48  40874  fourierdlem49  40875  fourierdlem51  40877  fourierdlem56  40882  fourierdlem57  40883  fourierdlem58  40884  fourierdlem59  40885  fourierdlem63  40889  fourierdlem64  40890  fourierdlem66  40892  fourierdlem71  40897  fourierdlem72  40898  fourierdlem78  40904  fourierdlem83  40909  fourierdlem87  40913  fourierdlem89  40915  fourierdlem90  40916  fourierdlem91  40917  fourierdlem95  40921  fourierdlem103  40929  fourierdlem104  40930  etransclem48  41002  qndenserrnbllem  41017  sge0rpcpnf  41141  sge0ad2en  41151  ovnsubaddlem1  41290  hoidmvlelem3  41317  ovolval5lem1  41372  ovolval5lem2  41373  vonioolem2  41401  vonicclem2  41404  pimrecltneg  41439  smfrec  41502  smfdiv  41510  sigardiv  41556  lighneallem2  42033  modn0mul  42825  refdivmptf  42846  fldivexpfllog2  42869  dignnld  42907  dig2nn1st  42909  dig2bits  42918  dignn0flhalflem2  42920
  Copyright terms: Public domain W3C validator