Step |
Hyp |
Ref |
Expression |
1 |
|
intfrac2.1 |
⊢ 𝑍 = ( ⌊ ‘ 𝐴 ) |
2 |
|
intfrac2.2 |
⊢ 𝐹 = ( 𝐴 − 𝑍 ) |
3 |
|
fracge0 |
⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) |
4 |
1
|
oveq2i |
⊢ ( 𝐴 − 𝑍 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) |
5 |
2 4
|
eqtri |
⊢ 𝐹 = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) |
6 |
3 5
|
breqtrrdi |
⊢ ( 𝐴 ∈ ℝ → 0 ≤ 𝐹 ) |
7 |
|
fraclt1 |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 ) |
8 |
5 7
|
eqbrtrid |
⊢ ( 𝐴 ∈ ℝ → 𝐹 < 1 ) |
9 |
2
|
oveq2i |
⊢ ( 𝑍 + 𝐹 ) = ( 𝑍 + ( 𝐴 − 𝑍 ) ) |
10 |
|
flcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
11 |
1 10
|
eqeltrid |
⊢ ( 𝐴 ∈ ℝ → 𝑍 ∈ ℤ ) |
12 |
11
|
zcnd |
⊢ ( 𝐴 ∈ ℝ → 𝑍 ∈ ℂ ) |
13 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
14 |
12 13
|
pncan3d |
⊢ ( 𝐴 ∈ ℝ → ( 𝑍 + ( 𝐴 − 𝑍 ) ) = 𝐴 ) |
15 |
9 14
|
eqtr2id |
⊢ ( 𝐴 ∈ ℝ → 𝐴 = ( 𝑍 + 𝐹 ) ) |
16 |
6 8 15
|
3jca |
⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = ( 𝑍 + 𝐹 ) ) ) |