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 ) / 𝑁 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑍 + 𝐹 ) ) ) |