Theorem rphalfcld 12995

Description: Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

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

Assertion

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

Proof of Theorem rphalfcld

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7364   / cdiv 11804  2c2 12233  ℝ⁺crp 12939

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 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

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 5523  df-po 5536  df-so 5537  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-div 11805  df-2 12241  df-rp 12940

This theorem is referenced by:  nnesq  14186  rlimuni  15509  climuni  15511  reccn2  15556  iseralt  15644  mertenslem1  15846  mertenslem2  15847  ege2le3  16052  rpcoshcl  16121  sqrt2irrlem  16212  4sqlem7  16912  ssblex  24409  methaus  24501  met2ndci  24503  metustexhalf  24537  cfilucfil  24540  nlmvscnlem2  24666  nlmvscnlem1  24667  nrginvrcnlem  24672  reperflem  24800  icccmplem2  24805  metdcnlem  24818  metnrmlem2  24842  metnrmlem3  24843  ipcnlem2  25227  ipcnlem1  25228  minveclem3  25412  ovollb2lem  25471  ovolunlem2  25481  uniioombl  25572  itg2cnlem2  25745  itg2cn  25746  lhop1lem  25996  lhop1  25997  aaliou2b  26324  ulmcn  26383  pserdvlem1  26411  pserdv  26413  cxpcn3lem  26730  lgamgulmlem3  27014  lgamucov  27021  ftalem2  27057  bposlem7  27273  bposlem9  27275  lgsquadlem2  27364  chebbnd1lem2  27453  pntibndlem3  27575  pntibnd  27576  pntlemr  27585  lt2addrd  32844  tpr2rico  34078  knoppndvlem17  36810  tan2h  37955  mblfinlem4  38003  sstotbnd2  38117  3lexlogpow2ineq2  42520  dstregt0  45741  suplesup  45795  infleinf  45827  lptre2pt  46094  0ellimcdiv  46103  limsupgtlem  46231  ioodvbdlimc1lem2  46386  ioodvbdlimc2lem  46388  stoweidlem62  46516  stirlinglem1  46528