Metamath Proof Explorer

Theorem intfracq

Description: Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 . (Contributed by NM, 16-Aug-2008)

Ref Expression
Hypotheses intfracq.1 
|- Z = ( |_ ` ( M / N ) )
intfracq.2 
|- F = ( ( M / N ) - Z )
Assertion intfracq 
|- ( ( M e. ZZ /\ N e. NN ) -> ( 0 <_ F /\ F <_ ( ( N - 1 ) / N ) /\ ( M / N ) = ( Z + F ) ) )

Proof

Step Hyp Ref Expression
1 intfracq.1 
 |-  Z = ( |_ ` ( M / N ) )
2 intfracq.2 
 |-  F = ( ( M / N ) - Z )
3 zre 
 |-  ( M e. ZZ -> M e. RR )
4 3 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. RR )
5 nnre 
 |-  ( N e. NN -> N e. RR )
6 5 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. RR )
7 nnne0 
 |-  ( N e. NN -> N =/= 0 )
8 7 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N =/= 0 )
9 4 6 8 redivcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. RR )
10 1 2 intfrac2 
 |-  ( ( M / N ) e. RR -> ( 0 <_ F /\ F < 1 /\ ( M / N ) = ( Z + F ) ) )
11 9 10 syl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( 0 <_ F /\ F < 1 /\ ( M / N ) = ( Z + F ) ) )
12 11 simp1d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> 0 <_ F )
13 fraclt1 
 |-  ( ( M / N ) e. RR -> ( ( M / N ) - ( |_ ` ( M / N ) ) ) < 1 )
14 9 13 syl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M / N ) - ( |_ ` ( M / N ) ) ) < 1 )
15 1 oveq2i 
 |-  ( ( M / N ) - Z ) = ( ( M / N ) - ( |_ ` ( M / N ) ) )
16 2 15 eqtri 
 |-  F = ( ( M / N ) - ( |_ ` ( M / N ) ) )
17 16 a1i 
 |-  ( ( M e. ZZ /\ N e. NN ) -> F = ( ( M / N ) - ( |_ ` ( M / N ) ) ) )
18 nncn 
 |-  ( N e. NN -> N e. CC )
19 18 7 dividd 
 |-  ( N e. NN -> ( N / N ) = 1 )
20 19 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N / N ) = 1 )
21 14 17 20 3brtr4d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> F < ( N / N ) )
22 reflcl 
 |-  ( ( M / N ) e. RR -> ( |_ ` ( M / N ) ) e. RR )
23 9 22 syl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. RR )
24 1 23 eqeltrid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> Z e. RR )
25 9 24 resubcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M / N ) - Z ) e. RR )
26 2 25 eqeltrid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> F e. RR )
27 nngt0 
 |-  ( N e. NN -> 0 < N )
28 5 27 jca 
 |-  ( N e. NN -> ( N e. RR /\ 0 < N ) )
29 28 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N e. RR /\ 0 < N ) )
30 ltmuldiv2 
 |-  ( ( F e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( N x. F ) < N <-> F < ( N / N ) ) )
31 26 6 29 30 syl3anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( N x. F ) < N <-> F < ( N / N ) ) )
32 21 31 mpbird 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. F ) < N )
33 2 oveq2i 
 |-  ( N x. F ) = ( N x. ( ( M / N ) - Z ) )
34 18 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. CC )
35 9 recnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. CC )
36 9 flcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( |_ ` ( M / N ) ) e. ZZ )
37 1 36 eqeltrid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> Z e. ZZ )
38 37 zcnd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> Z e. CC )
39 34 35 38 subdid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. ( ( M / N ) - Z ) ) = ( ( N x. ( M / N ) ) - ( N x. Z ) ) )
40 33 39 syl5eq 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. F ) = ( ( N x. ( M / N ) ) - ( N x. Z ) ) )
41 zcn 
 |-  ( M e. ZZ -> M e. CC )
42 41 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. CC )
43 42 34 8 divcan2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. ( M / N ) ) = M )
44 simpl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. ZZ )
45 43 44 eqeltrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. ( M / N ) ) e. ZZ )
46 nnz 
 |-  ( N e. NN -> N e. ZZ )
47 46 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. ZZ )
48 47 37 zmulcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. Z ) e. ZZ )
49 45 48 zsubcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( N x. ( M / N ) ) - ( N x. Z ) ) e. ZZ )
50 40 49 eqeltrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. F ) e. ZZ )
51 zltlem1 
 |-  ( ( ( N x. F ) e. ZZ /\ N e. ZZ ) -> ( ( N x. F ) < N <-> ( N x. F ) <_ ( N - 1 ) ) )
52 50 47 51 syl2anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( N x. F ) < N <-> ( N x. F ) <_ ( N - 1 ) ) )
53 32 52 mpbid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. F ) <_ ( N - 1 ) )
54 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
55 5 54 syl 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
56 55 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N - 1 ) e. RR )
57 lemuldiv2 
 |-  ( ( F e. RR /\ ( N - 1 ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( N x. F ) <_ ( N - 1 ) <-> F <_ ( ( N - 1 ) / N ) ) )
58 26 56 29 57 syl3anc 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( N x. F ) <_ ( N - 1 ) <-> F <_ ( ( N - 1 ) / N ) ) )
59 53 58 mpbid 
 |-  ( ( M e. ZZ /\ N e. NN ) -> F <_ ( ( N - 1 ) / N ) )
60 11 simp3d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) = ( Z + F ) )
61 12 59 60 3jca 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( 0 <_ F /\ F <_ ( ( N - 1 ) / N ) /\ ( M / N ) = ( Z + F ) ) )