Theorem redivcld 12041

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

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2940  (class class class)co 7408  ℝcr 11108  0cc0 11109   / cdiv 11870

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871

This theorem is referenced by:  recp1lt1  12111  ledivp1  12115  supmul1  12182  rimul  12202  div4p1lem1div2  12466  divelunit  13470  fldiv4p1lem1div2  13799  fldiv4lem1div2uz2  13800  quoremz  13819  intfracq  13823  fldiv  13824  modmulnn  13853  modmuladd  13877  modmuladdnn0  13879  expnbnd  14194  discr1  14201  discr  14202  sqreulem  15305  fprodle  15939  fldivndvdslt  16356  flodddiv4t2lthalf  16358  iccpnfhmeo  24460  ipcau2  24750  mbfmulc2lem  25163  i1fmulc  25220  itg1mulc  25221  itg2monolem3  25269  dvferm2lem  25502  dvcvx  25536  radcnvlem1  25924  tanord1  26045  logf1o2  26157  relogbcl  26275  ang180lem2  26312  chordthmlem2  26335  jensenlem2  26489  regamcl  26562  gausslemma2dlem0d  26859  gausslemma2dlem3  26868  gausslemma2dlem4  26869  gausslemma2dlem5  26871  2lgslem1a2  26890  2lgslem1  26894  2lgslem2  26895  2lgsoddprmlem2  26909  selberg3lem1  27057  selberg4lem1  27060  ostth2  27137  ttgcontlem1  28139  colinearalg  28165  axsegconlem8  28179  axpaschlem  28195  axeuclidlem  28217  nmophmi  31279  unitdivcld  32876  dya2icoseg  33271  dya2iocucvr  33278  signsply0  33557  logdivsqrle  33657  hgt750lem  33658  hgt750leme  33665  tgoldbachgtde  33667  sinccvglem  34652  circum  34654  knoppndvlem1  35383  knoppndvlem14  35396  knoppndvlem15  35397  knoppndvlem17  35399  knoppndvlem18  35400  knoppndvlem19  35401  knoppndvlem21  35403  poimirlem31  36514  itg2addnclem  36534  itg2addnclem2  36535  areacirclem1  36571  areacirclem4  36574  lcmineqlem15  40903  3lexlogpow5ineq2  40915  3lexlogpow5ineq4  40916  3lexlogpow2ineq1  40918  3lexlogpow2ineq2  40919  3lexlogpow5ineq5  40920  dvrelog2  40924  dvrelog3  40925  dvrelog2b  40926  dvrelogpow2b  40928  aks4d1p1p4  40931  aks4d1p1p6  40933  aks4d1p1p7  40934  aks4d1p1p5  40935  aks4d1p5  40940  aks4d1p8  40947  2ap1caineq  40956  pellexlem1  41557  pellexlem6  41562  reglogcl  41618  modabsdifz  41715  areaquad  41955  imo72b2  42914  hashnzfzclim  43071  sineq0ALT  43688  suplesup  44039  reclt0d  44087  xrralrecnnge  44090  ltdiv23neg  44094  iooiinioc  44259  0ellimcdiv  44355  dvdivbd  44629  ioodvbdlimc1lem1  44637  ioodvbdlimc1lem2  44638  ioodvbdlimc2lem  44640  stoweidlem1  44707  stoweidlem13  44719  stoweidlem26  44732  stoweidlem34  44740  stoweidlem36  44742  stoweidlem51  44757  stoweidlem60  44766  wallispilem4  44774  wallispilem5  44775  stirlingr  44796  dirker2re  44798  dirkerval2  44800  dirkerre  44801  dirkertrigeq  44807  dirkeritg  44808  dirkercncflem1  44809  dirkercncflem4  44812  fourierdlem4  44817  fourierdlem7  44820  fourierdlem9  44822  fourierdlem16  44829  fourierdlem19  44832  fourierdlem21  44834  fourierdlem22  44835  fourierdlem24  44837  fourierdlem26  44839  fourierdlem30  44843  fourierdlem39  44852  fourierdlem41  44854  fourierdlem42  44855  fourierdlem43  44856  fourierdlem47  44859  fourierdlem48  44860  fourierdlem49  44861  fourierdlem51  44863  fourierdlem56  44868  fourierdlem57  44869  fourierdlem58  44870  fourierdlem59  44871  fourierdlem63  44875  fourierdlem64  44876  fourierdlem66  44878  fourierdlem71  44883  fourierdlem72  44884  fourierdlem78  44890  fourierdlem83  44895  fourierdlem87  44899  fourierdlem89  44901  fourierdlem90  44902  fourierdlem91  44903  fourierdlem95  44907  fourierdlem103  44915  fourierdlem104  44916  etransclem48  44988  qndenserrnbllem  45000  sge0rpcpnf  45127  sge0ad2en  45137  ovnsubaddlem1  45276  hoidmvlelem3  45303  ovolval5lem1  45358  ovolval5lem2  45359  vonioolem2  45387  vonicclem2  45390  pimrecltneg  45430  smfrec  45495  smfdiv  45503  sigardiv  45567  lighneallem2  46264  requad01  46279  requad1  46280  requad2  46281  modn0mul  47196  refdivmptf  47218  fldivexpfllog2  47241  dignnld  47279  dig2nn1st  47281  dig2bits  47290  dignn0flhalflem2  47292  affinecomb1  47378  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  rrx2vlinest  47417  line2ylem  47427  line2  47428  line2xlem  47429  itsclc0lem1  47432  itsclc0lem2  47433  itscnhlc0yqe  47435  itsclquadb  47452