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 2932  (class class class)co 7367  ℝcr 11037  0cc0 11038   / cdiv 11807

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808

This theorem is referenced by:  recp1lt1  12054  ledivp1  12058  supmul1  12125  rimul  12150  div4p1lem1div2  12432  divelunit  13447  fldiv4p1lem1div2  13794  fldiv4lem1div2uz2  13795  quoremz  13814  intfracq  13818  fldiv  13819  modmulnn  13848  modmuladd  13875  modmuladdnn0  13877  expnbnd  14194  discr1  14201  discr  14202  sqreulem  15322  fprodle  15961  fldivndvdslt  16385  flodddiv4t2lthalf  16387  iccpnfhmeo  24912  ipcau2  25201  mbfmulc2lem  25614  i1fmulc  25670  itg1mulc  25671  itg2monolem3  25719  dvferm2lem  25953  dvcvx  25987  radcnvlem1  26378  tanord1  26501  logf1o2  26614  relogbcl  26737  ang180lem2  26774  chordthmlem2  26797  jensenlem2  26951  regamcl  27024  gausslemma2dlem0d  27322  gausslemma2dlem3  27331  gausslemma2dlem4  27332  gausslemma2dlem5  27334  2lgslem1a2  27353  2lgslem1  27357  2lgslem2  27358  2lgsoddprmlem2  27372  selberg3lem1  27520  selberg4lem1  27523  ostth2  27600  ttgcontlem1  28953  colinearalg  28979  axsegconlem8  28993  axpaschlem  29009  axeuclidlem  29031  nmophmi  32102  cos9thpinconstrlem1  33933  unitdivcld  34045  dya2icoseg  34421  dya2iocucvr  34428  signsply0  34695  logdivsqrle  34794  hgt750lem  34795  hgt750leme  34802  tgoldbachgtde  34804  sinccvglem  35854  circum  35856  knoppndvlem1  36772  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem19  36790  knoppndvlem21  36792  poimirlem31  37972  itg2addnclem  37992  itg2addnclem2  37993  areacirclem1  38029  areacirclem4  38032  lcmineqlem15  42482  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  dvrelog2  42503  dvrelog3  42504  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p5  42519  aks4d1p8  42526  aks6d1c2lem4  42566  2ap1caineq  42584  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  pellexlem1  43257  pellexlem6  43262  reglogcl  43318  modabsdifz  43414  areaquad  43644  imo72b2  44599  hashnzfzclim  44749  sineq0ALT  45363  suplesup  45769  reclt0d  45816  xrralrecnnge  45819  ltdiv23neg  45823  iooiinioc  45986  0ellimcdiv  46077  dvdivbd  46351  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem1  46429  stoweidlem13  46441  stoweidlem26  46454  stoweidlem34  46462  stoweidlem36  46464  stoweidlem51  46479  stoweidlem60  46488  wallispilem4  46496  wallispilem5  46497  stirlingr  46518  dirker2re  46520  dirkerval2  46522  dirkerre  46523  dirkertrigeq  46529  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem7  46542  fourierdlem9  46544  fourierdlem16  46551  fourierdlem19  46554  fourierdlem21  46556  fourierdlem22  46557  fourierdlem24  46559  fourierdlem26  46561  fourierdlem30  46565  fourierdlem39  46574  fourierdlem41  46576  fourierdlem42  46577  fourierdlem43  46578  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem63  46597  fourierdlem64  46598  fourierdlem66  46600  fourierdlem71  46605  fourierdlem72  46606  fourierdlem78  46612  fourierdlem83  46617  fourierdlem87  46621  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem95  46629  fourierdlem103  46637  fourierdlem104  46638  etransclem48  46710  qndenserrnbllem  46722  sge0rpcpnf  46849  sge0ad2en  46859  ovnsubaddlem1  46998  hoidmvlelem3  47025  ovolval5lem1  47080  ovolval5lem2  47081  vonioolem2  47109  vonicclem2  47112  pimrecltneg  47152  smfrec  47217  smfdiv  47225  sigardiv  47289  modn0mul  47811  lighneallem2  48069  requad01  48097  requad1  48098  requad2  48099  refdivmptf  49018  fldivexpfllog2  49041  dignnld  49079  dig2nn1st  49081  dig2bits  49090  dignn0flhalflem2  49092  affinecomb1  49178  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2vlinest  49217  line2ylem  49227  line2  49228  line2xlem  49229  itsclc0lem1  49232  itsclc0lem2  49233  itscnhlc0yqe  49235  itsclquadb  49252