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	$$⊢{\mathrm{+\infty e}}^{i\tau }=\left(x\in ℝ⟼⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinftyexpitau	$$class{\mathrm{+\infty e}}^{i\tau }$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		cfractemp	$$class{\{}_R$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarx$$
6	5 4	cfv	$$class{1}^{st}\left(x\right)$$
7	6 3	cfv	$$class{\{}_R\left(1^{st}\left(x\right)\right)$$
8		cnr	$$class𝑹$$
9	8	csn	$$class\left\{𝑹\right\}$$
10	7 9	cop	$$class⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩$$
11	1 2 10	cmpt	$$class\left(x\in ℝ⟼⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\right)$$
12	0 11	wceq	$$wff{\mathrm{+\infty e}}^{i\tau }=\left(x\in ℝ⟼⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\right)$$