Description: Define the temporary real "one-half". Once the machinery is developed, the real number "one-half" is commonly denoted by ( 1 / 2 ) . (Contributed by BJ, 4-Feb-2023) (New usage is discouraged.)
TODO:
$p |- 1/2 e. R. $= ? $. ( riotacl )
$p |- -. 0R = 1/2 $= ? $. (since -. ( 0R +R 0R ) = 1R )
$p |- 0R $p |- 1/2 $p |- ( {R `0R ) = 0R $= ? $. $p |- ( {R1/2 ) = 1/2 $= ? $. df-minfty $a |- minfty = ( inftyexpitau` <. 1/2 , 0R >. ) $.
Ref
Expression
Assertion
df-bj-onehalf
|- 1/2 = ( iota_ x e. R. ( x +R x ) = 1R )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
chalf
|- 1/2
1
vx
|- x
2
cnr
|- R.
3
1
cv
|- x
4
cplr
|- +R
5
3 3 4
co
|- ( x +R x )
6
c1r
|- 1R
7
5 6
wceq
|- ( x +R x ) = 1R
8
7 1 2
crio
|- ( iota_ x e. R. ( x +R x ) = 1R )
9
0 8
wceq
|- 1/2 = ( iota_ x e. R. ( x +R x ) = 1R )