Metamath Proof Explorer

Theorem rphalfcld

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

Ref Expression
Hypothesis rpred.1 
|- ( ph -> A e. RR+ )
Assertion rphalfcld 
|- ( ph -> ( A / 2 ) e. RR+ )

Proof

Step Hyp Ref Expression
1 rpred.1 
 |-  ( ph -> A e. RR+ )
2 rphalfcl 
 |-  ( A e. RR+ -> ( A / 2 ) e. RR+ )
3 1 2 syl 
 |-  ( ph -> ( A / 2 ) e. RR+ )