Theorem redivcld 11973

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7360  ℝcr 11029  0cc0 11030   / cdiv 11798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799

This theorem is referenced by:  recp1lt1  12044  ledivp1  12048  supmul1  12115  rimul  12140  div4p1lem1div2  12400  divelunit  13414  fldiv4p1lem1div2  13759  fldiv4lem1div2uz2  13760  quoremz  13779  intfracq  13783  fldiv  13784  modmulnn  13813  modmuladd  13840  modmuladdnn0  13842  expnbnd  14159  discr1  14166  discr  14167  sqreulem  15287  fprodle  15923  fldivndvdslt  16347  flodddiv4t2lthalf  16349  iccpnfhmeo  24903  ipcau2  25194  mbfmulc2lem  25608  i1fmulc  25664  itg1mulc  25665  itg2monolem3  25713  dvferm2lem  25950  dvcvx  25985  radcnvlem1  26382  tanord1  26506  logf1o2  26619  relogbcl  26743  ang180lem2  26780  chordthmlem2  26803  jensenlem2  26958  regamcl  27031  gausslemma2dlem0d  27330  gausslemma2dlem3  27339  gausslemma2dlem4  27340  gausslemma2dlem5  27342  2lgslem1a2  27361  2lgslem1  27365  2lgslem2  27366  2lgsoddprmlem2  27380  selberg3lem1  27528  selberg4lem1  27531  ostth2  27608  ttgcontlem1  28961  colinearalg  28987  axsegconlem8  29001  axpaschlem  29017  axeuclidlem  29039  nmophmi  32110  cos9thpinconstrlem1  33948  unitdivcld  34060  dya2icoseg  34436  dya2iocucvr  34443  signsply0  34710  logdivsqrle  34809  hgt750lem  34810  hgt750leme  34817  tgoldbachgtde  34819  sinccvglem  35868  circum  35870  knoppndvlem1  36714  knoppndvlem14  36727  knoppndvlem15  36728  knoppndvlem17  36730  knoppndvlem18  36731  knoppndvlem19  36732  knoppndvlem21  36734  poimirlem31  37854  itg2addnclem  37874  itg2addnclem2  37875  areacirclem1  37911  areacirclem4  37914  lcmineqlem15  42365  3lexlogpow5ineq2  42377  3lexlogpow5ineq4  42378  3lexlogpow2ineq1  42380  3lexlogpow2ineq2  42381  3lexlogpow5ineq5  42382  dvrelog2  42386  dvrelog3  42387  dvrelog2b  42388  dvrelogpow2b  42390  aks4d1p1p4  42393  aks4d1p1p6  42395  aks4d1p1p7  42396  aks4d1p1p5  42397  aks4d1p5  42402  aks4d1p8  42409  aks6d1c2lem4  42449  2ap1caineq  42467  bcled  42500  bcle2d  42501  aks6d1c7lem1  42502  pellexlem1  43138  pellexlem6  43143  reglogcl  43199  modabsdifz  43295  areaquad  43525  imo72b2  44480  hashnzfzclim  44630  sineq0ALT  45244  suplesup  45651  reclt0d  45698  xrralrecnnge  45701  ltdiv23neg  45705  iooiinioc  45869  0ellimcdiv  45960  dvdivbd  46234  ioodvbdlimc1lem1  46242  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweidlem1  46312  stoweidlem13  46324  stoweidlem26  46337  stoweidlem34  46345  stoweidlem36  46347  stoweidlem51  46362  stoweidlem60  46371  wallispilem4  46379  wallispilem5  46380  stirlingr  46401  dirker2re  46403  dirkerval2  46405  dirkerre  46406  dirkertrigeq  46412  dirkeritg  46413  dirkercncflem1  46414  dirkercncflem4  46417  fourierdlem4  46422  fourierdlem7  46425  fourierdlem9  46427  fourierdlem16  46434  fourierdlem19  46437  fourierdlem21  46439  fourierdlem22  46440  fourierdlem24  46442  fourierdlem26  46444  fourierdlem30  46448  fourierdlem39  46457  fourierdlem41  46459  fourierdlem42  46460  fourierdlem43  46461  fourierdlem47  46464  fourierdlem48  46465  fourierdlem49  46466  fourierdlem51  46468  fourierdlem56  46473  fourierdlem57  46474  fourierdlem58  46475  fourierdlem59  46476  fourierdlem63  46480  fourierdlem64  46481  fourierdlem66  46483  fourierdlem71  46488  fourierdlem72  46489  fourierdlem78  46495  fourierdlem83  46500  fourierdlem87  46504  fourierdlem89  46506  fourierdlem90  46507  fourierdlem91  46508  fourierdlem95  46512  fourierdlem103  46520  fourierdlem104  46521  etransclem48  46593  qndenserrnbllem  46605  sge0rpcpnf  46732  sge0ad2en  46742  ovnsubaddlem1  46881  hoidmvlelem3  46908  ovolval5lem1  46963  ovolval5lem2  46964  vonioolem2  46992  vonicclem2  46995  pimrecltneg  47035  smfrec  47100  smfdiv  47108  sigardiv  47172  modn0mul  47670  lighneallem2  47919  requad01  47934  requad1  47935  requad2  47936  refdivmptf  48855  fldivexpfllog2  48878  dignnld  48916  dig2nn1st  48918  dig2bits  48927  dignn0flhalflem2  48929  affinecomb1  49015  eenglngeehlnmlem1  49050  eenglngeehlnmlem2  49051  rrx2vlinest  49054  line2ylem  49064  line2  49065  line2xlem  49066  itsclc0lem1  49069  itsclc0lem2  49070  itscnhlc0yqe  49072  itsclquadb  49089