Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-onehalf Structured version   Visualization version   GIF version

Definition df-bj-onehalf 34567
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 7125)

$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
StepHypRef Expression
1 chalf 34566 . 2 class 1/2
2 vx . . . . . 6 setvar 𝑥
32cv 1537 . . . . 5 class 𝑥
4 cplr 10290 . . . . 5 class +R
53, 3, 4co 7150 . . . 4 class (𝑥 +R 𝑥)
6 c1r 10288 . . . 4 class 1R
75, 6wceq 1538 . . 3 wff (𝑥 +R 𝑥) = 1R
8 cnr 10286 . . 3 class R
97, 2, 8crio 7107 . 2 class (𝑥R (𝑥 +R 𝑥) = 1R)
101, 9wceq 1538 1 wff 1/2 = (𝑥R (𝑥 +R 𝑥) = 1R)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator