Theorem redivcld 11468

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

Step	Hyp	Ref	Expression
1		redivcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		redivcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		redivcld.3	. 2 ⊢ (𝜑 → 𝐵 ≠ 0)
4		redivcl 11359	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3016  (class class class)co 7156  ℝcr 10536  0cc0 10537   / cdiv 11297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298

This theorem is referenced by:  recp1lt1  11538  ledivp1  11542  supmul1  11610  rimul  11629  div4p1lem1div2  11893  divelunit  12881  fldiv4p1lem1div2  13206  fldiv4lem1div2uz2  13207  quoremz  13224  intfracq  13228  fldiv  13229  modmulnn  13258  modmuladd  13282  modmuladdnn0  13284  expnbnd  13594  discr1  13601  discr  13602  sqreulem  14719  fprodle  15350  fldivndvdslt  15765  flodddiv4t2lthalf  15767  iccpnfhmeo  23549  ipcau2  23837  mbfmulc2lem  24248  i1fmulc  24304  itg1mulc  24305  itg2monolem3  24353  dvferm2lem  24583  dvcvx  24617  radcnvlem1  25001  tanord1  25121  logf1o2  25233  relogbcl  25351  ang180lem2  25388  chordthmlem2  25411  jensenlem2  25565  regamcl  25638  gausslemma2dlem0d  25935  gausslemma2dlem3  25944  gausslemma2dlem4  25945  gausslemma2dlem5  25947  2lgslem1a2  25966  2lgslem1  25970  2lgslem2  25971  2lgsoddprmlem2  25985  selberg3lem1  26133  selberg4lem1  26136  ostth2  26213  ttgcontlem1  26671  colinearalg  26696  axsegconlem8  26710  axpaschlem  26726  axeuclidlem  26748  nmophmi  29808  unitdivcld  31144  dya2icoseg  31535  dya2iocucvr  31542  signsply0  31821  logdivsqrle  31921  hgt750lem  31922  hgt750leme  31929  tgoldbachgtde  31931  sinccvglem  32915  circum  32917  knoppndvlem1  33851  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem21  33871  poimirlem31  34938  itg2addnclem  34958  itg2addnclem2  34959  areacirclem1  34997  areacirclem4  35000  pellexlem1  39446  pellexlem6  39451  reglogcl  39507  modabsdifz  39603  areaquad  39843  imo72b2  40545  hashnzfzclim  40674  sineq0ALT  41291  suplesup  41627  reclt0d  41678  xrralrecnnge  41682  ltdiv23neg  41686  iooiinioc  41852  0ellimcdiv  41950  dvdivbd  42228  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  stoweidlem1  42306  stoweidlem13  42318  stoweidlem26  42331  stoweidlem34  42339  stoweidlem36  42341  stoweidlem51  42356  stoweidlem60  42365  wallispilem4  42373  wallispilem5  42374  stirlingr  42395  dirker2re  42397  dirkerval2  42399  dirkerre  42400  dirkertrigeq  42406  dirkeritg  42407  dirkercncflem1  42408  dirkercncflem4  42411  fourierdlem4  42416  fourierdlem7  42419  fourierdlem9  42421  fourierdlem16  42428  fourierdlem19  42431  fourierdlem21  42433  fourierdlem22  42434  fourierdlem24  42436  fourierdlem26  42438  fourierdlem30  42442  fourierdlem39  42451  fourierdlem41  42453  fourierdlem42  42454  fourierdlem43  42455  fourierdlem47  42458  fourierdlem48  42459  fourierdlem49  42460  fourierdlem51  42462  fourierdlem56  42467  fourierdlem57  42468  fourierdlem58  42469  fourierdlem59  42470  fourierdlem63  42474  fourierdlem64  42475  fourierdlem66  42477  fourierdlem71  42482  fourierdlem72  42483  fourierdlem78  42489  fourierdlem83  42494  fourierdlem87  42498  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem95  42506  fourierdlem103  42514  fourierdlem104  42515  etransclem48  42587  qndenserrnbllem  42599  sge0rpcpnf  42723  sge0ad2en  42733  ovnsubaddlem1  42872  hoidmvlelem3  42899  ovolval5lem1  42954  ovolval5lem2  42955  vonioolem2  42983  vonicclem2  42986  pimrecltneg  43021  smfrec  43084  smfdiv  43092  sigardiv  43138  lighneallem2  43791  requad01  43806  requad1  43807  requad2  43808  modn0mul  44600  refdivmptf  44622  fldivexpfllog2  44645  dignnld  44683  dig2nn1st  44685  dig2bits  44694  dignn0flhalflem2  44696  affinecomb1  44709  eenglngeehlnmlem1  44744  eenglngeehlnmlem2  44745  rrx2vlinest  44748  line2ylem  44758  line2  44759  line2xlem  44760  itsclc0lem1  44763  itsclc0lem2  44764  itscnhlc0yqe  44766  itsclquadb  44783