Theorem redivcld 12073

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

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2937  (class class class)co 7420  ℝcr 11138  0cc0 11139   / cdiv 11902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903

This theorem is referenced by:  recp1lt1  12143  ledivp1  12147  supmul1  12214  rimul  12234  div4p1lem1div2  12498  divelunit  13504  fldiv4p1lem1div2  13833  fldiv4lem1div2uz2  13834  quoremz  13853  intfracq  13857  fldiv  13858  modmulnn  13887  modmuladd  13911  modmuladdnn0  13913  expnbnd  14227  discr1  14234  discr  14235  sqreulem  15339  fprodle  15973  fldivndvdslt  16391  flodddiv4t2lthalf  16393  iccpnfhmeo  24883  ipcau2  25175  mbfmulc2lem  25589  i1fmulc  25646  itg1mulc  25647  itg2monolem3  25695  dvferm2lem  25931  dvcvx  25966  radcnvlem1  26362  tanord1  26484  logf1o2  26597  relogbcl  26718  ang180lem2  26755  chordthmlem2  26778  jensenlem2  26933  regamcl  27006  gausslemma2dlem0d  27305  gausslemma2dlem3  27314  gausslemma2dlem4  27315  gausslemma2dlem5  27317  2lgslem1a2  27336  2lgslem1  27340  2lgslem2  27341  2lgsoddprmlem2  27355  selberg3lem1  27503  selberg4lem1  27506  ostth2  27583  ttgcontlem1  28708  colinearalg  28734  axsegconlem8  28748  axpaschlem  28764  axeuclidlem  28786  nmophmi  31854  unitdivcld  33502  dya2icoseg  33897  dya2iocucvr  33904  signsply0  34183  logdivsqrle  34282  hgt750lem  34283  hgt750leme  34290  tgoldbachgtde  34292  sinccvglem  35276  circum  35278  knoppndvlem1  35987  knoppndvlem14  36000  knoppndvlem15  36001  knoppndvlem17  36003  knoppndvlem18  36004  knoppndvlem19  36005  knoppndvlem21  36007  poimirlem31  37124  itg2addnclem  37144  itg2addnclem2  37145  areacirclem1  37181  areacirclem4  37184  lcmineqlem15  41514  3lexlogpow5ineq2  41526  3lexlogpow5ineq4  41527  3lexlogpow2ineq1  41529  3lexlogpow2ineq2  41530  3lexlogpow5ineq5  41531  dvrelog2  41535  dvrelog3  41536  dvrelog2b  41537  dvrelogpow2b  41539  aks4d1p1p4  41542  aks4d1p1p6  41544  aks4d1p1p7  41545  aks4d1p1p5  41546  aks4d1p5  41551  aks4d1p8  41558  aks6d1c2lem4  41598  2ap1caineq  41617  bcled  41650  bcle2d  41651  aks6d1c7lem1  41652  itrere  41879  pellexlem1  42249  pellexlem6  42254  reglogcl  42310  modabsdifz  42407  areaquad  42644  imo72b2  43602  hashnzfzclim  43759  sineq0ALT  44376  suplesup  44721  reclt0d  44769  xrralrecnnge  44772  ltdiv23neg  44776  iooiinioc  44941  0ellimcdiv  45037  dvdivbd  45311  ioodvbdlimc1lem1  45319  ioodvbdlimc1lem2  45320  ioodvbdlimc2lem  45322  stoweidlem1  45389  stoweidlem13  45401  stoweidlem26  45414  stoweidlem34  45422  stoweidlem36  45424  stoweidlem51  45439  stoweidlem60  45448  wallispilem4  45456  wallispilem5  45457  stirlingr  45478  dirker2re  45480  dirkerval2  45482  dirkerre  45483  dirkertrigeq  45489  dirkeritg  45490  dirkercncflem1  45491  dirkercncflem4  45494  fourierdlem4  45499  fourierdlem7  45502  fourierdlem9  45504  fourierdlem16  45511  fourierdlem19  45514  fourierdlem21  45516  fourierdlem22  45517  fourierdlem24  45519  fourierdlem26  45521  fourierdlem30  45525  fourierdlem39  45534  fourierdlem41  45536  fourierdlem42  45537  fourierdlem43  45538  fourierdlem47  45541  fourierdlem48  45542  fourierdlem49  45543  fourierdlem51  45545  fourierdlem56  45550  fourierdlem57  45551  fourierdlem58  45552  fourierdlem59  45553  fourierdlem63  45557  fourierdlem64  45558  fourierdlem66  45560  fourierdlem71  45565  fourierdlem72  45566  fourierdlem78  45572  fourierdlem83  45577  fourierdlem87  45581  fourierdlem89  45583  fourierdlem90  45584  fourierdlem91  45585  fourierdlem95  45589  fourierdlem103  45597  fourierdlem104  45598  etransclem48  45670  qndenserrnbllem  45682  sge0rpcpnf  45809  sge0ad2en  45819  ovnsubaddlem1  45958  hoidmvlelem3  45985  ovolval5lem1  46040  ovolval5lem2  46041  vonioolem2  46069  vonicclem2  46072  pimrecltneg  46112  smfrec  46177  smfdiv  46185  sigardiv  46249  lighneallem2  46946  requad01  46961  requad1  46962  requad2  46963  modn0mul  47593  refdivmptf  47615  fldivexpfllog2  47638  dignnld  47676  dig2nn1st  47678  dig2bits  47687  dignn0flhalflem2  47689  affinecomb1  47775  eenglngeehlnmlem1  47810  eenglngeehlnmlem2  47811  rrx2vlinest  47814  line2ylem  47824  line2  47825  line2xlem  47826  itsclc0lem1  47829  itsclc0lem2  47830  itscnhlc0yqe  47832  itsclquadb  47849