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

Definition df-bj-fractemp 37191
Description: Temporary definition: fractional part of a temporary real.

To understand this definition, recall the canonical injection ω⟶R, 𝑛 ↦ [{𝑥Q𝑥 <Q ⟨suc 𝑛, 1o⟩}, 1P] ~R where we successively take the successor of 𝑛 to land in positive integers, then take the couple with 1o as second component to land in positive rationals, then take the Dedekind cut that positive rational forms, and finally take the equivalence class of the couple with 1P as second component. Adding one at the beginning and subtracting it at the end is necessary since the constructions used in set.mm use the positive integers, positive rationals, and positive reals as intermediate number systems. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. One could even inline it. The definitive fractional part of an extended or projective complex number will be defined later. (New usage is discouraged.)

Assertion
Ref Expression
df-bj-fractemp {R = (𝑥R ↦ (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑛

Detailed syntax breakdown of Definition df-bj-fractemp
StepHypRef Expression
1 cfractemp 37190 . 2 class {R
2 vx . . 3 setvar 𝑥
3 cnr 10901 . . 3 class R
4 vy . . . . . . . 8 setvar 𝑦
54cv 1539 . . . . . . 7 class 𝑦
6 c0r 10902 . . . . . . 7 class 0R
75, 6wceq 1540 . . . . . 6 wff 𝑦 = 0R
8 cltr 10907 . . . . . . . 8 class <R
96, 5, 8wbr 5141 . . . . . . 7 wff 0R <R 𝑦
10 c1r 10903 . . . . . . . 8 class 1R
115, 10, 8wbr 5141 . . . . . . 7 wff 𝑦 <R 1R
129, 11wa 395 . . . . . 6 wff (0R <R 𝑦𝑦 <R 1R)
137, 12wo 848 . . . . 5 wff (𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R))
14 vz . . . . . . . . . . . . 13 setvar 𝑧
1514cv 1539 . . . . . . . . . . . 12 class 𝑧
16 vn . . . . . . . . . . . . . . 15 setvar 𝑛
1716cv 1539 . . . . . . . . . . . . . 14 class 𝑛
1817csuc 6384 . . . . . . . . . . . . 13 class suc 𝑛
19 c1o 8495 . . . . . . . . . . . . 13 class 1o
2018, 19cop 4630 . . . . . . . . . . . 12 class ⟨suc 𝑛, 1o
21 cltq 10894 . . . . . . . . . . . 12 class <Q
2215, 20, 21wbr 5141 . . . . . . . . . . 11 wff 𝑧 <Q ⟨suc 𝑛, 1o
23 cnq 10888 . . . . . . . . . . 11 class Q
2422, 14, 23crab 3435 . . . . . . . . . 10 class {𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}
25 c1p 10896 . . . . . . . . . 10 class 1P
2624, 25cop 4630 . . . . . . . . 9 class ⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P
27 cer 10900 . . . . . . . . 9 class ~R
2826, 27cec 8739 . . . . . . . 8 class [⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
29 cplr 10905 . . . . . . . 8 class +R
3028, 5, 29co 7429 . . . . . . 7 class ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦)
312cv 1539 . . . . . . 7 class 𝑥
3230, 31wceq 1540 . . . . . 6 wff ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
33 com 7883 . . . . . 6 class ω
3432, 16, 33wrex 3069 . . . . 5 wff 𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
3513, 34wa 395 . . . 4 wff ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)
3635, 4, 3crio 7385 . . 3 class (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥))
372, 3, 36cmpt 5223 . 2 class (𝑥R ↦ (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
381, 37wceq 1540 1 wff {R = (𝑥R ↦ (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator