Metamath Proof Explorer


Theorem rehalfcli

Description: Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypothesis rehalfcli.1 A
Assertion rehalfcli A 2

Proof

Step Hyp Ref Expression
1 rehalfcli.1 A
2 rehalfcl A A 2
3 1 2 ax-mp A 2