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 N 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 M
4 3 adantr M N M
5 nnre N N
6 5 adantl M N N
7 nnne0 N N 0
8 7 adantl M N N 0
9 4 6 8 redivcld M N M N
10 1 2 intfrac2 M N 0 F F < 1 M N = Z + F
11 9 10 syl M N 0 F F < 1 M N = Z + F
12 11 simp1d M N 0 F
13 fraclt1 M N M N M N < 1
14 9 13 syl M N 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 N F = M N M N
18 nncn N N
19 18 7 dividd N N N = 1
20 19 adantl M N N N = 1
21 14 17 20 3brtr4d M N F < N N
22 reflcl M N M N
23 9 22 syl M N M N
24 1 23 eqeltrid M N Z
25 9 24 resubcld M N M N Z
26 2 25 eqeltrid M N F
27 nngt0 N 0 < N
28 5 27 jca N N 0 < N
29 28 adantl M N N 0 < N
30 ltmuldiv2 F N N 0 < N N F < N F < N N
31 26 6 29 30 syl3anc M N N F < N F < N N
32 21 31 mpbird M N N F < N
33 2 oveq2i N F = N M N Z
34 18 adantl M N N
35 9 recnd M N M N
36 9 flcld M N M N
37 1 36 eqeltrid M N Z
38 37 zcnd M N Z
39 34 35 38 subdid M N N M N Z = N M N N Z
40 33 39 eqtrid M N N F = N M N N Z
41 zcn M M
42 41 adantr M N M
43 42 34 8 divcan2d M N N M N = M
44 simpl M N M
45 43 44 eqeltrd M N N M N
46 nnz N N
47 46 adantl M N N
48 47 37 zmulcld M N N Z
49 45 48 zsubcld M N N M N N Z
50 40 49 eqeltrd M N N F
51 zltlem1 N F N N F < N N F N 1
52 50 47 51 syl2anc M N N F < N N F N 1
53 32 52 mpbid M N N F N 1
54 peano2rem N N 1
55 5 54 syl N N 1
56 55 adantl M N N 1
57 lemuldiv2 F N 1 N 0 < N N F N 1 F N 1 N
58 26 56 29 57 syl3anc M N N F N 1 F N 1 N
59 53 58 mpbid M N F N 1 N
60 11 simp3d M N M N = Z + F
61 12 59 60 3jca M N 0 F F N 1 N M N = Z + F