Metamath Proof Explorer

Theorem rphalfcl

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

Ref Expression
Assertion rphalfcl 
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )

Proof

Step Hyp Ref Expression
1 2rp 
 |-  2 e. RR+
2 rpdivcl 
 |-  ( ( A e. RR+ /\ 2 e. RR+ ) -> ( A / 2 ) e. RR+ )
3 1 2 mpan2 
 |-  ( A e. RR+ -> ( A / 2 ) e. RR+ )