Theorem rpreccld 13044

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

Hypothesis

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

Assertion

Ref	Expression
rpreccld	⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+)

Proof of Theorem rpreccld

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpreccl 13018	. 2 ⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
3	1, 2	syl 17	1 ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7414  1c1 11125   / cdiv 11887  ℝ⁺crp 12992

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 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

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 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  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 8716  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-rp 12993

This theorem is referenced by:  rprecred  13045  resqrex  15215  rlimno1  15618  supcvg  15820  harmonic  15823  expcnv  15828  eirrlem  16166  prmreclem5  16874  prmreclem6  16875  met1stc  24404  met2ndci  24405  nmoi2  24621  bcthlem5  25230  ovolsca  25418  vitali  25516  ismbf3d  25557  itg2seq  25646  itg2mulclem  25650  itg2mulc  25651  aalioulem3  26243  aaliou3lem8  26254  dvradcnv  26331  tanregt0  26447  divlogrlim  26543  advlogexp  26563  logtayllem  26567  divcxp  26595  cxpcn3lem  26656  loglesqrt  26667  logbrec  26688  ang180lem2  26716  asinlem3  26777  leibpi  26848  rlimcnp  26871  rlimcnp2  26872  efrlim  26875  efrlimOLD  26876  cxplim  26878  cxp2lim  26883  divsqrtsumlem  26886  amgmlem  26896  emcllem2  26903  emcllem4  26905  emcllem5  26906  emcllem6  26907  fsumharmonic  26918  lgamgulmlem5  26939  lgambdd  26943  basellem3  26989  basellem6  26992  logfaclbnd  27129  bclbnd  27187  rplogsumlem2  27392  rpvmasumlem  27394  dchrisum0lem2a  27424  log2sumbnd  27451  logdivbnd  27463  pntlemo  27514  nrt2irr  30257  smcnlem  30481  minvecolem3  30660  minvecolem4  30664  esumdivc  33625  dya2ub  33813  omssubadd  33843  logdivsqrle  34205  iprodgam  35259  faclimlem1  35260  faclimlem3  35262  faclim  35263  iprodfac  35264  poimirlem29  37044  poimirlem30  37045  heiborlem3  37208  heiborlem6  37211  heiborlem8  37213  heibor  37216  irrapxlem4  42157  irrapxlem5  42158  oddfl  44572  xralrple4  44668  xrralrecnnge  44685  ioodvbdlimc1lem2  45233  ioodvbdlimc2lem  45235  stoweid  45364  wallispi  45371  stirlinglem1  45375  stirlinglem6  45380  stirlinglem10  45384  stirlinglem11  45385  dirkertrigeqlem3  45401  dirkercncflem2  45405  iinhoiicc  45975  iunhoiioo  45977  vonioolem2  45982  vonicclem1  45984  eenglngeehlnmlem2  47724  amgmlemALT  48149  young2d  48151