Definition df-bj-onehalf 35302

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 7230)

$p |- -. 0R = 1/2 $= ? $. (since -. ( 0R +R 0R ) = 1R )

$p |- 0R <R 1/2 $= ? $.

$p |- 1/2 <R 1R $= ? $.

$p |- ( {R ` 0R ) = 0R $= ? $.

$p |- ( {R ` 1/2 ) = 1/2 $= ? $.

df-minfty $a |- minfty = ( inftyexpitau ` <. 1/2 , 0R >. ) $.

Assertion

Ref	Expression
df-bj-onehalf	⊢ 1/2 = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)

Detailed syntax breakdown of Definition df-bj-onehalf

Step	Hyp	Ref	Expression
1		chalf 35301	. 2 class 1/2
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1538	. . . . 5 class 𝑥
4		cplr 10556	. . . . 5 class +R
5	3, 3, 4	co 7255	. . . 4 class (𝑥 +R 𝑥)
6		c1r 10554	. . . 4 class 1R
7	5, 6	wceq 1539	. . 3 wff (𝑥 +R 𝑥) = 1R
8		cnr 10552	. . 3 class R
9	7, 2, 8	crio 7211	. 2 class (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)
10	1, 9	wceq 1539	1 wff 1/2 = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)

This definition is referenced by: (None)