Theorem redivcld 11970

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7358  ℝcr 11026  0cc0 11027   / cdiv 11795

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-sub 11367  df-neg 11368  df-div 11796

This theorem is referenced by:  recp1lt1  12041  ledivp1  12045  supmul1  12112  rimul  12137  div4p1lem1div2  12397  divelunit  13411  fldiv4p1lem1div2  13756  fldiv4lem1div2uz2  13757  quoremz  13776  intfracq  13780  fldiv  13781  modmulnn  13810  modmuladd  13837  modmuladdnn0  13839  expnbnd  14156  discr1  14163  discr  14164  sqreulem  15284  fprodle  15920  fldivndvdslt  16344  flodddiv4t2lthalf  16346  iccpnfhmeo  24890  ipcau2  25179  mbfmulc2lem  25592  i1fmulc  25648  itg1mulc  25649  itg2monolem3  25697  dvferm2lem  25931  dvcvx  25966  radcnvlem1  26362  tanord1  26486  logf1o2  26599  relogbcl  26723  ang180lem2  26760  chordthmlem2  26783  jensenlem2  26938  regamcl  27011  gausslemma2dlem0d  27310  gausslemma2dlem3  27319  gausslemma2dlem4  27320  gausslemma2dlem5  27322  2lgslem1a2  27341  2lgslem1  27345  2lgslem2  27346  2lgsoddprmlem2  27360  selberg3lem1  27508  selberg4lem1  27511  ostth2  27588  ttgcontlem1  28941  colinearalg  28967  axsegconlem8  28981  axpaschlem  28997  axeuclidlem  29019  nmophmi  32091  cos9thpinconstrlem1  33939  unitdivcld  34051  dya2icoseg  34427  dya2iocucvr  34434  signsply0  34701  logdivsqrle  34800  hgt750lem  34801  hgt750leme  34808  tgoldbachgtde  34810  sinccvglem  35860  circum  35862  knoppndvlem1  36770  knoppndvlem14  36783  knoppndvlem15  36784  knoppndvlem17  36786  knoppndvlem18  36787  knoppndvlem19  36788  knoppndvlem21  36790  poimirlem31  37963  itg2addnclem  37983  itg2addnclem2  37984  areacirclem1  38020  areacirclem4  38023  lcmineqlem15  42474  3lexlogpow5ineq2  42486  3lexlogpow5ineq4  42487  3lexlogpow2ineq1  42489  3lexlogpow2ineq2  42490  3lexlogpow5ineq5  42491  dvrelog2  42495  dvrelog3  42496  dvrelog2b  42497  dvrelogpow2b  42499  aks4d1p1p4  42502  aks4d1p1p6  42504  aks4d1p1p7  42505  aks4d1p1p5  42506  aks4d1p5  42511  aks4d1p8  42518  aks6d1c2lem4  42558  2ap1caineq  42576  bcled  42609  bcle2d  42610  aks6d1c7lem1  42611  pellexlem1  43260  pellexlem6  43265  reglogcl  43321  modabsdifz  43417  areaquad  43647  imo72b2  44602  hashnzfzclim  44752  sineq0ALT  45366  suplesup  45772  reclt0d  45819  xrralrecnnge  45822  ltdiv23neg  45826  iooiinioc  45990  0ellimcdiv  46081  dvdivbd  46355  ioodvbdlimc1lem1  46363  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  stoweidlem1  46433  stoweidlem13  46445  stoweidlem26  46458  stoweidlem34  46466  stoweidlem36  46468  stoweidlem51  46483  stoweidlem60  46492  wallispilem4  46500  wallispilem5  46501  stirlingr  46522  dirker2re  46524  dirkerval2  46526  dirkerre  46527  dirkertrigeq  46533  dirkeritg  46534  dirkercncflem1  46535  dirkercncflem4  46538  fourierdlem4  46543  fourierdlem7  46546  fourierdlem9  46548  fourierdlem16  46555  fourierdlem19  46558  fourierdlem21  46560  fourierdlem22  46561  fourierdlem24  46563  fourierdlem26  46565  fourierdlem30  46569  fourierdlem39  46578  fourierdlem41  46580  fourierdlem42  46581  fourierdlem43  46582  fourierdlem47  46585  fourierdlem48  46586  fourierdlem49  46587  fourierdlem51  46589  fourierdlem56  46594  fourierdlem57  46595  fourierdlem58  46596  fourierdlem59  46597  fourierdlem63  46601  fourierdlem64  46602  fourierdlem66  46604  fourierdlem71  46609  fourierdlem72  46610  fourierdlem78  46616  fourierdlem83  46621  fourierdlem87  46625  fourierdlem89  46627  fourierdlem90  46628  fourierdlem91  46629  fourierdlem95  46633  fourierdlem103  46641  fourierdlem104  46642  etransclem48  46714  qndenserrnbllem  46726  sge0rpcpnf  46853  sge0ad2en  46863  ovnsubaddlem1  47002  hoidmvlelem3  47029  ovolval5lem1  47084  ovolval5lem2  47085  vonioolem2  47113  vonicclem2  47116  pimrecltneg  47156  smfrec  47221  smfdiv  47229  sigardiv  47293  modn0mul  47791  lighneallem2  48040  requad01  48055  requad1  48056  requad2  48057  refdivmptf  48976  fldivexpfllog2  48999  dignnld  49037  dig2nn1st  49039  dig2bits  49048  dignn0flhalflem2  49050  affinecomb1  49136  eenglngeehlnmlem1  49171  eenglngeehlnmlem2  49172  rrx2vlinest  49175  line2ylem  49185  line2  49186  line2xlem  49187  itsclc0lem1  49190  itsclc0lem2  49191  itscnhlc0yqe  49193  itsclquadb  49210