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 ) ) ) |
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 ) ) ) |