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 e. RR -> ( 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 e. RR -> 0 <_ ( A - ( |_ ` A ) ) )
4 1 oveq2i
 |-  ( A - Z ) = ( A - ( |_ ` A ) )
5 2 4 eqtri
 |-  F = ( A - ( |_ ` A ) )
6 3 5 breqtrrdi
 |-  ( A e. RR -> 0 <_ F )
7 fraclt1
 |-  ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )
8 5 7 eqbrtrid
 |-  ( A e. RR -> F < 1 )
9 2 oveq2i
 |-  ( Z + F ) = ( Z + ( A - Z ) )
10 flcl
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
11 1 10 eqeltrid
 |-  ( A e. RR -> Z e. ZZ )
12 11 zcnd
 |-  ( A e. RR -> Z e. CC )
13 recn
 |-  ( A e. RR -> A e. CC )
14 12 13 pncan3d
 |-  ( A e. RR -> ( Z + ( A - Z ) ) = A )
15 9 14 eqtr2id
 |-  ( A e. RR -> A = ( Z + F ) )
16 6 8 15 3jca
 |-  ( A e. RR -> ( 0 <_ F /\ F < 1 /\ A = ( Z + F ) ) )