Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-inftyexpitau Structured version   Visualization version   GIF version

Definition df-bj-inftyexpitau 36536
Description: Definition of the auxiliary function +∞e parameterizing the circle at infinity in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 36542. (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𝐴) = (+∞e𝐵) ↔ (𝐴𝐵) ∈ ℤ)). (New usage is discouraged.)
Assertion
Ref Expression
df-bj-inftyexpitau +∞e = (𝑥 ∈ ℝ ↦ ⟨({R‘(1st𝑥)), {R}⟩)

Detailed syntax breakdown of Definition df-bj-inftyexpitau
StepHypRef Expression
1 cinftyexpitau 36535 . 2 class +∞e
2 vx . . 3 setvar 𝑥
3 cr 11104 . . 3 class
42cv 1532 . . . . . 6 class 𝑥
5 c1st 7966 . . . . . 6 class 1st
64, 5cfv 6533 . . . . 5 class (1st𝑥)
7 cfractemp 36533 . . . . 5 class {R
86, 7cfv 6533 . . . 4 class ({R‘(1st𝑥))
9 cnr 10855 . . . . 5 class R
109csn 4620 . . . 4 class {R}
118, 10cop 4626 . . 3 class ⟨({R‘(1st𝑥)), {R}⟩
122, 3, 11cmpt 5221 . 2 class (𝑥 ∈ ℝ ↦ ⟨({R‘(1st𝑥)), {R}⟩)
131, 12wceq 1533 1 wff +∞e = (𝑥 ∈ ℝ ↦ ⟨({R‘(1st𝑥)), {R}⟩)
Colors of variables: wff setvar class
This definition is referenced by:  bj-inftyexpitaufo  36539  bj-inftyexpitaudisj  36542
  Copyright terms: Public domain W3C validator