Theorem rpdivcld 13059

Description: Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)
rpaddcld.1	⊢ (𝜑 → 𝐵 ∈ ℝ+)

Assertion

Ref	Expression
rpdivcld	⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Proof of Theorem rpdivcld

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
3		rpdivcl 13025	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7414   / cdiv 11895  ℝ⁺crp 13000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-div 11896  df-rp 13001

This theorem is referenced by:  bcpasc  14306  mulcn2  15566  o1rlimmul  15589  mertenslem1  15856  mertenslem2  15857  effsumlt  16081  prmind2  16649  nlmvscnlem2  24595  nlmvscnlem1  24596  nghmcn  24655  lebnumlem3  24882  lebnumii  24885  nmoleub3  25039  ipcnlem2  25165  ipcnlem1  25166  equivcfil  25220  equivcau  25221  ovollb2lem  25410  ovoliunlem1  25424  uniioombllem6  25510  itg2const2  25664  itg2cnlem2  25685  aalioulem2  26261  aalioulem4  26263  aalioulem5  26264  aalioulem6  26265  aaliou  26266  aaliou2b  26269  aaliou3lem9  26278  itgulm  26337  abelthlem7  26368  abelthlem8  26369  tanrpcl  26432  logdivlti  26547  logcnlem2  26570  ang180lem2  26735  isosctrlem2  26744  birthdaylem2  26877  cxp2limlem  26901  cxp2lim  26902  cxploglim  26903  cxploglim2  26904  amgmlem  26915  logdiflbnd  26920  emcllem2  26922  fsumharmonic  26937  lgamgulmlem2  26955  lgamgulmlem3  26956  lgamgulmlem4  26957  lgamgulmlem5  26958  lgamgulmlem6  26959  lgamgulm2  26961  lgamucov  26963  lgamcvg2  26980  gamcvg  26981  gamcvg2lem  26984  regamcl  26986  relgamcl  26987  lgam1  26989  ftalem4  27001  chpval2  27144  chpchtsum  27145  logfacrlim  27150  logexprlim  27151  bclbnd  27206  bposlem1  27210  bposlem2  27211  lgsquadlem2  27307  chebbnd1lem1  27395  chebbnd1lem3  27397  chebbnd1  27398  chtppilimlem2  27400  chebbnd2  27403  chto1lb  27404  rplogsumlem2  27411  rpvmasumlem  27413  dchrvmasumlem1  27421  dchrvmasum2if  27423  dchrisum0lem1b  27441  dchrisum0lem2a  27443  vmalogdivsum2  27464  2vmadivsumlem  27466  selberglem3  27473  selberg  27474  selberg4lem1  27486  selberg3r  27495  selberg4r  27496  selberg34r  27497  pntrlog2bndlem1  27503  pntrlog2bndlem2  27504  pntrlog2bndlem3  27505  pntrlog2bndlem4  27506  pntrlog2bndlem5  27507  pntrlog2bndlem6a  27508  pntrlog2bndlem6  27509  pntrlog2bnd  27510  pntpbnd1a  27511  pntpbnd1  27512  pntpbnd2  27513  pntibndlem2  27517  pntibndlem3  27518  pntlemd  27520  pntlemc  27521  pntlema  27522  pntlemb  27523  pntlemg  27524  pntlemn  27526  pntlemq  27527  pntlemr  27528  pntlemj  27529  pntlemf  27531  pntlemo  27533  pnt2  27539  pnt  27540  ostth2lem3  27561  ostth2  27563  nrt2irr  30276  blocni  30608  ubthlem2  30674  lnconi  31836  rpxdivcld  32651  omssubadd  33914  hgt750leme  34284  faclimlem1  35331  faclimlem3  35333  faclim  35334  iprodfac  35335  equivtotbnd  37245  rrncmslem  37299  rrnequiv  37302  3lexlogpow2ineq2  41524  3lexlogpow5ineq5  41525  aks4d1p1p7  41539  fltne  42062  irrapxlem5  42240  xralrple2  44730  xralrple3  44750  iooiinicc  44921  iooiinioc  44935  limclner  45033  fprodsubrecnncnvlem  45289  fprodaddrecnncnvlem  45291  stoweidlem31  45413  stoweidlem59  45441  wallispilem3  45449  wallispilem4  45450  wallispilem5  45451  wallispi  45452  wallispi2lem1  45453  stirlinglem2  45457  stirlinglem4  45459  stirlinglem8  45463  stirlinglem13  45468  stirlinglem15  45470  stirlingr  45472  fourierdlem30  45519  fourierdlem73  45561  fourierdlem87  45575  qndenserrnbllem  45676  ovnsubaddlem1  45952  ovnsubaddlem2  45953  hoiqssbllem1  46004  hoiqssbllem2  46005  hoiqssbllem3  46006  ovolval5lem1  46034  ovolval5lem2  46035  vonioolem1  46062  smfmullem1  46173  smfmullem2  46174  smfmullem3  46175

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »