Description: Temporary definition: fractional part of a temporary real.
To understand this definition, recall the canonical injection
_om --> R. ,
n |-> [ { x e. Q. | x . } , 1P ] ~R
where we
successively take the successor of n to land in positive integers,
then take the couple with 1o as second component to land in positive
rationals, then take the Dedekind cut that positive rational forms, and
finally take the equivalence class of the couple with 1P as second
component. Adding one at the beginning and subtracting it at the end is
necessary since the constructions used in set.mm use the positive
integers, positive rationals, and positive reals as intermediate number
systems. (Contributed by BJ, 22-Jan-2023) The precise definition is
irrelevant and should generally not be used. One could even inline it.
The definitive fractional part of an extended or projective complex
number will be defined later. (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | df-bj-fractemp | |- {R = ( x e. R. |-> ( iota_ y e. R. ( ( y = 0R \/ ( 0R |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfractemp | |- {R |
|
1 | vx | |- x |
|
2 | cnr | |- R. |
|
3 | vy | |- y |
|
4 | 3 | cv | |- y |
5 | c0r | |- 0R |
|
6 | 4 5 | wceq | |- y = 0R |
7 | cltr | |- |
|
8 | 5 4 7 | wbr | |- 0R |
9 | c1r | |- 1R |
|
10 | 4 9 7 | wbr | |- y |
11 | 8 10 | wa | |- ( 0R |
12 | 6 11 | wo | |- ( y = 0R \/ ( 0R |
13 | vn | |- n |
|
14 | com | |- _om |
|
15 | vz | |- z |
|
16 | cnq | |- Q. |
|
17 | 15 | cv | |- z |
18 | cltq | |- |
|
19 | 13 | cv | |- n |
20 | 19 | csuc | |- suc n |
21 | c1o | |- 1o |
|
22 | 20 21 | cop | |- <. suc n , 1o >. |
23 | 17 22 18 | wbr | |- z. |
24 | 23 15 16 | crab | |- { z e. Q. | z. } |
25 | c1p | |- 1P |
|
26 | 24 25 | cop | |- <. { z e. Q. | z. } , 1P >. |
27 | cer | |- ~R |
|
28 | 26 27 | cec | |- [ <. { z e. Q. | z. } , 1P >. ] ~R |
29 | cplr | |- +R |
|
30 | 28 4 29 | co | |- ( [ <. { z e. Q. | z. } , 1P >. ] ~R +R y ) |
31 | 1 | cv | |- x |
32 | 30 31 | wceq | |- ( [ <. { z e. Q. | z. } , 1P >. ] ~R +R y ) = x |
33 | 32 13 14 | wrex | |- E. n e. _om ( [ <. { z e. Q. | z. } , 1P >. ] ~R +R y ) = x |
34 | 12 33 | wa | |- ( ( y = 0R \/ ( 0R |
35 | 34 3 2 | crio | |- ( iota_ y e. R. ( ( y = 0R \/ ( 0R |
36 | 1 2 35 | cmpt | |- ( x e. R. |-> ( iota_ y e. R. ( ( y = 0R \/ ( 0R |
37 | 0 36 | wceq | |- {R = ( x e. R. |-> ( iota_ y e. R. ( ( y = 0R \/ ( 0R |