Theorem redivcld 12070

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2957  (class class class)co 7416  ℝcr 11126  0cc0 11127   / cdiv 11898

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899

This theorem is used by:  recp1lt1  12140  ledivp1  12144  supmul1  12211  rimul  12236  div4p1lem1div2  12526  divelunit  13549  fldiv4p1lem1div2  13898  fldiv4lem1div2uz2  13899  quoremz  13918  intfracq  13922  fldiv  13923  modmulnn  13952  modmuladd  13979  modmuladdnn0  13981  expnbnd  14298  discr1  14305  discr  14306  sqreulem  15449  fprodle  16087  fldivndvdslt  16510  flodddiv4t2lthalf  16512  iccpnfhmeo  25174  ipcau2  25463  mbfmulc2lem  25876  i1fmulc  25932  itg1mulc  25933  itg2monolem3  25981  dvferm2lem  26215  dvcvx  26249  radcnvlem1  26646  tanord1  26772  logf1o2  26885  relogbcl  27008  ang180lem2  27045  chordthmlem2  27068  jensenlem2  27222  regamcl  27295  gausslemma2dlem0d  27593  gausslemma2dlem3  27602  gausslemma2dlem4  27603  gausslemma2dlem5  27605  2lgslem1a2  27624  2lgslem1  27628  2lgslem2  27629  2lgsoddprmlem2  27643  selberg3lem1  27791  selberg4lem1  27794  ostth2  27871  ttgcontlem1  29327  colinearalg  29353  axsegconlem8  29367  axpaschlem  29383  axeuclidlem  29405  nmophmi  32498  cos9thpinconstrlem1  34286  unitdivcld  34398  dya2icoseg  34775  dya2iocucvr  34782  signsply0  35046  logdivsqrle  35145  hgt750lem  35146  hgt750leme  35153  tgoldbachgtde  35155  sinccvglem  36238  circum  36240  knoppndvlem1  37196  knoppndvlem14  37209  knoppndvlem15  37210  knoppndvlem17  37212  knoppndvlem18  37213  knoppndvlem19  37214  knoppndvlem21  37216  poimirlem31  38387  itg2addnclem  38407  itg2addnclem2  38408  areacirclem1  38444  areacirclem4  38447  lcmineqlem15  42896  3lexlogpow5ineq2  42908  3lexlogpow5ineq4  42909  3lexlogpow2ineq1  42911  3lexlogpow2ineq2  42912  3lexlogpow5ineq5  42913  dvrelog2  42917  dvrelog3  42918  dvrelog2b  42919  dvrelogpow2b  42921  aks4d1p1p4  42924  aks4d1p1p6  42926  aks4d1p1p7  42927  aks4d1p1p5  42928  aks4d1p5  42933  aks4d1p8  42940  aks6d1c2lem4  42980  2ap1caineq  42998  bcled  43031  bcle2d  43032  aks6d1c7lem1  43033  pellexlem1  43657  pellexlem6  43662  reglogcl  43718  modabsdifz  43814  areaquad  44044  imo72b2  44999  hashnzfzclim  45133  sineq0ALT  45746  suplesup  46156  reclt0d  46203  xrralrecnnge  46206  ltdiv23neg  46210  iooiinioc  46373  0ellimcdiv  46464  dvdivbd  46738  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  stoweidlem1  46816  stoweidlem13  46828  stoweidlem26  46841  stoweidlem34  46849  stoweidlem36  46851  stoweidlem51  46866  stoweidlem60  46875  wallispilem4  46883  wallispilem5  46884  stirlingr  46905  dirker2re  46907  dirkerval2  46909  dirkerre  46910  dirkertrigeq  46916  dirkeritg  46917  dirkercncflem1  46918  dirkercncflem4  46921  fourierdlem4  46926  fourierdlem7  46929  fourierdlem9  46931  fourierdlem16  46938  fourierdlem19  46941  fourierdlem21  46943  fourierdlem22  46944  fourierdlem24  46946  fourierdlem26  46948  fourierdlem30  46952  fourierdlem39  46961  fourierdlem41  46963  fourierdlem42  46964  fourierdlem43  46965  fourierdlem47  46968  fourierdlem48  46969  fourierdlem49  46970  fourierdlem51  46972  fourierdlem56  46977  fourierdlem57  46978  fourierdlem58  46979  fourierdlem59  46980  fourierdlem63  46984  fourierdlem64  46985  fourierdlem66  46987  fourierdlem71  46992  fourierdlem72  46993  fourierdlem78  46999  fourierdlem83  47004  fourierdlem87  47008  fourierdlem89  47010  fourierdlem90  47011  fourierdlem91  47012  fourierdlem95  47016  fourierdlem103  47024  fourierdlem104  47025  etransclem48  47097  qndenserrnbllem  47109  sge0rpcpnf  47236  sge0ad2en  47246  ovnsubaddlem1  47385  hoidmvlelem3  47412  ovolval5lem1  47467  ovolval5lem2  47468  vonioolem2  47496  vonicclem2  47499  pimrecltneg  47539  smfrec  47604  smfdiv  47612  sigardiv  47676  modn0mul  48238  lighneallem2  48496  requad01  48524  requad1  48525  requad2  48526  refdivmptf  49459  fldivexpfllog2  49482  dignnld  49520  dig2nn1st  49522  dig2bits  49531  dignn0flhalflem2  49533  affinecomb1  49619  eenglngeehlnmlem1  49654  eenglngeehlnmlem2  49655  rrx2vlinest  49658  line2ylem  49668  line2  49669  line2xlem  49670  itsclc0lem1  49673  itsclc0lem2  49674  itscnhlc0yqe  49676  itsclquadb  49693