Definition df-bj-inftyexpitau 37651

Description: Definition of the auxiliary function +∞e^iτ parameterizing the circle at infinity ℂ_∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 37657. (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 ⊢ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((+∞e^iτ‘𝐴) = (+∞e^iτ‘𝐵) ↔ (𝐴 − 𝐵) ∈ ℤ)). (New usage is discouraged.)

Assertion

Ref	Expression
df-bj-inftyexpitau	⊢ +∞eiτ = (𝑥 ∈ ℝ ↦ ⟨({R‘(1st ‘𝑥)), {R}⟩)

Detailed syntax breakdown of Definition df-bj-inftyexpitau

Step	Hyp	Ref	Expression
1		cinftyexpitau 37650	. 2 class +∞eiτ
2		vx	. . 3 setvar 𝑥
3		cr 11065	. . 3 class ℝ
4	2	cv 1558	. . . . . 6 class 𝑥
5		c1st 7962	. . . . . 6 class 1st
6	4, 5	cfv 6515	. . . . 5 class (1st ‘𝑥)
7		cfractemp 37648	. . . . 5 class {R
8	6, 7	cfv 6515	. . . 4 class ({R‘(1st ‘𝑥))
9		cnr 10816	. . . . 5 class R
10	9	csn 4579	. . . 4 class {R}
11	8, 10	cop 4585	. . 3 class ⟨({R‘(1st ‘𝑥)), {R}⟩
12	2, 3, 11	cmpt 5178	. 2 class (𝑥 ∈ ℝ ↦ ⟨({R‘(1st ‘𝑥)), {R}⟩)
13	1, 12	wceq 1559	1 wff +∞eiτ = (𝑥 ∈ ℝ ↦ ⟨({R‘(1st ‘𝑥)), {R}⟩)

This definition is referenced by:  bj-inftyexpitaufo  37654  bj-inftyexpitaudisj  37657