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 37140
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 37139 . 2 class {R
2 vx . . 3 setvar 𝑥
3 cnr 10896 . . 3 class R
4 vy . . . . . . . 8 setvar 𝑦
54cv 1534 . . . . . . 7 class 𝑦
6 c0r 10897 . . . . . . 7 class 0R
75, 6wceq 1535 . . . . . 6 wff 𝑦 = 0R
8 cltr 10902 . . . . . . . 8 class <R
96, 5, 8wbr 5149 . . . . . . 7 wff 0R <R 𝑦
10 c1r 10898 . . . . . . . 8 class 1R
115, 10, 8wbr 5149 . . . . . . 7 wff 𝑦 <R 1R
129, 11wa 395 . . . . . 6 wff (0R <R 𝑦𝑦 <R 1R)
137, 12wo 846 . . . . 5 wff (𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R))
14 vz . . . . . . . . . . . . 13 setvar 𝑧
1514cv 1534 . . . . . . . . . . . 12 class 𝑧
16 vn . . . . . . . . . . . . . . 15 setvar 𝑛
1716cv 1534 . . . . . . . . . . . . . 14 class 𝑛
1817csuc 6382 . . . . . . . . . . . . 13 class suc 𝑛
19 c1o 8492 . . . . . . . . . . . . 13 class 1o
2018, 19cop 4636 . . . . . . . . . . . 12 class ⟨suc 𝑛, 1o
21 cltq 10889 . . . . . . . . . . . 12 class <Q
2215, 20, 21wbr 5149 . . . . . . . . . . 11 wff 𝑧 <Q ⟨suc 𝑛, 1o
23 cnq 10883 . . . . . . . . . . 11 class Q
2422, 14, 23crab 3432 . . . . . . . . . 10 class {𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}
25 c1p 10891 . . . . . . . . . 10 class 1P
2624, 25cop 4636 . . . . . . . . 9 class ⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P
27 cer 10895 . . . . . . . . 9 class ~R
2826, 27cec 8736 . . . . . . . 8 class [⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
29 cplr 10900 . . . . . . . 8 class +R
3028, 5, 29co 7425 . . . . . . 7 class ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦)
312cv 1534 . . . . . . 7 class 𝑥
3230, 31wceq 1535 . . . . . 6 wff ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
33 com 7880 . . . . . 6 class ω
3432, 16, 33wrex 3066 . . . . 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 7380 . . 3 class (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥))
372, 3, 36cmpt 5232 . 2 class (𝑥R ↦ (𝑦R ((𝑦 = 0R ∨ (0R <R 𝑦𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧Q𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
381, 37wceq 1535 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