Theorem redivcld 11983

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 11874	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7370  ℝcr 11039  0cc0 11040   / cdiv 11808

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-div 11809

This theorem is referenced by:  recp1lt1  12054  ledivp1  12058  supmul1  12125  rimul  12150  div4p1lem1div2  12410  divelunit  13424  fldiv4p1lem1div2  13769  fldiv4lem1div2uz2  13770  quoremz  13789  intfracq  13793  fldiv  13794  modmulnn  13823  modmuladd  13850  modmuladdnn0  13852  expnbnd  14169  discr1  14176  discr  14177  sqreulem  15297  fprodle  15933  fldivndvdslt  16357  flodddiv4t2lthalf  16359  iccpnfhmeo  24916  ipcau2  25207  mbfmulc2lem  25621  i1fmulc  25677  itg1mulc  25678  itg2monolem3  25726  dvferm2lem  25963  dvcvx  25998  radcnvlem1  26395  tanord1  26519  logf1o2  26632  relogbcl  26756  ang180lem2  26793  chordthmlem2  26816  jensenlem2  26971  regamcl  27044  gausslemma2dlem0d  27343  gausslemma2dlem3  27352  gausslemma2dlem4  27353  gausslemma2dlem5  27355  2lgslem1a2  27374  2lgslem1  27378  2lgslem2  27379  2lgsoddprmlem2  27393  selberg3lem1  27541  selberg4lem1  27544  ostth2  27621  ttgcontlem1  28975  colinearalg  29001  axsegconlem8  29015  axpaschlem  29031  axeuclidlem  29053  nmophmi  32125  cos9thpinconstrlem1  33973  unitdivcld  34085  dya2icoseg  34461  dya2iocucvr  34468  signsply0  34735  logdivsqrle  34834  hgt750lem  34835  hgt750leme  34842  tgoldbachgtde  34844  sinccvglem  35894  circum  35896  knoppndvlem1  36740  knoppndvlem14  36753  knoppndvlem15  36754  knoppndvlem17  36756  knoppndvlem18  36757  knoppndvlem19  36758  knoppndvlem21  36760  poimirlem31  37931  itg2addnclem  37951  itg2addnclem2  37952  areacirclem1  37988  areacirclem4  37991  lcmineqlem15  42442  3lexlogpow5ineq2  42454  3lexlogpow5ineq4  42455  3lexlogpow2ineq1  42457  3lexlogpow2ineq2  42458  3lexlogpow5ineq5  42459  dvrelog2  42463  dvrelog3  42464  dvrelog2b  42465  dvrelogpow2b  42467  aks4d1p1p4  42470  aks4d1p1p6  42472  aks4d1p1p7  42473  aks4d1p1p5  42474  aks4d1p5  42479  aks4d1p8  42486  aks6d1c2lem4  42526  2ap1caineq  42544  bcled  42577  bcle2d  42578  aks6d1c7lem1  42579  pellexlem1  43215  pellexlem6  43220  reglogcl  43276  modabsdifz  43372  areaquad  43602  imo72b2  44557  hashnzfzclim  44707  sineq0ALT  45321  suplesup  45727  reclt0d  45774  xrralrecnnge  45777  ltdiv23neg  45781  iooiinioc  45945  0ellimcdiv  46036  dvdivbd  46310  ioodvbdlimc1lem1  46318  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweidlem1  46388  stoweidlem13  46400  stoweidlem26  46413  stoweidlem34  46421  stoweidlem36  46423  stoweidlem51  46438  stoweidlem60  46447  wallispilem4  46455  wallispilem5  46456  stirlingr  46477  dirker2re  46479  dirkerval2  46481  dirkerre  46482  dirkertrigeq  46488  dirkeritg  46489  dirkercncflem1  46490  dirkercncflem4  46493  fourierdlem4  46498  fourierdlem7  46501  fourierdlem9  46503  fourierdlem16  46510  fourierdlem19  46513  fourierdlem21  46515  fourierdlem22  46516  fourierdlem24  46518  fourierdlem26  46520  fourierdlem30  46524  fourierdlem39  46533  fourierdlem41  46535  fourierdlem42  46536  fourierdlem43  46537  fourierdlem47  46540  fourierdlem48  46541  fourierdlem49  46542  fourierdlem51  46544  fourierdlem56  46549  fourierdlem57  46550  fourierdlem58  46551  fourierdlem59  46552  fourierdlem63  46556  fourierdlem64  46557  fourierdlem66  46559  fourierdlem71  46564  fourierdlem72  46565  fourierdlem78  46571  fourierdlem83  46576  fourierdlem87  46580  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem95  46588  fourierdlem103  46596  fourierdlem104  46597  etransclem48  46669  qndenserrnbllem  46681  sge0rpcpnf  46808  sge0ad2en  46818  ovnsubaddlem1  46957  hoidmvlelem3  46984  ovolval5lem1  47039  ovolval5lem2  47040  vonioolem2  47068  vonicclem2  47071  pimrecltneg  47111  smfrec  47176  smfdiv  47184  sigardiv  47248  modn0mul  47746  lighneallem2  47995  requad01  48010  requad1  48011  requad2  48012  refdivmptf  48931  fldivexpfllog2  48954  dignnld  48992  dig2nn1st  48994  dig2bits  49003  dignn0flhalflem2  49005  affinecomb1  49091  eenglngeehlnmlem1  49126  eenglngeehlnmlem2  49127  rrx2vlinest  49130  line2ylem  49140  line2  49141  line2xlem  49142  itsclc0lem1  49145  itsclc0lem2  49146  itscnhlc0yqe  49148  itsclquadb  49165