Database
REAL AND COMPLEX NUMBERS
Integer sets
Simple number properties
rehalfcli
Next ⟩
lt2addmuld
Metamath Proof Explorer
Ascii
Unicode
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
∈
ℝ