Theorem rpreccld 13214

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 13188	. 2 ⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
3	1, 2	syl 18	1 ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  1c1 11240   / cdiv 12013  ℝ⁺crp 13160

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 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

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 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-rp 13161

This theorem is used by:  rprecred  13215  resqrex  15460  rlimno1  15865  supcvg  16069  harmonic  16072  expcnv  16077  eirrlem  16416  prmreclem5  17142  prmreclem6  17143  met1stc  24895  met2ndci  24896  nmoi2  25104  bcthlem5  25704  ovolsca  25891  vitali  25989  ismbf3d  26030  itg2seq  26118  itg2mulclem  26122  itg2mulc  26123  aalioulem3  26718  aaliou3lem8  26729  dvradcnv  26805  tanregt0  26924  divlogrlim  27020  advlogexp  27040  logtayllem  27044  divcxp  27072  cxpcn3lem  27132  loglesqrt  27146  logbrec  27167  ang180lem2  27195  asinlem3  27256  leibpi  27327  rlimcnp  27350  rlimcnp2  27351  efrlim  27354  cxplim  27356  cxp2lim  27361  divsqrtsumlem  27364  amgmlem  27374  emcllem2  27381  emcllem4  27383  emcllem5  27384  emcllem6  27385  fsumharmonic  27396  lgamgulmlem5  27417  lgambdd  27421  basellem3  27467  basellem6  27470  logfaclbnd  27606  bclbnd  27664  rplogsumlem2  27869  rpvmasumlem  27871  dchrisum0lem2a  27901  log2sumbnd  27928  logdivbnd  27940  pntlemo  27991  nrt2irr  31131  smcnlem  31356  minvecolem3  31535  minvecolem4  31539  esumdivc  34826  dya2ub  35013  omssubadd  35043  logdivsqrle  35390  iprodgam  36722  faclimlem1  36723  faclimlem3  36725  faclim  36726  iprodfac  36727  poimirlem29  38835  poimirlem30  38836  heiborlem3  39013  heiborlem6  39016  heiborlem8  39018  heibor  39021  irrapxlem4  44098  irrapxlem5  44099  oddfl  46567  xralrple4  46657  xrralrecnnge  46674  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  stoweid  47346  wallispi  47353  stirlinglem1  47357  stirlinglem6  47362  stirlinglem10  47366  stirlinglem11  47367  dirkertrigeqlem3  47383  dirkercncflem2  47387  iinhoiicc  47957  iunhoiioo  47959  vonioolem2  47964  vonicclem1  47966  eenglngeehlnmlem2  50182  amgmlemALT  51416  young2d  51418