Theorem redivcld 12169

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  (class class class)co 7440  ℝcr 11223  0cc0 11224   / cdiv 11997

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998

This theorem is used by:  recp1lt1  12239  ledivp1  12243  supmul1  12310  rimul  12335  div4p1lem1div2  12625  divelunit  13649  fldiv4p1lem1div2  13999  fldiv4lem1div2uz2  14000  quoremz  14019  intfracq  14023  fldiv  14024  modmulnn  14053  modmuladd  14080  modmuladdnn0  14082  expnbnd  14400  discr1  14407  discr  14408  sqreulem  15553  fprodle  16189  fldivndvdslt  16612  flodddiv4t2lthalf  16614  iccpnfhmeo  25293  ipcau2  25582  mbfmulc2lem  25995  i1fmulc  26051  itg1mulc  26052  itg2monolem3  26100  dvferm2lem  26333  dvcvx  26367  radcnvlem1  26767  tanord1  26892  logf1o2  27005  relogbcl  27128  ang180lem2  27165  chordthmlem2  27188  jensenlem2  27342  regamcl  27415  gausslemma2dlem0d  27713  gausslemma2dlem3  27722  gausslemma2dlem4  27723  gausslemma2dlem5  27725  2lgslem1a2  27744  2lgslem1  27748  2lgslem2  27749  2lgsoddprmlem2  27763  selberg3lem1  27911  selberg4lem1  27914  ostth2  27991  ttgcontlem1  29489  colinearalg  29515  axsegconlem8  29529  axpaschlem  29545  axeuclidlem  29567  nmophmi  32660  cos9thpinconstrlem1  34488  unitdivcld  34600  dya2icoseg  34976  dya2iocucvr  34983  signsply0  35247  logdivsqrle  35346  hgt750lem  35347  hgt750leme  35354  tgoldbachgtde  35356  sinccvglem  36603  circum  36605  knoppndvlem1  37555  knoppndvlem14  37568  knoppndvlem15  37569  knoppndvlem17  37571  knoppndvlem18  37572  knoppndvlem19  37573  knoppndvlem21  37575  poimirlem31  38760  itg2addnclem  38780  itg2addnclem2  38781  areacirclem1  38817  areacirclem4  38820  lcmineqlem15  43284  3lexlogpow5ineq2  43296  3lexlogpow5ineq4  43297  3lexlogpow2ineq1  43299  3lexlogpow2ineq2  43300  3lexlogpow5ineq5  43301  dvrelog2  43305  dvrelog3  43306  dvrelog2b  43307  dvrelogpow2b  43309  aks4d1p1p4  43312  aks4d1p1p6  43314  aks4d1p1p7  43315  aks4d1p1p5  43316  aks4d1p5  43321  aks4d1p8  43328  aks6d1c2lem4  43368  2ap1caineq  43386  bcled  43419  bcle2d  43420  aks6d1c7lem1  43421  pellexlem1  44027  pellexlem6  44032  reglogcl  44088  modabsdifz  44184  areaquad  44408  imo72b2  45362  hashnzfzclim  45496  sineq0ALT  46108  suplesup  46554  reclt0d  46601  xrralrecnnge  46604  ltdiv23neg  46608  iooiinioc  46771  0ellimcdiv  46862  dvdivbd  47136  ioodvbdlimc1lem1  47144  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  stoweidlem1  47214  stoweidlem13  47226  stoweidlem26  47239  stoweidlem34  47247  stoweidlem36  47249  stoweidlem51  47264  stoweidlem60  47273  wallispilem4  47281  wallispilem5  47282  stirlingr  47303  dirker2re  47305  dirkerval2  47307  dirkerre  47308  dirkertrigeq  47314  dirkeritg  47315  dirkercncflem1  47316  dirkercncflem4  47319  fourierdlem4  47324  fourierdlem7  47327  fourierdlem9  47329  fourierdlem16  47336  fourierdlem19  47339  fourierdlem21  47341  fourierdlem22  47342  fourierdlem24  47344  fourierdlem26  47346  fourierdlem30  47350  fourierdlem39  47359  fourierdlem41  47361  fourierdlem42  47362  fourierdlem43  47363  fourierdlem47  47366  fourierdlem48  47367  fourierdlem49  47368  fourierdlem51  47370  fourierdlem56  47375  fourierdlem57  47376  fourierdlem58  47377  fourierdlem59  47378  fourierdlem63  47382  fourierdlem64  47383  fourierdlem66  47385  fourierdlem71  47390  fourierdlem72  47391  fourierdlem78  47397  fourierdlem83  47402  fourierdlem87  47406  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem95  47414  fourierdlem103  47422  fourierdlem104  47423  etransclem48  47495  qndenserrnbllem  47507  sge0rpcpnf  47634  sge0ad2en  47644  ovnsubaddlem1  47783  hoidmvlelem3  47810  ovolval5lem1  47865  ovolval5lem2  47866  vonioolem2  47894  vonicclem2  47897  pimrecltneg  47937  smfrec  48002  smfdiv  48010  sigardiv  48074  modn0mul  48636  lighneallem2  48894  requad01  48922  requad1  48923  requad2  48924  refdivmptf  49857  fldivexpfllog2  49880  dignnld  49918  dig2nn1st  49920  dig2bits  49929  dignn0flhalflem2  49931  affinecomb1  50017  eenglngeehlnmlem1  50053  eenglngeehlnmlem2  50054  rrx2vlinest  50056  line2ylem  50066  line2  50067  line2xlem  50068  itsclc0lem1  50071  itsclc0lem2  50072  itscnhlc0yqe  50074  itsclquadb  50091