Proof of Theorem fldiv
Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . . 9
⊢
(⌊‘𝐴) =
(⌊‘𝐴) |
2 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐴 − (⌊‘𝐴)) = (𝐴 − (⌊‘𝐴)) |
3 | 1, 2 | intfrac2 13431 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 ≤
(𝐴 −
(⌊‘𝐴)) ∧
(𝐴 −
(⌊‘𝐴)) < 1
∧ 𝐴 =
((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))))) |
4 | 3 | simp3d 1146 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
6 | 5 | oveq1d 7228 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))) / 𝑁)) |
7 | | reflcl 13371 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
8 | 7 | recnd 10861 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℂ) |
9 | | resubcl 11142 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
ℝ) → (𝐴 −
(⌊‘𝐴)) ∈
ℝ) |
10 | 7, 9 | mpdan 687 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
11 | 10 | recnd 10861 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ∈
ℂ) |
12 | | nncn 11838 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
13 | | nnne0 11864 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
14 | 12, 13 | jca 515 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
15 | | divdir 11515 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℂ ∧ (𝐴
− (⌊‘𝐴))
∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → (((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))) / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
16 | 8, 11, 14, 15 | syl2an3an 1424 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) +
(𝐴 −
(⌊‘𝐴))) / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
17 | 6, 16 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
18 | | flcl 13370 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
19 | | eqid 2737 |
. . . . . . . 8
⊢
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘((⌊‘𝐴) / 𝑁)) |
20 | | eqid 2737 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
/ 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) = (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) |
21 | 19, 20 | intfracq 13432 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∧ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))))) |
22 | 21 | simp3d 1146 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
23 | 18, 22 | sylan 583 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) =
((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
24 | 23 | oveq1d 7228 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = (((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
25 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℝ) |
26 | | nnre 11837 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
27 | 26 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
28 | 13 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
29 | 25, 27, 28 | redivcld 11660 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) ∈
ℝ) |
30 | | reflcl 13371 |
. . . . . . 7
⊢
(((⌊‘𝐴)
/ 𝑁) ∈ ℝ →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℝ) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℝ) |
32 | 31 | recnd 10861 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℂ) |
33 | 29, 31 | resubcld 11260 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ) |
34 | 33 | recnd 10861 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℂ) |
35 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
36 | 35, 27, 28 | redivcld 11660 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) |
37 | 36 | recnd 10861 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℂ) |
38 | 32, 34, 37 | addassd 10855 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
39 | 17, 24, 38 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
40 | 39 | fveq2d 6721 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝐴 / 𝑁)) =
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))))) |
41 | 21 | simp1d 1144 |
. . . . 5
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → 0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
42 | 18, 41 | sylan 583 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
43 | | fracge0 13379 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 0 ≤
(𝐴 −
(⌊‘𝐴))) |
44 | 10, 43 | jca 515 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 0 ≤
(𝐴 −
(⌊‘𝐴)))) |
45 | | nngt0 11861 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
46 | 26, 45 | jca 515 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 0 <
𝑁)) |
47 | | divge0 11701 |
. . . . 5
⊢ ((((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 0 ≤
(𝐴 −
(⌊‘𝐴))) ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → 0 ≤
((𝐴 −
(⌊‘𝐴)) / 𝑁)) |
48 | 44, 46, 47 | syl2an 599 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
((𝐴 −
(⌊‘𝐴)) / 𝑁)) |
49 | 33, 36, 42, 48 | addge0d 11408 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → 0 ≤
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
50 | | peano2rem 11145 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
51 | 26, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
52 | 51, 26, 13 | redivcld 11660 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
53 | | nnrecre 11872 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1 /
𝑁) ∈
ℝ) |
54 | 52, 53 | jca 515 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ)) |
55 | 54 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ)) |
56 | 33, 36, 55 | jca31 518 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) ∧ (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈
ℝ))) |
57 | 21 | simp2d 1145 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
58 | 18, 57 | sylan 583 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
59 | | fraclt1 13377 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) < 1) |
60 | 59 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) < 1) |
61 | | 1re 10833 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
62 | | ltdiv1 11696 |
. . . . . . . . 9
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ ((𝐴 −
(⌊‘𝐴)) < 1
↔ ((𝐴 −
(⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
63 | 61, 62 | mp3an2 1451 |
. . . . . . . 8
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
64 | 10, 46, 63 | syl2an 599 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
65 | 60, 64 | mpbid 235 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁)) |
66 | 58, 65 | jca 515 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
67 | | leltadd 11316 |
. . . . 5
⊢
((((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) ∧ (((𝑁 − 1) / 𝑁) ∈ ℝ ∧ (1 / 𝑁) ∈ ℝ)) →
(((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁)) → ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < (((𝑁 − 1) / 𝑁) + (1 / 𝑁)))) |
68 | 56, 66, 67 | sylc 65 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
69 | | ax-1cn 10787 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
70 | | npcan 11087 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
71 | 12, 69, 70 | sylancl 589 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
72 | 71 | oveq1d 7228 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (𝑁 / 𝑁)) |
73 | 51 | recnd 10861 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
74 | | divdir 11515 |
. . . . . . . 8
⊢ (((𝑁 − 1) ∈ ℂ ∧
1 ∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → (((𝑁 − 1)
+ 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
75 | 69, 74 | mp3an2 1451 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 ∈ ℂ ∧
𝑁 ≠ 0)) → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
76 | 73, 12, 13, 75 | syl12anc 837 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
77 | 12, 13 | dividd 11606 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 / 𝑁) = 1) |
78 | 72, 76, 77 | 3eqtr3d 2785 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
79 | 78 | adantl 485 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
80 | 68, 79 | breqtrd 5079 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1) |
81 | 29 | flcld 13373 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ) |
82 | 33, 36 | readdcld 10862 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℝ) |
83 | | flbi2 13392 |
. . . 4
⊢
(((⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ ∧
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℝ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
84 | 81, 82, 83 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
85 | 49, 80, 84 | mpbir2and 713 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁))) |
86 | 40, 85 | eqtr2d 2778 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) |