Theorem redivcld 12145

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955  (class class class)co 7420  ℝcr 11199  0cc0 11200   / cdiv 11973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-div 11974

This theorem is used by:  recp1lt1  12215  ledivp1  12219  supmul1  12286  rimul  12311  div4p1lem1div2  12601  divelunit  13625  fldiv4p1lem1div2  13975  fldiv4lem1div2uz2  13976  quoremz  13995  intfracq  13999  fldiv  14000  modmulnn  14029  modmuladd  14056  modmuladdnn0  14058  expnbnd  14376  discr1  14383  discr  14384  sqreulem  15527  fprodle  16163  fldivndvdslt  16586  flodddiv4t2lthalf  16588  iccpnfhmeo  25266  ipcau2  25555  mbfmulc2lem  25968  i1fmulc  26024  itg1mulc  26025  itg2monolem3  26073  dvferm2lem  26306  dvcvx  26340  radcnvlem1  26740  tanord1  26865  logf1o2  26978  relogbcl  27101  ang180lem2  27138  chordthmlem2  27161  jensenlem2  27315  regamcl  27388  gausslemma2dlem0d  27686  gausslemma2dlem3  27695  gausslemma2dlem4  27696  gausslemma2dlem5  27698  2lgslem1a2  27717  2lgslem1  27721  2lgslem2  27722  2lgsoddprmlem2  27736  selberg3lem1  27884  selberg4lem1  27887  ostth2  27964  ttgcontlem1  29462  colinearalg  29488  axsegconlem8  29502  axpaschlem  29518  axeuclidlem  29540  nmophmi  32633  cos9thpinconstrlem1  34421  unitdivcld  34533  dya2icoseg  34909  dya2iocucvr  34916  signsply0  35180  logdivsqrle  35279  hgt750lem  35280  hgt750leme  35287  tgoldbachgtde  35289  sinccvglem  36437  circum  36439  knoppndvlem1  37378  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem18  37395  knoppndvlem19  37396  knoppndvlem21  37398  poimirlem31  38570  itg2addnclem  38590  itg2addnclem2  38591  areacirclem1  38627  areacirclem4  38630  lcmineqlem15  43094  3lexlogpow5ineq2  43106  3lexlogpow5ineq4  43107  3lexlogpow2ineq1  43109  3lexlogpow2ineq2  43110  3lexlogpow5ineq5  43111  dvrelog2  43115  dvrelog3  43116  dvrelog2b  43117  dvrelogpow2b  43119  aks4d1p1p4  43122  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p1p5  43126  aks4d1p5  43131  aks4d1p8  43138  aks6d1c2lem4  43178  2ap1caineq  43196  bcled  43229  bcle2d  43230  aks6d1c7lem1  43231  pellexlem1  43836  pellexlem6  43841  reglogcl  43897  modabsdifz  43993  areaquad  44218  imo72b2  45172  hashnzfzclim  45306  sineq0ALT  45919  suplesup  46351  reclt0d  46398  xrralrecnnge  46401  ltdiv23neg  46405  iooiinioc  46568  0ellimcdiv  46659  dvdivbd  46933  ioodvbdlimc1lem1  46941  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  stoweidlem1  47011  stoweidlem13  47023  stoweidlem26  47036  stoweidlem34  47044  stoweidlem36  47046  stoweidlem51  47061  stoweidlem60  47070  wallispilem4  47078  wallispilem5  47079  stirlingr  47100  dirker2re  47102  dirkerval2  47104  dirkerre  47105  dirkertrigeq  47111  dirkeritg  47112  dirkercncflem1  47113  dirkercncflem4  47116  fourierdlem4  47121  fourierdlem7  47124  fourierdlem9  47126  fourierdlem16  47133  fourierdlem19  47136  fourierdlem21  47138  fourierdlem22  47139  fourierdlem24  47141  fourierdlem26  47143  fourierdlem30  47147  fourierdlem39  47156  fourierdlem41  47158  fourierdlem42  47159  fourierdlem43  47160  fourierdlem47  47163  fourierdlem48  47164  fourierdlem49  47165  fourierdlem51  47167  fourierdlem56  47172  fourierdlem57  47173  fourierdlem58  47174  fourierdlem59  47175  fourierdlem63  47179  fourierdlem64  47180  fourierdlem66  47182  fourierdlem71  47187  fourierdlem72  47188  fourierdlem78  47194  fourierdlem83  47199  fourierdlem87  47203  fourierdlem89  47205  fourierdlem90  47206  fourierdlem91  47207  fourierdlem95  47211  fourierdlem103  47219  fourierdlem104  47220  etransclem48  47292  qndenserrnbllem  47304  sge0rpcpnf  47431  sge0ad2en  47441  ovnsubaddlem1  47580  hoidmvlelem3  47607  ovolval5lem1  47662  ovolval5lem2  47663  vonioolem2  47691  vonicclem2  47694  pimrecltneg  47734  smfrec  47799  smfdiv  47807  sigardiv  47871  modn0mul  48433  lighneallem2  48691  requad01  48719  requad1  48720  requad2  48721  refdivmptf  49654  fldivexpfllog2  49677  dignnld  49715  dig2nn1st  49717  dig2bits  49726  dignn0flhalflem2  49728  affinecomb1  49814  eenglngeehlnmlem1  49849  eenglngeehlnmlem2  49850  rrx2vlinest  49853  line2ylem  49863  line2  49864  line2xlem  49865  itsclc0lem1  49868  itsclc0lem2  49869  itscnhlc0yqe  49871  itsclquadb  49888