Theorem redivcld 11812

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2944  (class class class)co 7284  ℝcr 10879  0cc0 10880   / cdiv 11641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642

This theorem is referenced by:  recp1lt1  11882  ledivp1  11886  supmul1  11953  rimul  11973  div4p1lem1div2  12237  divelunit  13235  fldiv4p1lem1div2  13564  fldiv4lem1div2uz2  13565  quoremz  13584  intfracq  13588  fldiv  13589  modmulnn  13618  modmuladd  13642  modmuladdnn0  13644  expnbnd  13956  discr1  13963  discr  13964  sqreulem  15080  fprodle  15715  fldivndvdslt  16132  flodddiv4t2lthalf  16134  iccpnfhmeo  24117  ipcau2  24407  mbfmulc2lem  24820  i1fmulc  24877  itg1mulc  24878  itg2monolem3  24926  dvferm2lem  25159  dvcvx  25193  radcnvlem1  25581  tanord1  25702  logf1o2  25814  relogbcl  25932  ang180lem2  25969  chordthmlem2  25992  jensenlem2  26146  regamcl  26219  gausslemma2dlem0d  26516  gausslemma2dlem3  26525  gausslemma2dlem4  26526  gausslemma2dlem5  26528  2lgslem1a2  26547  2lgslem1  26551  2lgslem2  26552  2lgsoddprmlem2  26566  selberg3lem1  26714  selberg4lem1  26717  ostth2  26794  ttgcontlem1  27261  colinearalg  27287  axsegconlem8  27301  axpaschlem  27317  axeuclidlem  27339  nmophmi  30402  unitdivcld  31860  dya2icoseg  32253  dya2iocucvr  32260  signsply0  32539  logdivsqrle  32639  hgt750lem  32640  hgt750leme  32647  tgoldbachgtde  32649  sinccvglem  33639  circum  33641  knoppndvlem1  34701  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem19  34719  knoppndvlem21  34721  poimirlem31  35817  itg2addnclem  35837  itg2addnclem2  35838  areacirclem1  35874  areacirclem4  35877  lcmineqlem15  40058  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow2ineq1  40073  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  dvrelog2  40079  dvrelog3  40080  dvrelog2b  40081  dvrelogpow2b  40083  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p5  40095  aks4d1p8  40102  2ap1caineq  40108  pellexlem1  40658  pellexlem6  40663  reglogcl  40719  modabsdifz  40815  areaquad  41054  imo72b2  41790  hashnzfzclim  41947  sineq0ALT  42564  suplesup  42885  reclt0d  42933  xrralrecnnge  42937  ltdiv23neg  42941  iooiinioc  43101  0ellimcdiv  43197  dvdivbd  43471  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem1  43549  stoweidlem13  43561  stoweidlem26  43574  stoweidlem34  43582  stoweidlem36  43584  stoweidlem51  43599  stoweidlem60  43608  wallispilem4  43616  wallispilem5  43617  stirlingr  43638  dirker2re  43640  dirkerval2  43642  dirkerre  43643  dirkertrigeq  43649  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem4  43659  fourierdlem7  43662  fourierdlem9  43664  fourierdlem16  43671  fourierdlem19  43674  fourierdlem21  43676  fourierdlem22  43677  fourierdlem24  43679  fourierdlem26  43681  fourierdlem30  43685  fourierdlem39  43694  fourierdlem41  43696  fourierdlem42  43697  fourierdlem43  43698  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem51  43705  fourierdlem56  43710  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem63  43717  fourierdlem64  43718  fourierdlem66  43720  fourierdlem71  43725  fourierdlem72  43726  fourierdlem78  43732  fourierdlem83  43737  fourierdlem87  43741  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem95  43749  fourierdlem103  43757  fourierdlem104  43758  etransclem48  43830  qndenserrnbllem  43842  sge0rpcpnf  43966  sge0ad2en  43976  ovnsubaddlem1  44115  hoidmvlelem3  44142  ovolval5lem1  44197  ovolval5lem2  44198  vonioolem2  44226  vonicclem2  44229  pimrecltneg  44269  smfrec  44334  smfdiv  44342  sigardiv  44388  lighneallem2  45069  requad01  45084  requad1  45085  requad2  45086  modn0mul  45877  refdivmptf  45899  fldivexpfllog2  45922  dignnld  45960  dig2nn1st  45962  dig2bits  45971  dignn0flhalflem2  45973  affinecomb1  46059  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2vlinest  46098  line2ylem  46108  line2  46109  line2xlem  46110  itsclc0lem1  46113  itsclc0lem2  46114  itscnhlc0yqe  46116  itsclquadb  46133