Proof of Theorem fldiv
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . . 9
⊢
(⌊‘𝐴) =
(⌊‘𝐴) |
2 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝐴 − (⌊‘𝐴)) = (𝐴 − (⌊‘𝐴)) |
3 | 1, 2 | intfrac2 12519 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 ≤
(𝐴 −
(⌊‘𝐴)) ∧
(𝐴 −
(⌊‘𝐴)) < 1
∧ 𝐴 =
((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))))) |
4 | 3 | simp3d 1068 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
6 | 5 | oveq1d 6564 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))) / 𝑁)) |
7 | | reflcl 12459 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
8 | 7 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℂ) |
10 | | resubcl 10224 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (𝐴 −
(⌊‘𝐴)) ∈
ℝ) |
11 | 7, 10 | mpdan 699 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
12 | 11 | recnd 9947 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ∈
ℂ) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℂ) |
14 | | nncn 10905 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
15 | | nnne0 10930 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
16 | 14, 15 | jca 553 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
18 | | divdir 10589 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℂ ∧ (𝐴
− (⌊‘𝐴))
∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → (((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))) / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
19 | 9, 13, 17, 18 | syl3anc 1318 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) +
(𝐴 −
(⌊‘𝐴))) / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
20 | 6, 19 | eqtrd 2644 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
21 | | flcl 12458 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘((⌊‘𝐴) / 𝑁)) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
/ 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) = (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) |
24 | 22, 23 | intfracq 12520 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∧ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))))) |
25 | 24 | simp3d 1068 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
26 | 21, 25 | sylan 487 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) =
((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
27 | 26 | oveq1d 6564 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = (((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
28 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℝ) |
29 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
30 | 29 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
31 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
32 | 28, 30, 31 | redivcld 10732 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) ∈
ℝ) |
33 | | reflcl 12459 |
. . . . . . 7
⊢
(((⌊‘𝐴)
/ 𝑁) ∈ ℝ →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℝ) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℝ) |
35 | 34 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℂ) |
36 | 32, 34 | resubcld 10337 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ) |
37 | 36 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℂ) |
38 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
39 | 38, 30, 31 | redivcld 10732 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) |
40 | 39 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℂ) |
41 | 35, 37, 40 | addassd 9941 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
42 | 20, 27, 41 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
43 | 42 | fveq2d 6107 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝐴 / 𝑁)) =
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))))) |
44 | 24 | simp1d 1066 |
. . . . 5
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → 0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
45 | 21, 44 | sylan 487 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
46 | | fracge0 12467 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 0 ≤
(𝐴 −
(⌊‘𝐴))) |
47 | 11, 46 | jca 553 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 0 ≤
(𝐴 −
(⌊‘𝐴)))) |
48 | | nngt0 10926 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
49 | 29, 48 | jca 553 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
50 | | divge0 10771 |
. . . . 5
⊢ ((((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 0 ≤
(𝐴 −
(⌊‘𝐴))) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((𝐴 −
(⌊‘𝐴)) / 𝑁)) |
51 | 47, 49, 50 | syl2an 493 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
((𝐴 −
(⌊‘𝐴)) / 𝑁)) |
52 | 36, 39, 45, 51 | addge0d 10482 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
53 | | peano2rem 10227 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
54 | 29, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
55 | 54, 29, 15 | redivcld 10732 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
56 | | nnrecre 10934 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 /
𝑁) ∈
ℝ) |
57 | 55, 56 | jca 553 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ)) |
58 | 57 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ)) |
59 | 36, 39, 58 | jca31 555 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) ∧ (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ))) |
60 | 24 | simp2d 1067 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
61 | 21, 60 | sylan 487 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
62 | | fraclt1 12465 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) < 1) |
63 | 62 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) < 1) |
64 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
65 | | ltdiv1 10766 |
. . . . . . . . 9
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ ((𝐴 −
(⌊‘𝐴)) < 1
↔ ((𝐴 −
(⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
66 | 64, 65 | mp3an2 1404 |
. . . . . . . 8
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
67 | 11, 49, 66 | syl2an 493 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
68 | 63, 67 | mpbid 221 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁)) |
69 | 61, 68 | jca 553 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
70 | | leltadd 10391 |
. . . . 5
⊢
((((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) ∧ (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈ ℝ)) →
(((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁)) → ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < (((𝑁 − 1) / 𝑁) + (1 / 𝑁)))) |
71 | 59, 69, 70 | sylc 63 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
72 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
73 | | npcan 10169 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
74 | 14, 72, 73 | sylancl 693 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
75 | 74 | oveq1d 6564 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (𝑁 / 𝑁)) |
76 | 54 | recnd 9947 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
77 | | divdir 10589 |
. . . . . . . 8
⊢ (((𝑁 − 1) ∈ ℂ ∧
1 ∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → (((𝑁 − 1)
+ 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
78 | 72, 77 | mp3an2 1404 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 ∈ ℂ ∧
𝑁 ≠ 0)) → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
79 | 76, 14, 15, 78 | syl12anc 1316 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
80 | 14, 15 | dividd 10678 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 / 𝑁) = 1) |
81 | 75, 79, 80 | 3eqtr3d 2652 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
82 | 81 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
83 | 71, 82 | breqtrd 4609 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1) |
84 | 32 | flcld 12461 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ) |
85 | 36, 39 | readdcld 9948 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℝ) |
86 | | flbi2 12480 |
. . . 4
⊢
(((⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ ∧
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℝ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
87 | 84, 85, 86 | syl2anc 691 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
88 | 52, 83, 87 | mpbir2and 959 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁))) |
89 | 43, 88 | eqtr2d 2645 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) |