Metamath Proof Explorer


Definition df-bj-inftyexpitau

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 +∞e = x { R 1 st x 𝑹

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinftyexpitau class +∞e
1 vx setvar x
2 cr class
3 cfractemp class { R
4 c1st class 1 st
5 1 cv setvar x
6 5 4 cfv class 1 st x
7 6 3 cfv class { R 1 st x
8 cnr class 𝑹
9 8 csn class 𝑹
10 7 9 cop class { R 1 st x 𝑹
11 1 2 10 cmpt class x { R 1 st x 𝑹
12 0 11 wceq wff +∞e = x { R 1 st x 𝑹