Theorem redivcld 12021

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

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2959  (class class class)co 7398  ℝcr 11074  0cc0 11075   / cdiv 11846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847

This theorem is referenced by:  recp1lt1  12092  ledivp1  12096  supmul1  12163  rimul  12188  div4p1lem1div2  12478  divelunit  13500  fldiv4p1lem1div2  13847  fldiv4lem1div2uz2  13848  quoremz  13867  intfracq  13871  fldiv  13872  modmulnn  13901  modmuladd  13928  modmuladdnn0  13930  expnbnd  14247  discr1  14254  discr  14255  sqreulem  15389  fprodle  16028  fldivndvdslt  16452  flodddiv4t2lthalf  16454  iccpnfhmeo  25009  ipcau2  25298  mbfmulc2lem  25711  i1fmulc  25767  itg1mulc  25768  itg2monolem3  25816  dvferm2lem  26050  dvcvx  26084  radcnvlem1  26478  tanord1  26604  logf1o2  26717  relogbcl  26840  ang180lem2  26877  chordthmlem2  26900  jensenlem2  27054  regamcl  27127  gausslemma2dlem0d  27425  gausslemma2dlem3  27434  gausslemma2dlem4  27435  gausslemma2dlem5  27437  2lgslem1a2  27456  2lgslem1  27460  2lgslem2  27461  2lgsoddprmlem2  27475  selberg3lem1  27623  selberg4lem1  27626  ostth2  27703  ttgcontlem1  29087  colinearalg  29113  axsegconlem8  29127  axpaschlem  29143  axeuclidlem  29165  nmophmi  32236  cos9thpinconstrlem1  34088  unitdivcld  34200  dya2icoseg  34576  dya2iocucvr  34583  signsply0  34847  logdivsqrle  34946  hgt750lem  34947  hgt750leme  34954  tgoldbachgtde  34956  sinccvglem  36027  circum  36029  knoppndvlem1  36955  knoppndvlem14  36968  knoppndvlem15  36969  knoppndvlem17  36971  knoppndvlem18  36972  knoppndvlem19  36973  knoppndvlem21  36975  poimirlem31  38155  itg2addnclem  38175  itg2addnclem2  38176  areacirclem1  38212  areacirclem4  38215  lcmineqlem15  42665  3lexlogpow5ineq2  42677  3lexlogpow5ineq4  42678  3lexlogpow2ineq1  42680  3lexlogpow2ineq2  42681  3lexlogpow5ineq5  42682  dvrelog2  42686  dvrelog3  42687  dvrelog2b  42688  dvrelogpow2b  42690  aks4d1p1p4  42693  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p1p5  42697  aks4d1p5  42702  aks4d1p8  42709  aks6d1c2lem4  42749  2ap1caineq  42767  bcled  42800  bcle2d  42801  aks6d1c7lem1  42802  pellexlem1  43411  pellexlem6  43416  reglogcl  43472  modabsdifz  43568  areaquad  43798  imo72b2  44753  hashnzfzclim  44903  sineq0ALT  45517  suplesup  45920  reclt0d  45967  xrralrecnnge  45970  ltdiv23neg  45974  iooiinioc  46137  0ellimcdiv  46228  dvdivbd  46502  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweidlem1  46580  stoweidlem13  46592  stoweidlem26  46605  stoweidlem34  46613  stoweidlem36  46615  stoweidlem51  46630  stoweidlem60  46639  wallispilem4  46647  wallispilem5  46648  stirlingr  46669  dirker2re  46671  dirkerval2  46673  dirkerre  46674  dirkertrigeq  46680  dirkeritg  46681  dirkercncflem1  46682  dirkercncflem4  46685  fourierdlem4  46690  fourierdlem7  46693  fourierdlem9  46695  fourierdlem16  46702  fourierdlem19  46705  fourierdlem21  46707  fourierdlem22  46708  fourierdlem24  46710  fourierdlem26  46712  fourierdlem30  46716  fourierdlem39  46725  fourierdlem41  46727  fourierdlem42  46728  fourierdlem43  46729  fourierdlem47  46732  fourierdlem48  46733  fourierdlem49  46734  fourierdlem51  46736  fourierdlem56  46741  fourierdlem57  46742  fourierdlem58  46743  fourierdlem59  46744  fourierdlem63  46748  fourierdlem64  46749  fourierdlem66  46751  fourierdlem71  46756  fourierdlem72  46757  fourierdlem78  46763  fourierdlem83  46768  fourierdlem87  46772  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fourierdlem95  46780  fourierdlem103  46788  fourierdlem104  46789  etransclem48  46861  qndenserrnbllem  46873  sge0rpcpnf  47000  sge0ad2en  47010  ovnsubaddlem1  47149  hoidmvlelem3  47176  ovolval5lem1  47231  ovolval5lem2  47232  vonioolem2  47260  vonicclem2  47263  pimrecltneg  47303  smfrec  47368  smfdiv  47376  sigardiv  47440  modn0mul  47962  lighneallem2  48220  requad01  48248  requad1  48249  requad2  48250  refdivmptf  49169  fldivexpfllog2  49192  dignnld  49230  dig2nn1st  49232  dig2bits  49241  dignn0flhalflem2  49243  affinecomb1  49329  eenglngeehlnmlem1  49364  eenglngeehlnmlem2  49365  rrx2vlinest  49368  line2ylem  49378  line2  49379  line2xlem  49380  itsclc0lem1  49383  itsclc0lem2  49384  itscnhlc0yqe  49386  itsclquadb  49403