Theorem modfrac

Description: The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008)

	Ref	Expression
Assertion	modfrac	|- ( A e. RR -> ( A mod 1 ) = ( A - ( |_ ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		1rp	|- 1 e. RR+
2		modval	|- ( ( A e. RR /\ 1 e. RR+ ) -> ( A mod 1 ) = ( A - ( 1 x. ( |_ ` ( A / 1 ) ) ) ) )
3	1 2	mpan2	|- ( A e. RR -> ( A mod 1 ) = ( A - ( 1 x. ( |_ ` ( A / 1 ) ) ) ) )
4		recn	|- ( A e. RR -> A e. CC )
5	4	div1d	|- ( A e. RR -> ( A / 1 ) = A )
6	5	fveq2d	|- ( A e. RR -> ( |_ ` ( A / 1 ) ) = ( |_ ` A ) )
7	6	oveq2d	|- ( A e. RR -> ( 1 x. ( |_ ` ( A / 1 ) ) ) = ( 1 x. ( |_ ` A ) ) )
8		reflcl	|- ( A e. RR -> ( |_ ` A ) e. RR )
9	8	recnd	|- ( A e. RR -> ( |_ ` A ) e. CC )
10	9	mullidd	|- ( A e. RR -> ( 1 x. ( |_ ` A ) ) = ( |_ ` A ) )
11	7 10	eqtrd	|- ( A e. RR -> ( 1 x. ( |_ ` ( A / 1 ) ) ) = ( |_ ` A ) )
12	11	oveq2d	|- ( A e. RR -> ( A - ( 1 x. ( |_ ` ( A / 1 ) ) ) ) = ( A - ( |_ ` A ) ) )
13	3 12	eqtrd	|- ( A e. RR -> ( A mod 1 ) = ( A - ( |_ ` A ) ) )