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