Proof of Theorem flqdiv
Step | Hyp | Ref
| Expression |
1 | | eqid 2170 |
. . . . . . . . 9
⊢
(⌊‘𝐴) =
(⌊‘𝐴) |
2 | | eqid 2170 |
. . . . . . . . 9
⊢ (𝐴 − (⌊‘𝐴)) = (𝐴 − (⌊‘𝐴)) |
3 | 1, 2 | intqfrac2 10275 |
. . . . . . . 8
⊢ (𝐴 ∈ ℚ → (0 ≤
(𝐴 −
(⌊‘𝐴)) ∧
(𝐴 −
(⌊‘𝐴)) < 1
∧ 𝐴 =
((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))))) |
4 | 3 | simp3d 1006 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
5 | 4 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝐴 = ((⌊‘𝐴) + (𝐴 − (⌊‘𝐴)))) |
6 | 5 | oveq1d 5868 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) + (𝐴 − (⌊‘𝐴))) / 𝑁)) |
7 | | simpl 108 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝐴 ∈
ℚ) |
8 | 7 | flqcld 10233 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℤ) |
9 | 8 | zcnd 9335 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℂ) |
10 | | zq 9585 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℤ → (⌊‘𝐴) ∈ ℚ) |
11 | 8, 10 | syl 14 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘𝐴) ∈
ℚ) |
12 | | qsubcl 9597 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧
(⌊‘𝐴) ∈
ℚ) → (𝐴 −
(⌊‘𝐴)) ∈
ℚ) |
13 | | qcn 9593 |
. . . . . . . 8
⊢ ((𝐴 − (⌊‘𝐴)) ∈ ℚ → (𝐴 − (⌊‘𝐴)) ∈
ℂ) |
14 | 12, 13 | syl 14 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧
(⌊‘𝐴) ∈
ℚ) → (𝐴 −
(⌊‘𝐴)) ∈
ℂ) |
15 | 11, 14 | syldan 280 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℂ) |
16 | | simpr 109 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
17 | 16 | nncnd 8892 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
18 | 16 | nnap0d 8924 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 # 0) |
19 | 9, 15, 17, 18 | divdirapd 8746 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) +
(𝐴 −
(⌊‘𝐴))) / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
20 | 6, 19 | eqtrd 2203 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = (((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
21 | | flqcl 10229 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
(⌊‘𝐴) ∈
ℤ) |
22 | | eqid 2170 |
. . . . . . . 8
⊢
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘((⌊‘𝐴) / 𝑁)) |
23 | | eqid 2170 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
/ 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) = (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) |
24 | 22, 23 | intfracq 10276 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∧ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁) ∧ ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))))) |
25 | 24 | simp3d 1006 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → ((⌊‘𝐴) / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
26 | 21, 25 | sylan 281 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) =
((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))))) |
27 | 26 | oveq1d 5868 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = (((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
28 | | znq 9583 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → ((⌊‘𝐴) / 𝑁) ∈ ℚ) |
29 | 28 | flqcld 10233 |
. . . . . . 7
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ) |
30 | 21, 29 | sylan 281 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ) |
31 | 30 | zcnd 9335 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℂ) |
32 | 8, 16, 28 | syl2anc 409 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((⌊‘𝐴) / 𝑁) ∈
ℚ) |
33 | | zq 9585 |
. . . . . . . 8
⊢
((⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℚ) |
34 | 30, 33 | syl 14 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℚ) |
35 | | qsubcl 9597 |
. . . . . . 7
⊢
((((⌊‘𝐴)
/ 𝑁) ∈ ℚ ∧
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℚ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℚ) |
36 | 32, 34, 35 | syl2anc 409 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℚ) |
37 | | qcn 9593 |
. . . . . 6
⊢
((((⌊‘𝐴)
/ 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℚ →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℂ) |
38 | 36, 37 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℂ) |
39 | 11, 12 | syldan 280 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℚ) |
40 | | nnq 9592 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
41 | 40 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℚ) |
42 | 16 | nnne0d 8923 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) |
43 | | qdivcl 9602 |
. . . . . . 7
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℚ) |
44 | 39, 41, 42, 43 | syl3anc 1233 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℚ) |
45 | | qcn 9593 |
. . . . . 6
⊢ (((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℚ → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℂ) |
46 | 44, 45 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℂ) |
47 | 31, 38, 46 | addassd 7942 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘((⌊‘𝐴) / 𝑁)) + (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
48 | 20, 27, 47 | 3eqtrd 2207 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) = ((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) |
49 | 48 | fveq2d 5500 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘(𝐴 / 𝑁)) =
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))))) |
50 | | qre 9584 |
. . . . 5
⊢
((((⌊‘𝐴)
/ 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℚ →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ) |
51 | 36, 50 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℝ) |
52 | | qre 9584 |
. . . . . 6
⊢ ((𝐴 − (⌊‘𝐴)) ∈ ℚ → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
53 | 39, 52 | syl 14 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) ∈
ℝ) |
54 | 53, 16 | nndivred 8928 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℝ) |
55 | 24 | simp1d 1004 |
. . . . 5
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → 0 ≤ (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
56 | 21, 55 | sylan 281 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 0 ≤
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁)))) |
57 | 16 | nnrpd 9651 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ+) |
58 | | qfracge0 10237 |
. . . . . 6
⊢ (𝐴 ∈ ℚ → 0 ≤
(𝐴 −
(⌊‘𝐴))) |
59 | 58 | adantr 274 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 0 ≤
(𝐴 −
(⌊‘𝐴))) |
60 | 53, 57, 59 | divge0d 9694 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 0 ≤
((𝐴 −
(⌊‘𝐴)) / 𝑁)) |
61 | 51, 54, 56, 60 | addge0d 8441 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 0 ≤
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁))) |
62 | | nnre 8885 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
63 | | peano2rem 8186 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
64 | 62, 63 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
65 | | nnap0 8907 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 # 0) |
66 | 64, 62, 65 | redivclapd 8752 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
67 | 66 | adantl 275 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 1) / 𝑁) ∈ ℝ) |
68 | 16 | nnrecred 8925 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (1 /
𝑁) ∈
ℝ) |
69 | 24 | simp2d 1005 |
. . . . . 6
⊢
(((⌊‘𝐴)
∈ ℤ ∧ 𝑁
∈ ℕ) → (((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
70 | 21, 69 | sylan 281 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ≤ ((𝑁 − 1) / 𝑁)) |
71 | | qfraclt1 10236 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → (𝐴 − (⌊‘𝐴)) < 1) |
72 | 71 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (𝐴 − (⌊‘𝐴)) < 1) |
73 | 16 | nnred 8891 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) |
74 | 16 | nngt0d 8922 |
. . . . . . 7
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → 0 <
𝑁) |
75 | | 1re 7919 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
76 | | ltdiv1 8784 |
. . . . . . . 8
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ ((𝐴 −
(⌊‘𝐴)) < 1
↔ ((𝐴 −
(⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
77 | 75, 76 | mp3an2 1320 |
. . . . . . 7
⊢ (((𝐴 − (⌊‘𝐴)) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
78 | 53, 73, 74, 77 | syl12anc 1231 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) < 1 ↔ ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁))) |
79 | 72, 78 | mpbid 146 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → ((𝐴 − (⌊‘𝐴)) / 𝑁) < (1 / 𝑁)) |
80 | 51, 54, 67, 68, 70, 79 | leltaddd 8485 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
81 | | nncn 8886 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
82 | | npcan1 8297 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
83 | 81, 82 | syl 14 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
84 | 83 | oveq1d 5868 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (𝑁 / 𝑁)) |
85 | 64 | recnd 7948 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
86 | | ax-1cn 7867 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
87 | | divdirap 8614 |
. . . . . . . 8
⊢ (((𝑁 − 1) ∈ ℂ ∧
1 ∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 #
0)) → (((𝑁 − 1)
+ 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
88 | 86, 87 | mp3an2 1320 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈ ℂ ∧
(𝑁 ∈ ℂ ∧
𝑁 # 0)) → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
89 | 85, 81, 65, 88 | syl12anc 1231 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) + 1) / 𝑁) = (((𝑁 − 1) / 𝑁) + (1 / 𝑁))) |
90 | 81, 65 | dividapd 8703 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 / 𝑁) = 1) |
91 | 84, 89, 90 | 3eqtr3d 2211 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
92 | 91 | adantl 275 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1) / 𝑁) + (1 / 𝑁)) = 1) |
93 | 80, 92 | breqtrd 4015 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1) |
94 | 32 | flqcld 10233 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ) |
95 | | qaddcl 9594 |
. . . . 5
⊢
(((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) ∈ ℚ ∧ ((𝐴 − (⌊‘𝐴)) / 𝑁) ∈ ℚ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℚ) |
96 | 36, 44, 95 | syl2anc 409 |
. . . 4
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℚ) |
97 | | flqbi2 10247 |
. . . 4
⊢
(((⌊‘((⌊‘𝐴) / 𝑁)) ∈ ℤ ∧
((((⌊‘𝐴) /
𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∈ ℚ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
98 | 94, 96, 97 | syl2anc 409 |
. . 3
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
((⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁)) ↔ (0 ≤ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) ∧ ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)) < 1))) |
99 | 61, 93, 98 | mpbir2and 939 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘((⌊‘𝐴) / 𝑁)) + ((((⌊‘𝐴) / 𝑁) −
(⌊‘((⌊‘𝐴) / 𝑁))) + ((𝐴 − (⌊‘𝐴)) / 𝑁)))) = (⌊‘((⌊‘𝐴) / 𝑁))) |
100 | 49, 99 | eqtr2d 2204 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ) →
(⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) |