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	$$⊢\frac{1}{2}=\left(\iota x\in 𝑹|x{+}_{𝑹}x=1_{𝑹}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chalf	$$class\frac{1}{2}$$
1		vx	$$setvarx$$
2		cnr	$$class𝑹$$
3	1	cv	$$setvarx$$
4		cplr	$$class{+}_{𝑹}$$
5	3 3 4	co	$$class\left(x{+}_{𝑹}x\right)$$
6		c1r	$$class{1}_{𝑹}$$
7	5 6	wceq	$$wffx{+}_{𝑹}x=1_{𝑹}$$
8	7 1 2	crio	$$class\left(\iota x\in 𝑹|x{+}_{𝑹}x=1_{𝑹}\right)$$
9	0 8	wceq	$$wff\frac{1}{2}=\left(\iota x\in 𝑹|x{+}_{𝑹}x=1_{𝑹}\right)$$