Theorem redivcld 12017

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2926  (class class class)co 7390  ℝcr 11074  0cc0 11075   / cdiv 11842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843

This theorem is referenced by:  recp1lt1  12088  ledivp1  12092  supmul1  12159  rimul  12184  div4p1lem1div2  12444  divelunit  13462  fldiv4p1lem1div2  13804  fldiv4lem1div2uz2  13805  quoremz  13824  intfracq  13828  fldiv  13829  modmulnn  13858  modmuladd  13885  modmuladdnn0  13887  expnbnd  14204  discr1  14211  discr  14212  sqreulem  15333  fprodle  15969  fldivndvdslt  16393  flodddiv4t2lthalf  16395  iccpnfhmeo  24850  ipcau2  25141  mbfmulc2lem  25555  i1fmulc  25611  itg1mulc  25612  itg2monolem3  25660  dvferm2lem  25897  dvcvx  25932  radcnvlem1  26329  tanord1  26453  logf1o2  26566  relogbcl  26690  ang180lem2  26727  chordthmlem2  26750  jensenlem2  26905  regamcl  26978  gausslemma2dlem0d  27277  gausslemma2dlem3  27286  gausslemma2dlem4  27287  gausslemma2dlem5  27289  2lgslem1a2  27308  2lgslem1  27312  2lgslem2  27313  2lgsoddprmlem2  27327  selberg3lem1  27475  selberg4lem1  27478  ostth2  27555  ttgcontlem1  28819  colinearalg  28844  axsegconlem8  28858  axpaschlem  28874  axeuclidlem  28896  nmophmi  31967  cos9thpinconstrlem1  33786  unitdivcld  33898  dya2icoseg  34275  dya2iocucvr  34282  signsply0  34549  logdivsqrle  34648  hgt750lem  34649  hgt750leme  34656  tgoldbachgtde  34658  sinccvglem  35666  circum  35668  knoppndvlem1  36507  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem19  36525  knoppndvlem21  36527  poimirlem31  37652  itg2addnclem  37672  itg2addnclem2  37673  areacirclem1  37709  areacirclem4  37712  lcmineqlem15  42038  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  dvrelog2  42059  dvrelog3  42060  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p5  42075  aks4d1p8  42082  aks6d1c2lem4  42122  2ap1caineq  42140  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  pellexlem1  42824  pellexlem6  42829  reglogcl  42885  modabsdifz  42982  areaquad  43212  imo72b2  44168  hashnzfzclim  44318  sineq0ALT  44933  suplesup  45342  reclt0d  45390  xrralrecnnge  45393  ltdiv23neg  45397  iooiinioc  45561  0ellimcdiv  45654  dvdivbd  45928  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem1  46006  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  stoweidlem36  46041  stoweidlem51  46056  stoweidlem60  46065  wallispilem4  46073  wallispilem5  46074  stirlingr  46095  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkertrigeq  46106  dirkeritg  46107  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem4  46116  fourierdlem7  46119  fourierdlem9  46121  fourierdlem16  46128  fourierdlem19  46131  fourierdlem21  46133  fourierdlem22  46134  fourierdlem24  46136  fourierdlem26  46138  fourierdlem30  46142  fourierdlem39  46151  fourierdlem41  46153  fourierdlem42  46154  fourierdlem43  46155  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem63  46174  fourierdlem64  46175  fourierdlem66  46177  fourierdlem71  46182  fourierdlem72  46183  fourierdlem78  46189  fourierdlem83  46194  fourierdlem87  46198  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  etransclem48  46287  qndenserrnbllem  46299  sge0rpcpnf  46426  sge0ad2en  46436  ovnsubaddlem1  46575  hoidmvlelem3  46602  ovolval5lem1  46657  ovolval5lem2  46658  vonioolem2  46686  vonicclem2  46689  pimrecltneg  46729  smfrec  46794  smfdiv  46802  sigardiv  46866  modn0mul  47362  lighneallem2  47611  requad01  47626  requad1  47627  requad2  47628  refdivmptf  48535  fldivexpfllog2  48558  dignnld  48596  dig2nn1st  48598  dig2bits  48607  dignn0flhalflem2  48609  affinecomb1  48695  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2vlinest  48734  line2ylem  48744  line2  48745  line2xlem  48746  itsclc0lem1  48749  itsclc0lem2  48750  itscnhlc0yqe  48752  itsclquadb  48769