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

Theorem redivcld 11461
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 11352 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
51, 2, 3, 4syl3anc 1368 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wne 2990  (class class class)co 7139  cr 10529  0cc0 10530   / cdiv 11290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291
This theorem is referenced by:  recp1lt1  11531  ledivp1  11535  supmul1  11601  rimul  11620  div4p1lem1div2  11884  divelunit  12876  fldiv4p1lem1div2  13204  fldiv4lem1div2uz2  13205  quoremz  13222  intfracq  13226  fldiv  13227  modmulnn  13256  modmuladd  13280  modmuladdnn0  13282  expnbnd  13593  discr1  13600  discr  13601  sqreulem  14714  fprodle  15345  fldivndvdslt  15758  flodddiv4t2lthalf  15760  iccpnfhmeo  23553  ipcau2  23841  mbfmulc2lem  24254  i1fmulc  24310  itg1mulc  24311  itg2monolem3  24359  dvferm2lem  24592  dvcvx  24626  radcnvlem1  25011  tanord1  25132  logf1o2  25244  relogbcl  25362  ang180lem2  25399  chordthmlem2  25422  jensenlem2  25576  regamcl  25649  gausslemma2dlem0d  25946  gausslemma2dlem3  25955  gausslemma2dlem4  25956  gausslemma2dlem5  25958  2lgslem1a2  25977  2lgslem1  25981  2lgslem2  25982  2lgsoddprmlem2  25996  selberg3lem1  26144  selberg4lem1  26147  ostth2  26224  ttgcontlem1  26682  colinearalg  26707  axsegconlem8  26721  axpaschlem  26737  axeuclidlem  26759  nmophmi  29817  unitdivcld  31252  dya2icoseg  31643  dya2iocucvr  31650  signsply0  31929  logdivsqrle  32029  hgt750lem  32030  hgt750leme  32037  tgoldbachgtde  32039  sinccvglem  33023  circum  33025  knoppndvlem1  33959  knoppndvlem14  33972  knoppndvlem15  33973  knoppndvlem17  33975  knoppndvlem18  33976  knoppndvlem19  33977  knoppndvlem21  33979  poimirlem31  35081  itg2addnclem  35101  itg2addnclem2  35102  areacirclem1  35138  areacirclem4  35141  lcmineqlem15  39324  2ap1caineq  39340  pellexlem1  39757  pellexlem6  39762  reglogcl  39818  modabsdifz  39914  areaquad  40153  imo72b2  40865  hashnzfzclim  41013  sineq0ALT  41630  suplesup  41958  reclt0d  42009  xrralrecnnge  42013  ltdiv23neg  42017  iooiinioc  42180  0ellimcdiv  42278  dvdivbd  42552  ioodvbdlimc1lem1  42560  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  stoweidlem1  42630  stoweidlem13  42642  stoweidlem26  42655  stoweidlem34  42663  stoweidlem36  42665  stoweidlem51  42680  stoweidlem60  42689  wallispilem4  42697  wallispilem5  42698  stirlingr  42719  dirker2re  42721  dirkerval2  42723  dirkerre  42724  dirkertrigeq  42730  dirkeritg  42731  dirkercncflem1  42732  dirkercncflem4  42735  fourierdlem4  42740  fourierdlem7  42743  fourierdlem9  42745  fourierdlem16  42752  fourierdlem19  42755  fourierdlem21  42757  fourierdlem22  42758  fourierdlem24  42760  fourierdlem26  42762  fourierdlem30  42766  fourierdlem39  42775  fourierdlem41  42777  fourierdlem42  42778  fourierdlem43  42779  fourierdlem47  42782  fourierdlem48  42783  fourierdlem49  42784  fourierdlem51  42786  fourierdlem56  42791  fourierdlem57  42792  fourierdlem58  42793  fourierdlem59  42794  fourierdlem63  42798  fourierdlem64  42799  fourierdlem66  42801  fourierdlem71  42806  fourierdlem72  42807  fourierdlem78  42813  fourierdlem83  42818  fourierdlem87  42822  fourierdlem89  42824  fourierdlem90  42825  fourierdlem91  42826  fourierdlem95  42830  fourierdlem103  42838  fourierdlem104  42839  etransclem48  42911  qndenserrnbllem  42923  sge0rpcpnf  43047  sge0ad2en  43057  ovnsubaddlem1  43196  hoidmvlelem3  43223  ovolval5lem1  43278  ovolval5lem2  43279  vonioolem2  43307  vonicclem2  43310  pimrecltneg  43345  smfrec  43408  smfdiv  43416  sigardiv  43462  lighneallem2  44111  requad01  44126  requad1  44127  requad2  44128  modn0mul  44921  refdivmptf  44943  fldivexpfllog2  44966  dignnld  45004  dig2nn1st  45006  dig2bits  45015  dignn0flhalflem2  45017  affinecomb1  45103  eenglngeehlnmlem1  45138  eenglngeehlnmlem2  45139  rrx2vlinest  45142  line2ylem  45152  line2  45153  line2xlem  45154  itsclc0lem1  45157  itsclc0lem2  45158  itscnhlc0yqe  45160  itsclquadb  45177
  Copyright terms: Public domain W3C validator