Metamath Proof Explorer


Definition df-bj-fractemp

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

To understand this definition, recall the canonical injection _om --> R. , n |-> [ { x e. Q. | x . } , 1P ] ~R where we successively take the successor of n 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.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfractemp {R
1 vx 𝑥
2 cnr R
3 vy 𝑦
4 3 cv 𝑦
5 c0r 0R
6 4 5 wceq 𝑦 = 0R
7 cltr <R
8 5 4 7 wbr 0R <R 𝑦
9 c1r 1R
10 4 9 7 wbr 𝑦 <R 1R
11 8 10 wa ( 0R <R 𝑦𝑦 <R 1R )
12 6 11 wo ( 𝑦 = 0R ∨ ( 0R <R 𝑦𝑦 <R 1R ) )
13 vn 𝑛
14 com ω
15 vz 𝑧
16 cnq Q
17 15 cv 𝑧
18 cltq <Q
19 13 cv 𝑛
20 19 csuc suc 𝑛
21 c1o 1o
22 20 21 cop ⟨ suc 𝑛 , 1o
23 17 22 18 wbr 𝑧 <Q ⟨ suc 𝑛 , 1o
24 23 15 16 crab { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ }
25 c1p 1P
26 24 25 cop ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P
27 cer ~R
28 26 27 cec [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R
29 cplr +R
30 28 4 29 co ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 )
31 1 cv 𝑥
32 30 31 wceq ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥
33 32 13 14 wrex 𝑛 ∈ ω ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥
34 12 33 wa ( ( 𝑦 = 0R ∨ ( 0R <R 𝑦𝑦 <R 1R ) ) ∧ ∃ 𝑛 ∈ ω ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥 )
35 34 3 2 crio ( 𝑦R ( ( 𝑦 = 0R ∨ ( 0R <R 𝑦𝑦 <R 1R ) ) ∧ ∃ 𝑛 ∈ ω ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥 ) )
36 1 2 35 cmpt ( 𝑥R ↦ ( 𝑦R ( ( 𝑦 = 0R ∨ ( 0R <R 𝑦𝑦 <R 1R ) ) ∧ ∃ 𝑛 ∈ ω ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥 ) ) )
37 0 36 wceq {R = ( 𝑥R ↦ ( 𝑦R ( ( 𝑦 = 0R ∨ ( 0R <R 𝑦𝑦 <R 1R ) ) ∧ ∃ 𝑛 ∈ ω ( [ ⟨ { 𝑧Q𝑧 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R +R 𝑦 ) = 𝑥 ) ) )