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