![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-inftyexpitau | Structured version Visualization version GIF version |
Description: Definition of the auxiliary function +∞eiτ 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 ⊢ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((+∞eiτ‘𝐴) = (+∞eiτ‘𝐵) ↔ (𝐴 − 𝐵) ∈ ℤ)). (New usage is discouraged.) |
Ref | Expression |
---|---|
df-bj-inftyexpitau | ⊢ +∞eiτ = (𝑥 ∈ ℝ ↦ 〈({R‘(1st ‘𝑥)), {R}〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cinftyexpitau 36535 | . 2 class +∞eiτ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cr 11104 | . . 3 class ℝ | |
4 | 2 | cv 1532 | . . . . . 6 class 𝑥 |
5 | c1st 7966 | . . . . . 6 class 1st | |
6 | 4, 5 | cfv 6533 | . . . . 5 class (1st ‘𝑥) |
7 | cfractemp 36533 | . . . . 5 class {R | |
8 | 6, 7 | cfv 6533 | . . . 4 class ({R‘(1st ‘𝑥)) |
9 | cnr 10855 | . . . . 5 class R | |
10 | 9 | csn 4620 | . . . 4 class {R} |
11 | 8, 10 | cop 4626 | . . 3 class 〈({R‘(1st ‘𝑥)), {R}〉 |
12 | 2, 3, 11 | cmpt 5221 | . 2 class (𝑥 ∈ ℝ ↦ 〈({R‘(1st ‘𝑥)), {R}〉) |
13 | 1, 12 | wceq 1533 | 1 wff +∞eiτ = (𝑥 ∈ ℝ ↦ 〈({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 |