Description: Definition of the auxiliary function inftyexpitau parameterizing the circle at infinity CCinfty in CCbar . We use coupling with { R. } to simplify the proof of bj-inftyexpitaudisj . (Contributed by BJ, 22-Jan-2023) The precise definition is irrelevant and should generally not be used. TODO: prove only the necessary lemmas to prove |- ( A e. RR /\ B e. RR ) -> ( ( inftyexpitauA ) = ( inftyexpitauB ) <-> ( A - B ) e. ZZ ) ) . (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-bj-inftyexpitau | |- inftyexpitau = ( x e. RR |-> <. ( {R ` ( 1st ` x ) ) , { R. } >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cinftyexpitau | |- inftyexpitau |
|
| 1 | vx | |- x |
|
| 2 | cr | |- RR |
|
| 3 | cfractemp | |- {R |
|
| 4 | c1st | |- 1st |
|
| 5 | 1 | cv | |- x |
| 6 | 5 4 | cfv | |- ( 1st ` x ) |
| 7 | 6 3 | cfv | |- ( {R ` ( 1st ` x ) ) |
| 8 | cnr | |- R. |
|
| 9 | 8 | csn | |- { R. } |
| 10 | 7 9 | cop | |- <. ( {R ` ( 1st ` x ) ) , { R. } >. |
| 11 | 1 2 10 | cmpt | |- ( x e. RR |-> <. ( {R ` ( 1st ` x ) ) , { R. } >. ) |
| 12 | 0 11 | wceq | |- inftyexpitau = ( x e. RR |-> <. ( {R ` ( 1st ` x ) ) , { R. } >. ) |