Proof of Theorem intfracq
| Step | Hyp | Ref
| Expression |
| 1 | | zre 12617 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
| 3 | | nnre 12273 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 4 | 3 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 5 | | nnne0 12300 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 6 | 5 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
| 7 | 2, 4, 6 | redivcld 12095 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
| 8 | | intfracq.1 |
. . . . 5
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁)) |
| 9 | | intfracq.2 |
. . . . 5
⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍) |
| 10 | 8, 9 | intfrac2 13898 |
. . . 4
⊢ ((𝑀 / 𝑁) ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |
| 11 | 7, 10 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤
𝐹 ∧ 𝐹 < 1 ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |
| 12 | 11 | simp1d 1143 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝐹) |
| 13 | | fraclt1 13842 |
. . . . . . 7
⊢ ((𝑀 / 𝑁) ∈ ℝ → ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) < 1) |
| 14 | 7, 13 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) < 1) |
| 15 | 8 | oveq2i 7442 |
. . . . . . . 8
⊢ ((𝑀 / 𝑁) − 𝑍) = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) |
| 16 | 9, 15 | eqtri 2765 |
. . . . . . 7
⊢ 𝐹 = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) |
| 17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁)))) |
| 18 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 19 | 18, 5 | dividd 12041 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 / 𝑁) = 1) |
| 20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1) |
| 21 | 14, 17, 20 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 < (𝑁 / 𝑁)) |
| 22 | | reflcl 13836 |
. . . . . . . . . 10
⊢ ((𝑀 / 𝑁) ∈ ℝ →
(⌊‘(𝑀 / 𝑁)) ∈
ℝ) |
| 23 | 7, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℝ) |
| 24 | 8, 23 | eqeltrid 2845 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℝ) |
| 25 | 7, 24 | resubcld 11691 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − 𝑍) ∈ ℝ) |
| 26 | 9, 25 | eqeltrid 2845 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 ∈
ℝ) |
| 27 | | nngt0 12297 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 28 | 3, 27 | jca 511 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
| 30 | | ltmuldiv2 12142 |
. . . . . 6
⊢ ((𝐹 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝑁 · 𝐹) < 𝑁 ↔ 𝐹 < (𝑁 / 𝑁))) |
| 31 | 26, 4, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) < 𝑁 ↔ 𝐹 < (𝑁 / 𝑁))) |
| 32 | 21, 31 | mpbird 257 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) < 𝑁) |
| 33 | 9 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑁 · 𝐹) = (𝑁 · ((𝑀 / 𝑁) − 𝑍)) |
| 34 | 18 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
| 35 | 7 | recnd 11289 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ) |
| 36 | 7 | flcld 13838 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
| 37 | 8, 36 | eqeltrid 2845 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℤ) |
| 38 | 37 | zcnd 12723 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℂ) |
| 39 | 34, 35, 38 | subdid 11719 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · ((𝑀 / 𝑁) − 𝑍)) = ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍))) |
| 40 | 33, 39 | eqtrid 2789 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) = ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍))) |
| 41 | | zcn 12618 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
| 42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
| 43 | 42, 34, 6 | divcan2d 12045 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) = 𝑀) |
| 44 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
| 45 | 43, 44 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) ∈ ℤ) |
| 46 | | nnz 12634 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
| 48 | 47, 37 | zmulcld 12728 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝑍) ∈ ℤ) |
| 49 | 45, 48 | zsubcld 12727 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍)) ∈ ℤ) |
| 50 | 40, 49 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) ∈ ℤ) |
| 51 | | zltlem1 12670 |
. . . . 5
⊢ (((𝑁 · 𝐹) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 · 𝐹) < 𝑁 ↔ (𝑁 · 𝐹) ≤ (𝑁 − 1))) |
| 52 | 50, 47, 51 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) < 𝑁 ↔ (𝑁 · 𝐹) ≤ (𝑁 − 1))) |
| 53 | 32, 52 | mpbid 232 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) ≤ (𝑁 − 1)) |
| 54 | | peano2rem 11576 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
| 55 | 3, 54 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
| 56 | 55 | adantl 481 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℝ) |
| 57 | | lemuldiv2 12149 |
. . . 4
⊢ ((𝐹 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝑁 · 𝐹) ≤ (𝑁 − 1) ↔ 𝐹 ≤ ((𝑁 − 1) / 𝑁))) |
| 58 | 26, 56, 29, 57 | syl3anc 1373 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) ≤ (𝑁 − 1) ↔ 𝐹 ≤ ((𝑁 − 1) / 𝑁))) |
| 59 | 53, 58 | mpbid 232 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 ≤ ((𝑁 − 1) / 𝑁)) |
| 60 | 11 | simp3d 1145 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) = (𝑍 + 𝐹)) |
| 61 | 12, 59, 60 | 3jca 1129 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤
𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |