Proof of Theorem intfracq
Step | Hyp | Ref
| Expression |
1 | | zre 11381 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℝ) |
3 | | nnre 11027 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
4 | 3 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
5 | | nnne0 11053 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
6 | 5 | adantl 482 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
7 | 2, 4, 6 | redivcld 10853 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℝ) |
8 | | intfracq.1 |
. . . . 5
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁)) |
9 | | intfracq.2 |
. . . . 5
⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍) |
10 | 8, 9 | intfrac2 12657 |
. . . 4
⊢ ((𝑀 / 𝑁) ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |
11 | 7, 10 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤
𝐹 ∧ 𝐹 < 1 ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |
12 | 11 | simp1d 1073 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝐹) |
13 | | fraclt1 12603 |
. . . . . . 7
⊢ ((𝑀 / 𝑁) ∈ ℝ → ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) < 1) |
14 | 7, 13 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) < 1) |
15 | 8 | oveq2i 6661 |
. . . . . . . 8
⊢ ((𝑀 / 𝑁) − 𝑍) = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) |
16 | 9, 15 | eqtri 2644 |
. . . . . . 7
⊢ 𝐹 = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁))) |
17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑀 / 𝑁) − (⌊‘(𝑀 / 𝑁)))) |
18 | | nncn 11028 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
19 | 18, 5 | dividd 10799 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 / 𝑁) = 1) |
20 | 19 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 / 𝑁) = 1) |
21 | 14, 17, 20 | 3brtr4d 4685 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 < (𝑁 / 𝑁)) |
22 | | reflcl 12597 |
. . . . . . . . . 10
⊢ ((𝑀 / 𝑁) ∈ ℝ →
(⌊‘(𝑀 / 𝑁)) ∈
ℝ) |
23 | 7, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℝ) |
24 | 8, 23 | syl5eqel 2705 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℝ) |
25 | 7, 24 | resubcld 10458 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 / 𝑁) − 𝑍) ∈ ℝ) |
26 | 9, 25 | syl5eqel 2705 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 ∈
ℝ) |
27 | | nngt0 11049 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
28 | 3, 27 | jca 554 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
29 | 28 | adantl 482 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
30 | | ltmuldiv2 10897 |
. . . . . 6
⊢ ((𝐹 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝑁 · 𝐹) < 𝑁 ↔ 𝐹 < (𝑁 / 𝑁))) |
31 | 26, 4, 29, 30 | syl3anc 1326 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) < 𝑁 ↔ 𝐹 < (𝑁 / 𝑁))) |
32 | 21, 31 | mpbird 247 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) < 𝑁) |
33 | 9 | oveq2i 6661 |
. . . . . . 7
⊢ (𝑁 · 𝐹) = (𝑁 · ((𝑀 / 𝑁) − 𝑍)) |
34 | 18 | adantl 482 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
35 | 7 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) ∈ ℂ) |
36 | 7 | flcld 12599 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝑀 / 𝑁)) ∈
ℤ) |
37 | 8, 36 | syl5eqel 2705 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℤ) |
38 | 37 | zcnd 11483 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑍 ∈
ℂ) |
39 | 34, 35, 38 | subdid 10486 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · ((𝑀 / 𝑁) − 𝑍)) = ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍))) |
40 | 33, 39 | syl5eq 2668 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) = ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍))) |
41 | | zcn 11382 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
42 | 41 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℂ) |
43 | 42, 34, 6 | divcan2d 10803 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) = 𝑀) |
44 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℤ) |
45 | 43, 44 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · (𝑀 / 𝑁)) ∈ ℤ) |
46 | | nnz 11399 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
47 | 46 | adantl 482 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
48 | 47, 37 | zmulcld 11488 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝑍) ∈ ℤ) |
49 | 45, 48 | zsubcld 11487 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · (𝑀 / 𝑁)) − (𝑁 · 𝑍)) ∈ ℤ) |
50 | 40, 49 | eqeltrd 2701 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) ∈ ℤ) |
51 | | zltlem1 11430 |
. . . . 5
⊢ (((𝑁 · 𝐹) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 · 𝐹) < 𝑁 ↔ (𝑁 · 𝐹) ≤ (𝑁 − 1))) |
52 | 50, 47, 51 | syl2anc 693 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) < 𝑁 ↔ (𝑁 · 𝐹) ≤ (𝑁 − 1))) |
53 | 32, 52 | mpbid 222 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 · 𝐹) ≤ (𝑁 − 1)) |
54 | | peano2rem 10348 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
55 | 3, 54 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
56 | 55 | adantl 482 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈
ℝ) |
57 | | lemuldiv2 10904 |
. . . 4
⊢ ((𝐹 ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝑁 · 𝐹) ≤ (𝑁 − 1) ↔ 𝐹 ≤ ((𝑁 − 1) / 𝑁))) |
58 | 26, 56, 29, 57 | syl3anc 1326 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 · 𝐹) ≤ (𝑁 − 1) ↔ 𝐹 ≤ ((𝑁 − 1) / 𝑁))) |
59 | 53, 58 | mpbid 222 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝐹 ≤ ((𝑁 − 1) / 𝑁)) |
60 | 11 | simp3d 1075 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 / 𝑁) = (𝑍 + 𝐹)) |
61 | 12, 59, 60 | 3jca 1242 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤
𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |