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	syl5req	|- ( A e. RR -> A = ( Z + F ) )
16	6 8 15	3jca	|- ( A e. RR -> ( 0 <_ F /\ F < 1 /\ A = ( Z + F ) ) )