This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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