Theorem rphalfcl 13059

Description: Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)

Assertion

Ref	Expression
rphalfcl	⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+)

Proof of Theorem rphalfcl

Step	Hyp	Ref	Expression
1		2rp 13037	. 2 ⊢ 2 ∈ ℝ+
2		rpdivcl 13057	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (𝐴 / 2) ∈ ℝ+)
3	1, 2	mpan2 689	1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2100  (class class class)co 7427   / cdiv 11922  2c2 12323  ℝ⁺crp 13032

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 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-po 5596  df-so 5597  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7383  df-ov 7430  df-oprab 7431  df-mpo 7432  df-er 8738  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11497  df-neg 11498  df-div 11923  df-2 12331  df-rp 13033

This theorem is referenced by:  rphalfcld  13086  rpltrp  13378  cau3lem  15372  2clim  15587  addcn2  15609  mulcn2  15611  climcau  15688  metcnpi3  24546  ngptgp  24636  iccntr  24828  reconnlem2  24834  opnreen  24838  xmetdcn2  24844  cnllycmp  24973  iscfil3  25292  cfilfcls  25293  iscmet3lem3  25309  iscmet3lem1  25310  iscmet3lem2  25311  iscmet3  25312  lmcau  25332  bcthlem5  25347  ivthlem2  25472  uniioombl  25609  dvcnvre  26043  aaliou  26363  ulmcaulem  26420  ulmcau  26421  ulmcn  26425  ulmdvlem3  26428  tanregt0  26563  argregt0  26634  argrege0  26635  logimul  26638  resqrtcn  26774  asin1  26919  reasinsin  26921  atanbnd  26951  atan1  26953  sqrtlim  26998  basellem4  27109  chpchtlim  27505  mulog2sumlem2  27561  pntlem3  27635  vacn  30669  ubthlem1  30845  nmcexi  32001  poimirlem29  37435  heicant  37441  ftc1anclem6  37484  ftc1anclem7  37485  ftc1anc  37487  heibor1lem  37595  heiborlem8  37604  bfplem2  37609  supxrge  45064  suplesup  45065  infleinflem1  45096  infleinf  45098  addlimc  45380  fourierdlem103  45941  fourierdlem104  45942  sge0xaddlem2  46166  smflimlem4  46506