Definition df-bj-fractemp 36078

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 36077	. 2 class {R
2		vx	. . 3 setvar 𝑥
3		cnr 10860	. . 3 class R
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1541	. . . . . . 7 class 𝑦
6		c0r 10861	. . . . . . 7 class 0R
7	5, 6	wceq 1542	. . . . . 6 wff 𝑦 = 0R
8		cltr 10866	. . . . . . . 8 class <R
9	6, 5, 8	wbr 5149	. . . . . . 7 wff 0R <R 𝑦
10		c1r 10862	. . . . . . . 8 class 1R
11	5, 10, 8	wbr 5149	. . . . . . 7 wff 𝑦 <R 1R
12	9, 11	wa 397	. . . . . 6 wff (0R <R 𝑦 ∧ 𝑦 <R 1R)
13	7, 12	wo 846	. . . . 5 wff (𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R))
14		vz	. . . . . . . . . . . . 13 setvar 𝑧
15	14	cv 1541	. . . . . . . . . . . 12 class 𝑧
16		vn	. . . . . . . . . . . . . . 15 setvar 𝑛
17	16	cv 1541	. . . . . . . . . . . . . 14 class 𝑛
18	17	csuc 6367	. . . . . . . . . . . . 13 class suc 𝑛
19		c1o 8459	. . . . . . . . . . . . 13 class 1o
20	18, 19	cop 4635	. . . . . . . . . . . 12 class ⟨suc 𝑛, 1o⟩
21		cltq 10853	. . . . . . . . . . . 12 class <Q
22	15, 20, 21	wbr 5149	. . . . . . . . . . 11 wff 𝑧 <Q ⟨suc 𝑛, 1o⟩
23		cnq 10847	. . . . . . . . . . 11 class Q
24	22, 14, 23	crab 3433	. . . . . . . . . 10 class {𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}
25		c1p 10855	. . . . . . . . . 10 class 1P
26	24, 25	cop 4635	. . . . . . . . 9 class ⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩
27		cer 10859	. . . . . . . . 9 class ~R
28	26, 27	cec 8701	. . . . . . . 8 class [⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
29		cplr 10864	. . . . . . . 8 class +R
30	28, 5, 29	co 7409	. . . . . . 7 class ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦)
31	2	cv 1541	. . . . . . 7 class 𝑥
32	30, 31	wceq 1542	. . . . . 6 wff ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
33		com 7855	. . . . . 6 class ω
34	32, 16, 33	wrex 3071	. . . . 5 wff ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥
35	13, 34	wa 397	. . . 4 wff ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)
36	35, 4, 3	crio 7364	. . 3 class (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥))
37	2, 3, 36	cmpt 5232	. 2 class (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
38	1, 37	wceq 1542	1 wff {R = (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))

This definition is referenced by: (None)