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 𝑍 = ( ⌊ ‘ ( 𝑀 / 𝑁 ) )
intfracq.2 𝐹 = ( ( 𝑀 / 𝑁 ) − 𝑍 )
Assertion intfracq ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 intfracq.1 𝑍 = ( ⌊ ‘ ( 𝑀 / 𝑁 ) )
2 intfracq.2 𝐹 = ( ( 𝑀 / 𝑁 ) − 𝑍 )
3 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4 3 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℝ )
5 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
6 5 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
7 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
8 7 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
9 4 6 8 redivcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
10 1 2 intfrac2 ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( 0 ≤ 𝐹𝐹 < 1 ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )
11 9 10 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹𝐹 < 1 ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )
12 11 simp1d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 0 ≤ 𝐹 )
13 fraclt1 ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) < 1 )
14 9 13 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) < 1 )
15 1 oveq2i ( ( 𝑀 / 𝑁 ) − 𝑍 ) = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
16 2 15 eqtri 𝐹 = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) )
17 16 a1i ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 = ( ( 𝑀 / 𝑁 ) − ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ) )
18 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
19 18 7 dividd ( 𝑁 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
20 19 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / 𝑁 ) = 1 )
21 14 17 20 3brtr4d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 < ( 𝑁 / 𝑁 ) )
22 reflcl ( ( 𝑀 / 𝑁 ) ∈ ℝ → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℝ )
23 9 22 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℝ )
24 1 23 eqeltrid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℝ )
25 9 24 resubcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 / 𝑁 ) − 𝑍 ) ∈ ℝ )
26 2 25 eqeltrid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 ∈ ℝ )
27 nngt0 ( 𝑁 ∈ ℕ → 0 < 𝑁 )
28 5 27 jca ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
29 28 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
30 ltmuldiv2 ( ( 𝐹 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑁 · 𝐹 ) < 𝑁𝐹 < ( 𝑁 / 𝑁 ) ) )
31 26 6 29 30 syl3anc ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) < 𝑁𝐹 < ( 𝑁 / 𝑁 ) ) )
32 21 31 mpbird ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) < 𝑁 )
33 2 oveq2i ( 𝑁 · 𝐹 ) = ( 𝑁 · ( ( 𝑀 / 𝑁 ) − 𝑍 ) )
34 18 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
35 9 recnd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) ∈ ℂ )
36 9 flcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑀 / 𝑁 ) ) ∈ ℤ )
37 1 36 eqeltrid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℤ )
38 37 zcnd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑍 ∈ ℂ )
39 34 35 38 subdid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( ( 𝑀 / 𝑁 ) − 𝑍 ) ) = ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) )
40 33 39 eqtrid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) = ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) )
41 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
42 41 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℂ )
43 42 34 8 divcan2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) = 𝑀 )
44 simpl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℤ )
45 43 44 eqeltrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · ( 𝑀 / 𝑁 ) ) ∈ ℤ )
46 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
47 46 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
48 47 37 zmulcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑍 ) ∈ ℤ )
49 45 48 zsubcld ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · ( 𝑀 / 𝑁 ) ) − ( 𝑁 · 𝑍 ) ) ∈ ℤ )
50 40 49 eqeltrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) ∈ ℤ )
51 zltlem1 ( ( ( 𝑁 · 𝐹 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
52 50 47 51 syl2anc ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) < 𝑁 ↔ ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
53 32 52 mpbid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) )
54 peano2rem ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
55 5 54 syl ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
56 55 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℝ )
57 lemuldiv2 ( ( 𝐹 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ↔ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ) )
58 26 56 29 57 syl3anc ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 · 𝐹 ) ≤ ( 𝑁 − 1 ) ↔ 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ) )
59 53 58 mpbid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) )
60 11 simp3d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) )
61 12 59 60 3jca ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 0 ≤ 𝐹𝐹 ≤ ( ( 𝑁 − 1 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) )