Metamath Proof Explorer


Definition df-bj-onehalf

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 = ι x 𝑹 | x + 𝑹 x = 1 𝑹

Detailed syntax breakdown

Step Hyp Ref Expression
0 chalf class 1 2
1 vx setvar x
2 cnr class 𝑹
3 1 cv setvar x
4 cplr class + 𝑹
5 3 3 4 co class x + 𝑹 x
6 c1r class 1 𝑹
7 5 6 wceq wff x + 𝑹 x = 1 𝑹
8 7 1 2 crio class ι x 𝑹 | x + 𝑹 x = 1 𝑹
9 0 8 wceq wff 1 2 = ι x 𝑹 | x + 𝑹 x = 1 𝑹