Definition df-bj-fractemp 36382

Description: Temporary definition: fractional part of a temporary real.

To understand this definition, recall the canonical injection ω⟶R, 𝑛 ↦ [{𝑥 ∈ Q ∣ 𝑥 <_Q ⟨suc 𝑛, 1_o⟩}, 1_P] ~_R where we successively take the successor of 𝑛 to land in positive integers, then take the couple with 1_o 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 1_P 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

Step	Hyp	Ref	Expression
1		cfractemp 36381	. 2 class {R
2		vx	. . 3 setvar 𝑥
3		cnr 10864	. . 3 class R
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1539	. . . . . . 7 class 𝑦
6		c0r 10865	. . . . . . 7 class 0R
7	5, 6	wceq 1540	. . . . . 6 wff 𝑦 = 0R
8		cltr 10870	. . . . . . . 8 class <R
9	6, 5, 8	wbr 5148	. . . . . . 7 wff 0R <R 𝑦
10		c1r 10866	. . . . . . . 8 class 1R
11	5, 10, 8	wbr 5148	. . . . . . 7 wff 𝑦 <R 1R
12	9, 11	wa 395	. . . . . 6 wff (0R <R 𝑦 ∧ 𝑦 <R 1R)
13	7, 12	wo 844	. . . . 5 wff (𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R))
14		vz	. . . . . . . . . . . . 13 setvar 𝑧
15	14	cv 1539	. . . . . . . . . . . 12 class 𝑧
16		vn	. . . . . . . . . . . . . . 15 setvar 𝑛
17	16	cv 1539	. . . . . . . . . . . . . 14 class 𝑛
18	17	csuc 6366	. . . . . . . . . . . . 13 class suc 𝑛
19		c1o 8463	. . . . . . . . . . . . 13 class 1o
20	18, 19	cop 4634	. . . . . . . . . . . 12 class ⟨suc 𝑛, 1o⟩
21		cltq 10857	. . . . . . . . . . . 12 class <Q
22	15, 20, 21	wbr 5148	. . . . . . . . . . 11 wff 𝑧 <Q ⟨suc 𝑛, 1o⟩
23		cnq 10851	. . . . . . . . . . 11 class Q
24	22, 14, 23	crab 3431	. . . . . . . . . 10 class {𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}
25		c1p 10859	. . . . . . . . . 10 class 1P
26	24, 25	cop 4634	. . . . . . . . 9 class ⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩
27		cer 10863	. . . . . . . . 9 class ~R
28	26, 27	cec 8705	. . . . . . . 8 class [⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
29		cplr 10868	. . . . . . . 8 class +R
30	28, 5, 29	co 7412	. . . . . . 7 class ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦)
31	2	cv 1539	. . . . . . 7 class 𝑥
32	30, 31	wceq 1540	. . . . . 6 wff ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
33		com 7859	. . . . . 6 class ω
34	32, 16, 33	wrex 3069	. . . . 5 wff ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
35	13, 34	wa 395	. . . 4 wff ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)
36	35, 4, 3	crio 7367	. . 3 class (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥))
37	2, 3, 36	cmpt 5231	. 2 class (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
38	1, 37	wceq 1540	1 wff {R = (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))

This definition is referenced by: (None)