Metamath Proof Explorer


Theorem intfrac

Description: Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008)

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

Proof

Step Hyp Ref Expression
1 modfrac
 |-  ( A e. RR -> ( A mod 1 ) = ( A - ( |_ ` A ) ) )
2 1 oveq2d
 |-  ( A e. RR -> ( ( |_ ` A ) + ( A mod 1 ) ) = ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) )
3 reflcl
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
4 3 recnd
 |-  ( A e. RR -> ( |_ ` A ) e. CC )
5 recn
 |-  ( A e. RR -> A e. CC )
6 4 5 pncan3d
 |-  ( A e. RR -> ( ( |_ ` A ) + ( A - ( |_ ` A ) ) ) = A )
7 2 6 eqtr2d
 |-  ( A e. RR -> A = ( ( |_ ` A ) + ( A mod 1 ) ) )