Theorem redivcld 11978

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  (class class class)co 7362  ℝcr 11032  0cc0 11033   / cdiv 11802

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 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

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 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-po 5534  df-so 5535  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803

This theorem is referenced by:  recp1lt1  12049  ledivp1  12053  supmul1  12120  rimul  12145  div4p1lem1div2  12427  divelunit  13442  fldiv4p1lem1div2  13789  fldiv4lem1div2uz2  13790  quoremz  13809  intfracq  13813  fldiv  13814  modmulnn  13843  modmuladd  13870  modmuladdnn0  13872  expnbnd  14189  discr1  14196  discr  14197  sqreulem  15317  fprodle  15956  fldivndvdslt  16380  flodddiv4t2lthalf  16382  iccpnfhmeo  24926  ipcau2  25215  mbfmulc2lem  25628  i1fmulc  25684  itg1mulc  25685  itg2monolem3  25733  dvferm2lem  25967  dvcvx  26001  radcnvlem1  26395  tanord1  26518  logf1o2  26631  relogbcl  26754  ang180lem2  26791  chordthmlem2  26814  jensenlem2  26969  regamcl  27042  gausslemma2dlem0d  27340  gausslemma2dlem3  27349  gausslemma2dlem4  27350  gausslemma2dlem5  27352  2lgslem1a2  27371  2lgslem1  27375  2lgslem2  27376  2lgsoddprmlem2  27390  selberg3lem1  27538  selberg4lem1  27541  ostth2  27618  ttgcontlem1  28971  colinearalg  28997  axsegconlem8  29011  axpaschlem  29027  axeuclidlem  29049  nmophmi  32121  cos9thpinconstrlem1  33953  unitdivcld  34065  dya2icoseg  34441  dya2iocucvr  34448  signsply0  34715  logdivsqrle  34814  hgt750lem  34815  hgt750leme  34822  tgoldbachgtde  34824  sinccvglem  35874  circum  35876  knoppndvlem1  36792  knoppndvlem14  36805  knoppndvlem15  36806  knoppndvlem17  36808  knoppndvlem18  36809  knoppndvlem19  36810  knoppndvlem21  36812  poimirlem31  37992  itg2addnclem  38012  itg2addnclem2  38013  areacirclem1  38049  areacirclem4  38052  lcmineqlem15  42502  3lexlogpow5ineq2  42514  3lexlogpow5ineq4  42515  3lexlogpow2ineq1  42517  3lexlogpow2ineq2  42518  3lexlogpow5ineq5  42519  dvrelog2  42523  dvrelog3  42524  dvrelog2b  42525  dvrelogpow2b  42527  aks4d1p1p4  42530  aks4d1p1p6  42532  aks4d1p1p7  42533  aks4d1p1p5  42534  aks4d1p5  42539  aks4d1p8  42546  aks6d1c2lem4  42586  2ap1caineq  42604  bcled  42637  bcle2d  42638  aks6d1c7lem1  42639  pellexlem1  43281  pellexlem6  43286  reglogcl  43342  modabsdifz  43438  areaquad  43668  imo72b2  44623  hashnzfzclim  44773  sineq0ALT  45387  suplesup  45793  reclt0d  45840  xrralrecnnge  45843  ltdiv23neg  45847  iooiinioc  46010  0ellimcdiv  46101  dvdivbd  46375  ioodvbdlimc1lem1  46383  ioodvbdlimc1lem2  46384  ioodvbdlimc2lem  46386  stoweidlem1  46453  stoweidlem13  46465  stoweidlem26  46478  stoweidlem34  46486  stoweidlem36  46488  stoweidlem51  46503  stoweidlem60  46512  wallispilem4  46520  wallispilem5  46521  stirlingr  46542  dirker2re  46544  dirkerval2  46546  dirkerre  46547  dirkertrigeq  46553  dirkeritg  46554  dirkercncflem1  46555  dirkercncflem4  46558  fourierdlem4  46563  fourierdlem7  46566  fourierdlem9  46568  fourierdlem16  46575  fourierdlem19  46578  fourierdlem21  46580  fourierdlem22  46581  fourierdlem24  46583  fourierdlem26  46585  fourierdlem30  46589  fourierdlem39  46598  fourierdlem41  46600  fourierdlem42  46601  fourierdlem43  46602  fourierdlem47  46605  fourierdlem48  46606  fourierdlem49  46607  fourierdlem51  46609  fourierdlem56  46614  fourierdlem57  46615  fourierdlem58  46616  fourierdlem59  46617  fourierdlem63  46621  fourierdlem64  46622  fourierdlem66  46624  fourierdlem71  46629  fourierdlem72  46630  fourierdlem78  46636  fourierdlem83  46641  fourierdlem87  46645  fourierdlem89  46647  fourierdlem90  46648  fourierdlem91  46649  fourierdlem95  46653  fourierdlem103  46661  fourierdlem104  46662  etransclem48  46734  qndenserrnbllem  46746  sge0rpcpnf  46873  sge0ad2en  46883  ovnsubaddlem1  47022  hoidmvlelem3  47049  ovolval5lem1  47104  ovolval5lem2  47105  vonioolem2  47133  vonicclem2  47136  pimrecltneg  47176  smfrec  47241  smfdiv  47249  sigardiv  47313  modn0mul  47829  lighneallem2  48087  requad01  48115  requad1  48116  requad2  48117  refdivmptf  49036  fldivexpfllog2  49059  dignnld  49097  dig2nn1st  49099  dig2bits  49108  dignn0flhalflem2  49110  affinecomb1  49196  eenglngeehlnmlem1  49231  eenglngeehlnmlem2  49232  rrx2vlinest  49235  line2ylem  49245  line2  49246  line2xlem  49247  itsclc0lem1  49250  itsclc0lem2  49251  itscnhlc0yqe  49253  itsclquadb  49270