Theorem redivcld 11952

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  (class class class)co 7349  ℝcr 11008  0cc0 11009   / cdiv 11777

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778

This theorem is referenced by:  recp1lt1  12023  ledivp1  12027  supmul1  12094  rimul  12119  div4p1lem1div2  12379  divelunit  13397  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  quoremz  13759  intfracq  13763  fldiv  13764  modmulnn  13793  modmuladd  13820  modmuladdnn0  13822  expnbnd  14139  discr1  14146  discr  14147  sqreulem  15267  fprodle  15903  fldivndvdslt  16327  flodddiv4t2lthalf  16329  iccpnfhmeo  24841  ipcau2  25132  mbfmulc2lem  25546  i1fmulc  25602  itg1mulc  25603  itg2monolem3  25651  dvferm2lem  25888  dvcvx  25923  radcnvlem1  26320  tanord1  26444  logf1o2  26557  relogbcl  26681  ang180lem2  26718  chordthmlem2  26741  jensenlem2  26896  regamcl  26969  gausslemma2dlem0d  27268  gausslemma2dlem3  27277  gausslemma2dlem4  27278  gausslemma2dlem5  27280  2lgslem1a2  27299  2lgslem1  27303  2lgslem2  27304  2lgsoddprmlem2  27318  selberg3lem1  27466  selberg4lem1  27469  ostth2  27546  ttgcontlem1  28834  colinearalg  28859  axsegconlem8  28873  axpaschlem  28889  axeuclidlem  28911  nmophmi  31979  cos9thpinconstrlem1  33772  unitdivcld  33884  dya2icoseg  34261  dya2iocucvr  34268  signsply0  34535  logdivsqrle  34634  hgt750lem  34635  hgt750leme  34642  tgoldbachgtde  34644  sinccvglem  35665  circum  35667  knoppndvlem1  36506  knoppndvlem14  36519  knoppndvlem15  36520  knoppndvlem17  36522  knoppndvlem18  36523  knoppndvlem19  36524  knoppndvlem21  36526  poimirlem31  37651  itg2addnclem  37671  itg2addnclem2  37672  areacirclem1  37708  areacirclem4  37711  lcmineqlem15  42036  3lexlogpow5ineq2  42048  3lexlogpow5ineq4  42049  3lexlogpow2ineq1  42051  3lexlogpow2ineq2  42052  3lexlogpow5ineq5  42053  dvrelog2  42057  dvrelog3  42058  dvrelog2b  42059  dvrelogpow2b  42061  aks4d1p1p4  42064  aks4d1p1p6  42066  aks4d1p1p7  42067  aks4d1p1p5  42068  aks4d1p5  42073  aks4d1p8  42080  aks6d1c2lem4  42120  2ap1caineq  42138  bcled  42171  bcle2d  42172  aks6d1c7lem1  42173  pellexlem1  42822  pellexlem6  42827  reglogcl  42883  modabsdifz  42979  areaquad  43209  imo72b2  44165  hashnzfzclim  44315  sineq0ALT  44930  suplesup  45339  reclt0d  45386  xrralrecnnge  45389  ltdiv23neg  45393  iooiinioc  45557  0ellimcdiv  45650  dvdivbd  45924  ioodvbdlimc1lem1  45932  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  stoweidlem1  46002  stoweidlem13  46014  stoweidlem26  46027  stoweidlem34  46035  stoweidlem36  46037  stoweidlem51  46052  stoweidlem60  46061  wallispilem4  46069  wallispilem5  46070  stirlingr  46091  dirker2re  46093  dirkerval2  46095  dirkerre  46096  dirkertrigeq  46102  dirkeritg  46103  dirkercncflem1  46104  dirkercncflem4  46107  fourierdlem4  46112  fourierdlem7  46115  fourierdlem9  46117  fourierdlem16  46124  fourierdlem19  46127  fourierdlem21  46129  fourierdlem22  46130  fourierdlem24  46132  fourierdlem26  46134  fourierdlem30  46138  fourierdlem39  46147  fourierdlem41  46149  fourierdlem42  46150  fourierdlem43  46151  fourierdlem47  46154  fourierdlem48  46155  fourierdlem49  46156  fourierdlem51  46158  fourierdlem56  46163  fourierdlem57  46164  fourierdlem58  46165  fourierdlem59  46166  fourierdlem63  46170  fourierdlem64  46171  fourierdlem66  46173  fourierdlem71  46178  fourierdlem72  46179  fourierdlem78  46185  fourierdlem83  46190  fourierdlem87  46194  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem95  46202  fourierdlem103  46210  fourierdlem104  46211  etransclem48  46283  qndenserrnbllem  46295  sge0rpcpnf  46422  sge0ad2en  46432  ovnsubaddlem1  46571  hoidmvlelem3  46598  ovolval5lem1  46653  ovolval5lem2  46654  vonioolem2  46682  vonicclem2  46685  pimrecltneg  46725  smfrec  46790  smfdiv  46798  sigardiv  46862  modn0mul  47361  lighneallem2  47610  requad01  47625  requad1  47626  requad2  47627  refdivmptf  48547  fldivexpfllog2  48570  dignnld  48608  dig2nn1st  48610  dig2bits  48619  dignn0flhalflem2  48621  affinecomb1  48707  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  rrx2vlinest  48746  line2ylem  48756  line2  48757  line2xlem  48758  itsclc0lem1  48761  itsclc0lem2  48762  itscnhlc0yqe  48764  itsclquadb  48781