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 ⊢ Z = A
intfrac2.2 ⊢ F = A − Z
Assertion intfrac2 ⊢ A ∈ ℝ → 0 ≤ F ∧ F < 1 ∧ A = Z + F

Proof

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