This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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