Theorem redivcld 11801

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

Syntax hints:   → wi 4   ∈ wcel 2110   ≠ wne 2945  (class class class)co 7269  ℝcr 10869  0cc0 10870   / cdiv 11630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-resscn 10927  ax-1cn 10928  ax-icn 10929  ax-addcl 10930  ax-addrcl 10931  ax-mulcl 10932  ax-mulrcl 10933  ax-mulcom 10934  ax-addass 10935  ax-mulass 10936  ax-distr 10937  ax-i2m1 10938  ax-1ne0 10939  ax-1rid 10940  ax-rnegex 10941  ax-rrecex 10942  ax-cnre 10943  ax-pre-lttri 10944  ax-pre-lttrn 10945  ax-pre-ltadd 10946  ax-pre-mulgt0 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-er 8479  df-en 8715  df-dom 8716  df-sdom 8717  df-pnf 11010  df-mnf 11011  df-xr 11012  df-ltxr 11013  df-le 11014  df-sub 11205  df-neg 11206  df-div 11631

This theorem is referenced by:  recp1lt1  11871  ledivp1  11875  supmul1  11942  rimul  11962  div4p1lem1div2  12226  divelunit  13223  fldiv4p1lem1div2  13551  fldiv4lem1div2uz2  13552  quoremz  13571  intfracq  13575  fldiv  13576  modmulnn  13605  modmuladd  13629  modmuladdnn0  13631  expnbnd  13943  discr1  13950  discr  13951  sqreulem  15067  fprodle  15702  fldivndvdslt  16119  flodddiv4t2lthalf  16121  iccpnfhmeo  24104  ipcau2  24394  mbfmulc2lem  24807  i1fmulc  24864  itg1mulc  24865  itg2monolem3  24913  dvferm2lem  25146  dvcvx  25180  radcnvlem1  25568  tanord1  25689  logf1o2  25801  relogbcl  25919  ang180lem2  25956  chordthmlem2  25979  jensenlem2  26133  regamcl  26206  gausslemma2dlem0d  26503  gausslemma2dlem3  26512  gausslemma2dlem4  26513  gausslemma2dlem5  26515  2lgslem1a2  26534  2lgslem1  26538  2lgslem2  26539  2lgsoddprmlem2  26553  selberg3lem1  26701  selberg4lem1  26704  ostth2  26781  ttgcontlem1  27248  colinearalg  27274  axsegconlem8  27288  axpaschlem  27304  axeuclidlem  27326  nmophmi  30387  unitdivcld  31845  dya2icoseg  32238  dya2iocucvr  32245  signsply0  32524  logdivsqrle  32624  hgt750lem  32625  hgt750leme  32632  tgoldbachgtde  32634  sinccvglem  33624  circum  33626  knoppndvlem1  34686  knoppndvlem14  34699  knoppndvlem15  34700  knoppndvlem17  34702  knoppndvlem18  34703  knoppndvlem19  34704  knoppndvlem21  34706  poimirlem31  35802  itg2addnclem  35822  itg2addnclem2  35823  areacirclem1  35859  areacirclem4  35862  lcmineqlem15  40046  3lexlogpow5ineq2  40058  3lexlogpow5ineq4  40059  3lexlogpow2ineq1  40061  3lexlogpow2ineq2  40062  3lexlogpow5ineq5  40063  dvrelog2  40067  dvrelog3  40068  dvrelog2b  40069  dvrelogpow2b  40071  aks4d1p1p4  40074  aks4d1p1p6  40076  aks4d1p1p7  40077  aks4d1p1p5  40078  aks4d1p5  40083  aks4d1p8  40090  2ap1caineq  40096  pellexlem1  40646  pellexlem6  40651  reglogcl  40707  modabsdifz  40803  areaquad  41042  imo72b2  41751  hashnzfzclim  41908  sineq0ALT  42525  suplesup  42847  reclt0d  42895  xrralrecnnge  42899  ltdiv23neg  42903  iooiinioc  43063  0ellimcdiv  43159  dvdivbd  43433  ioodvbdlimc1lem1  43441  ioodvbdlimc1lem2  43442  ioodvbdlimc2lem  43444  stoweidlem1  43511  stoweidlem13  43523  stoweidlem26  43536  stoweidlem34  43544  stoweidlem36  43546  stoweidlem51  43561  stoweidlem60  43570  wallispilem4  43578  wallispilem5  43579  stirlingr  43600  dirker2re  43602  dirkerval2  43604  dirkerre  43605  dirkertrigeq  43611  dirkeritg  43612  dirkercncflem1  43613  dirkercncflem4  43616  fourierdlem4  43621  fourierdlem7  43624  fourierdlem9  43626  fourierdlem16  43633  fourierdlem19  43636  fourierdlem21  43638  fourierdlem22  43639  fourierdlem24  43641  fourierdlem26  43643  fourierdlem30  43647  fourierdlem39  43656  fourierdlem41  43658  fourierdlem42  43659  fourierdlem43  43660  fourierdlem47  43663  fourierdlem48  43664  fourierdlem49  43665  fourierdlem51  43667  fourierdlem56  43672  fourierdlem57  43673  fourierdlem58  43674  fourierdlem59  43675  fourierdlem63  43679  fourierdlem64  43680  fourierdlem66  43682  fourierdlem71  43687  fourierdlem72  43688  fourierdlem78  43694  fourierdlem83  43699  fourierdlem87  43703  fourierdlem89  43705  fourierdlem90  43706  fourierdlem91  43707  fourierdlem95  43711  fourierdlem103  43719  fourierdlem104  43720  etransclem48  43792  qndenserrnbllem  43804  sge0rpcpnf  43928  sge0ad2en  43938  ovnsubaddlem1  44077  hoidmvlelem3  44104  ovolval5lem1  44159  ovolval5lem2  44160  vonioolem2  44188  vonicclem2  44191  pimrecltneg  44226  smfrec  44289  smfdiv  44297  sigardiv  44343  lighneallem2  45025  requad01  45040  requad1  45041  requad2  45042  modn0mul  45833  refdivmptf  45855  fldivexpfllog2  45878  dignnld  45916  dig2nn1st  45918  dig2bits  45927  dignn0flhalflem2  45929  affinecomb1  46015  eenglngeehlnmlem1  46050  eenglngeehlnmlem2  46051  rrx2vlinest  46054  line2ylem  46064  line2  46065  line2xlem  46066  itsclc0lem1  46069  itsclc0lem2  46070  itscnhlc0yqe  46072  itsclquadb  46089