Metamath Proof Explorer


Theorem intfrac2

Description: Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac ? (Contributed by NM, 16-Aug-2008)

Ref Expression
Hypotheses intfrac2.1 𝑍 = ( ⌊ ‘ 𝐴 )
intfrac2.2 𝐹 = ( 𝐴𝑍 )
Assertion intfrac2 ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐹𝐹 < 1 ∧ 𝐴 = ( 𝑍 + 𝐹 ) ) )

Proof

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 ∧ 𝐴 = ( 𝑍 + 𝐹 ) ) )