Theorem redivcld 12043

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  (class class class)co 7411  ℝcr 11099  0cc0 11100   / cdiv 11871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872

This theorem is referenced by:  recp1lt1  12113  ledivp1  12117  supmul1  12184  rimul  12209  div4p1lem1div2  12499  divelunit  13521  fldiv4p1lem1div2  13868  fldiv4lem1div2uz2  13869  quoremz  13888  intfracq  13892  fldiv  13893  modmulnn  13922  modmuladd  13949  modmuladdnn0  13951  expnbnd  14268  discr1  14275  discr  14276  sqreulem  15411  fprodle  16050  fldivndvdslt  16474  flodddiv4t2lthalf  16476  iccpnfhmeo  25073  ipcau2  25362  mbfmulc2lem  25775  i1fmulc  25831  itg1mulc  25832  itg2monolem3  25880  dvferm2lem  26114  dvcvx  26148  radcnvlem1  26542  tanord1  26668  logf1o2  26781  relogbcl  26904  ang180lem2  26941  chordthmlem2  26964  jensenlem2  27118  regamcl  27191  gausslemma2dlem0d  27489  gausslemma2dlem3  27498  gausslemma2dlem4  27499  gausslemma2dlem5  27501  2lgslem1a2  27520  2lgslem1  27524  2lgslem2  27525  2lgsoddprmlem2  27539  selberg3lem1  27687  selberg4lem1  27690  ostth2  27767  ttgcontlem1  29175  colinearalg  29201  axsegconlem8  29215  axpaschlem  29231  axeuclidlem  29253  nmophmi  32324  cos9thpinconstrlem1  34124  unitdivcld  34236  dya2icoseg  34612  dya2iocucvr  34619  signsply0  34883  logdivsqrle  34982  hgt750lem  34983  hgt750leme  34990  tgoldbachgtde  34992  sinccvglem  36097  circum  36099  knoppndvlem1  37024  knoppndvlem14  37037  knoppndvlem15  37038  knoppndvlem17  37040  knoppndvlem18  37041  knoppndvlem19  37042  knoppndvlem21  37044  poimirlem31  38225  itg2addnclem  38245  itg2addnclem2  38246  areacirclem1  38282  areacirclem4  38285  lcmineqlem15  42735  3lexlogpow5ineq2  42747  3lexlogpow5ineq4  42748  3lexlogpow2ineq1  42750  3lexlogpow2ineq2  42751  3lexlogpow5ineq5  42752  dvrelog2  42756  dvrelog3  42757  dvrelog2b  42758  dvrelogpow2b  42760  aks4d1p1p4  42763  aks4d1p1p6  42765  aks4d1p1p7  42766  aks4d1p1p5  42767  aks4d1p5  42772  aks4d1p8  42779  aks6d1c2lem4  42819  2ap1caineq  42837  bcled  42870  bcle2d  42871  aks6d1c7lem1  42872  pellexlem1  43483  pellexlem6  43488  reglogcl  43544  modabsdifz  43640  areaquad  43870  imo72b2  44825  hashnzfzclim  44959  sineq0ALT  45572  suplesup  45982  reclt0d  46029  xrralrecnnge  46032  ltdiv23neg  46036  iooiinioc  46199  0ellimcdiv  46290  dvdivbd  46564  ioodvbdlimc1lem1  46572  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  stoweidlem1  46642  stoweidlem13  46654  stoweidlem26  46667  stoweidlem34  46675  stoweidlem36  46677  stoweidlem51  46692  stoweidlem60  46701  wallispilem4  46709  wallispilem5  46710  stirlingr  46731  dirker2re  46733  dirkerval2  46735  dirkerre  46736  dirkertrigeq  46742  dirkeritg  46743  dirkercncflem1  46744  dirkercncflem4  46747  fourierdlem4  46752  fourierdlem7  46755  fourierdlem9  46757  fourierdlem16  46764  fourierdlem19  46767  fourierdlem21  46769  fourierdlem22  46770  fourierdlem24  46772  fourierdlem26  46774  fourierdlem30  46778  fourierdlem39  46787  fourierdlem41  46789  fourierdlem42  46790  fourierdlem43  46791  fourierdlem47  46794  fourierdlem48  46795  fourierdlem49  46796  fourierdlem51  46798  fourierdlem56  46803  fourierdlem57  46804  fourierdlem58  46805  fourierdlem59  46806  fourierdlem63  46810  fourierdlem64  46811  fourierdlem66  46813  fourierdlem71  46818  fourierdlem72  46819  fourierdlem78  46825  fourierdlem83  46830  fourierdlem87  46834  fourierdlem89  46836  fourierdlem90  46837  fourierdlem91  46838  fourierdlem95  46842  fourierdlem103  46850  fourierdlem104  46851  etransclem48  46923  qndenserrnbllem  46935  sge0rpcpnf  47062  sge0ad2en  47072  ovnsubaddlem1  47211  hoidmvlelem3  47238  ovolval5lem1  47293  ovolval5lem2  47294  vonioolem2  47322  vonicclem2  47325  pimrecltneg  47365  smfrec  47430  smfdiv  47438  sigardiv  47502  modn0mul  48024  lighneallem2  48282  requad01  48310  requad1  48311  requad2  48312  refdivmptf  49242  fldivexpfllog2  49265  dignnld  49303  dig2nn1st  49305  dig2bits  49314  dignn0flhalflem2  49316  affinecomb1  49402  eenglngeehlnmlem1  49437  eenglngeehlnmlem2  49438  rrx2vlinest  49441  line2ylem  49451  line2  49452  line2xlem  49453  itsclc0lem1  49456  itsclc0lem2  49457  itscnhlc0yqe  49459  itsclquadb  49476