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

Theorem redivcld 11037
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 10928 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
51, 2, 3, 4syl3anc 1473 1 (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2131  wne 2924  (class class class)co 6805  cr 10119  0cc0 10120   / cdiv 10868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-po 5179  df-so 5180  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869
This theorem is referenced by:  recp1lt1  11105  ledivp1  11109  supmul1  11176  rimul  11195  div4p1lem1div2  11471  divelunit  12499  fldiv4p1lem1div2  12822  fldiv4lem1div2uz2  12823  quoremz  12840  intfracq  12844  fldiv  12845  modmulnn  12874  modmuladd  12898  modmuladdnn0  12900  expnbnd  13179  discr1  13186  discr  13187  sqreulem  14290  fprodle  14918  fldivndvdslt  15332  flodddiv4t2lthalf  15334  iccpnfhmeo  22937  ipcau2  23225  mbfmulc2lem  23605  i1fmulc  23661  itg1mulc  23662  itg2monolem3  23710  dvferm2lem  23940  dvcvx  23974  radcnvlem1  24358  tanord1  24474  logf1o2  24587  relogbcl  24702  ang180lem2  24731  chordthmlem2  24751  jensenlem2  24905  regamcl  24978  gausslemma2dlem0d  25275  gausslemma2dlem3  25284  gausslemma2dlem4  25285  gausslemma2dlem5  25287  2lgslem1a2  25306  2lgslem1  25310  2lgslem2  25311  2lgsoddprmlem2  25325  selberg3lem1  25437  selberg4lem1  25440  ostth2  25517  ttgcontlem1  25956  colinearalg  25981  axsegconlem8  25995  axpaschlem  26011  axeuclidlem  26033  nmophmi  29191  unitdivcld  30248  dya2icoseg  30640  dya2iocucvr  30647  signsply0  30929  logdivsqrle  31029  hgt750lem  31030  hgt750leme  31037  tgoldbachgtde  31039  sinccvglem  31865  circum  31867  knoppndvlem1  32801  knoppndvlem14  32814  knoppndvlem15  32815  knoppndvlem17  32817  knoppndvlem18  32818  knoppndvlem19  32819  knoppndvlem21  32821  poimirlem31  33745  itg2addnclem  33766  itg2addnclem2  33767  areacirclem1  33805  areacirclem4  33808  pellexlem1  37887  pellexlem6  37892  reglogcl  37948  modabsdifz  38047  areaquad  38296  imo72b2  38969  hashnzfzclim  39015  sineq0ALT  39664  suplesup  40045  reclt0d  40097  xrralrecnnge  40103  ltdiv23neg  40107  iooiinioc  40278  0ellimcdiv  40376  dvdivbd  40633  ioodvbdlimc1lem1  40641  ioodvbdlimc1lem2  40642  ioodvbdlimc2lem  40644  stoweidlem1  40713  stoweidlem13  40725  stoweidlem26  40738  stoweidlem34  40746  stoweidlem36  40748  stoweidlem51  40763  stoweidlem60  40772  wallispilem4  40780  wallispilem5  40781  stirlingr  40802  dirker2re  40804  dirkerval2  40806  dirkerre  40807  dirkertrigeq  40813  dirkeritg  40814  dirkercncflem1  40815  dirkercncflem4  40818  fourierdlem4  40823  fourierdlem7  40826  fourierdlem9  40828  fourierdlem16  40835  fourierdlem19  40838  fourierdlem21  40840  fourierdlem22  40841  fourierdlem24  40843  fourierdlem26  40845  fourierdlem30  40849  fourierdlem39  40858  fourierdlem41  40860  fourierdlem42  40861  fourierdlem43  40862  fourierdlem47  40865  fourierdlem48  40866  fourierdlem49  40867  fourierdlem51  40869  fourierdlem56  40874  fourierdlem57  40875  fourierdlem58  40876  fourierdlem59  40877  fourierdlem63  40881  fourierdlem64  40882  fourierdlem66  40884  fourierdlem71  40889  fourierdlem72  40890  fourierdlem78  40896  fourierdlem83  40901  fourierdlem87  40905  fourierdlem89  40907  fourierdlem90  40908  fourierdlem91  40909  fourierdlem95  40913  fourierdlem103  40921  fourierdlem104  40922  etransclem48  40994  qndenserrnbllem  41009  sge0rpcpnf  41133  sge0ad2en  41143  ovnsubaddlem1  41282  hoidmvlelem3  41309  ovolval5lem1  41364  ovolval5lem2  41365  vonioolem2  41393  vonicclem2  41396  pimrecltneg  41431  smfrec  41494  smfdiv  41502  sigardiv  41548  lighneallem2  42025  modn0mul  42817  refdivmptf  42838  fldivexpfllog2  42861  dignnld  42899  dig2nn1st  42901  dig2bits  42910  dignn0flhalflem2  42912
  Copyright terms: Public domain W3C validator