Step | Hyp | Ref
| Expression |
1 | | hashnzfzclim.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝑀 ∈
ℕ) |
3 | | hashnzfzclim.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝐽 ∈
ℤ) |
5 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝑘 ∈
(ℤ≥‘(𝐽 − 1))) |
6 | 2, 4, 5 | hashnzfz 37541 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → (#‘((
∥ “ {𝑀}) ∩
(𝐽...𝑘))) = ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) |
7 | 6 | oveq1d 6564 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) →
((#‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘) = (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) |
8 | 7 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((#‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
9 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
10 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
12 | 1 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
13 | 1 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) |
14 | 12, 13 | reccld 10673 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℂ) |
15 | 9 | eqimss2i 3623 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ |
16 | | nnex 10903 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
17 | 15, 16 | climconst2 14127 |
. . . . . . . . 9
⊢ (((1 /
𝑀) ∈ ℂ ∧ 1
∈ ℤ) → (ℕ × {(1 / 𝑀)}) ⇝ (1 / 𝑀)) |
18 | 14, 10, 17 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (ℕ × {(1 /
𝑀)}) ⇝ (1 / 𝑀)) |
19 | 16 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ ↦ ((1 /
𝑀) − (1 / 𝑘))) ∈ V |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ∈ V) |
21 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
22 | | divcnv 14424 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑘 ∈
ℕ ↦ (1 / 𝑘))
⇝ 0) |
23 | 21, 22 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) ⇝ 0) |
24 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (1 /
𝑀) ∈
V |
25 | 24 | fvconst2 6374 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → ((ℕ
× {(1 / 𝑀)})‘𝑥) = (1 / 𝑀)) |
26 | 25 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) = (1 / 𝑀)) |
27 | 14 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℂ) |
28 | 26, 27 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) ∈
ℂ) |
29 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) = (𝑘 ∈ ℕ ↦ (1 / 𝑘))) |
30 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (1 / 𝑘) = (1 / 𝑥)) |
31 | 30 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (1 / 𝑘) = (1 / 𝑥)) |
32 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ) |
33 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (1 /
𝑥) ∈
V |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈ V) |
35 | 29, 31, 32, 34 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) = (1 / 𝑥)) |
36 | 32 | nnrecred 10943 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) |
37 | 35, 36 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℝ) |
38 | 37 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℂ) |
39 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) = (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))) |
40 | 30 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) |
41 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) |
42 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((1 /
𝑀) − (1 / 𝑥)) ∈ V |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈ V) |
44 | 39, 41, 32, 43 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = ((1 / 𝑀) − (1 / 𝑥))) |
45 | 26, 35 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((ℕ ×
{(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) |
46 | 44, 45 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = (((ℕ × {(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥))) |
47 | 9, 11, 18, 20, 23, 28, 38, 46 | climsub 14212 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ ((1 / 𝑀) − 0)) |
48 | 14 | subid1d 10260 |
. . . . . . 7
⊢ (𝜑 → ((1 / 𝑀) − 0) = (1 / 𝑀)) |
49 | 47, 48 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ (1 / 𝑀)) |
50 | 16 | mptex 6390 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V) |
52 | 1 | nnrecred 10943 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
53 | 52 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℝ) |
54 | | nnre 10904 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ) |
56 | | nnne0 10930 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ≠ 0) |
58 | 55, 57 | rereccld 10731 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) |
59 | 53, 58 | resubcld 10337 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈
ℝ) |
60 | 44, 59 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ∈ ℝ) |
61 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))) |
62 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → (𝑘 / 𝑀) = (𝑥 / 𝑀)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) |
64 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → 𝑘 = 𝑥) |
65 | 63, 64 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
66 | 65 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
67 | | ovex 6577 |
. . . . . . . . 9
⊢
((⌊‘(𝑥 /
𝑀)) / 𝑥) ∈ V |
68 | 67 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ V) |
69 | 61, 66, 32, 68 | fvmptd 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
70 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℕ) |
71 | 55, 70 | nndivred 10946 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℝ) |
72 | | reflcl 12459 |
. . . . . . . . 9
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ∈
ℝ) |
73 | 71, 72 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℝ) |
74 | 73, 55, 57 | redivcld 10732 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ ℝ) |
75 | 69, 74 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℝ) |
76 | 71 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℂ) |
77 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℂ) |
78 | | nncn 10905 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℂ) |
80 | 76, 77, 79, 57 | divsubdird 10719 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥))) |
81 | 12 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℂ) |
82 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ≠ 0) |
83 | 79, 81, 82 | divrecd 10683 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) = (𝑥 · (1 / 𝑀))) |
84 | 83 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = ((𝑥 · (1 / 𝑀)) / 𝑥)) |
85 | 27, 79, 57 | divcan3d 10685 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 · (1 / 𝑀)) / 𝑥) = (1 / 𝑀)) |
86 | 84, 85 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = (1 / 𝑀)) |
87 | 86 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) |
88 | 80, 87 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = ((1 / 𝑀) − (1 / 𝑥))) |
89 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℝ) |
90 | 71, 89 | resubcld 10337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) ∈
ℝ) |
91 | | nnrp 11718 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
92 | 91 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ+) |
93 | 73, 89 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) + 1) ∈
ℝ) |
94 | | flle 12462 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) |
95 | 71, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) |
96 | | flflp1 12470 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑀) ∈ ℝ ∧ (𝑥 / 𝑀) ∈ ℝ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) |
97 | 71, 71, 96 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) |
98 | 95, 97 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1)) |
99 | 71, 93, 89, 98 | ltsub1dd 10518 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (((⌊‘(𝑥 / 𝑀)) + 1) − 1)) |
100 | 73 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℂ) |
101 | 100, 77 | pncand 10272 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) + 1) − 1) =
(⌊‘(𝑥 / 𝑀))) |
102 | 99, 101 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (⌊‘(𝑥 / 𝑀))) |
103 | 90, 73, 92, 102 | ltdiv1dd 11805 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
104 | 88, 103 | eqbrtrrd 4607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
105 | 59, 74, 104 | ltled 10064 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ≤ ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
106 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥) |
107 | 106 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (𝑘 / 𝑀) = (𝑥 / 𝑀)) |
108 | 107 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) |
109 | 108, 106 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
110 | 61, 109, 32, 68 | fvmptd 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
111 | 105, 44, 110 | 3brtr4d 4615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ≤ ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥)) |
112 | 73, 71, 92, 95 | lediv1dd 11806 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ ((𝑥 / 𝑀) / 𝑥)) |
113 | 112, 86 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ (1 / 𝑀)) |
114 | 110, 113 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ≤ (1 / 𝑀)) |
115 | 9, 11, 49, 51, 60, 75, 111, 114 | climsqz 14219 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ⇝ (1 / 𝑀)) |
116 | 16 | mptex 6390 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V |
117 | 116 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) |
118 | 3 | zred 11358 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℝ) |
119 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
120 | 118, 119 | resubcld 10337 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) |
121 | 120, 1 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → ((𝐽 − 1) / 𝑀) ∈ ℝ) |
122 | 121 | flcld 12461 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℤ) |
123 | 122 | zcnd 11359 |
. . . . . 6
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℂ) |
124 | | divcnv 14424 |
. . . . . 6
⊢
((⌊‘((𝐽
− 1) / 𝑀)) ∈
ℂ → (𝑘 ∈
ℕ ↦ ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘)) ⇝ 0) |
125 | 123, 124 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) ⇝ 0) |
126 | 75 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) |
127 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))) |
128 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
129 | 128 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
130 | | ovex 6577 |
. . . . . . . 8
⊢
((⌊‘((𝐽
− 1) / 𝑀)) / 𝑥) ∈ V |
131 | 130 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈ V) |
132 | 127, 129,
32, 131 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
133 | 123 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(⌊‘((𝐽 −
1) / 𝑀)) ∈
ℂ) |
134 | 133, 79, 57 | divcld 10680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈
ℂ) |
135 | 132, 134 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) |
136 | 100, 133,
79, 57 | divsubdird 10719 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) |
137 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
138 | 63 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) = ((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) |
139 | 138, 64 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
140 | 139 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
141 | | ovex 6577 |
. . . . . . . 8
⊢
(((⌊‘(𝑥
/ 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) ∈ V |
142 | 141 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) ∈ V) |
143 | 137, 140,
32, 142 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
144 | 69, 132 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥)) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) |
145 | 136, 143,
144 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥))) |
146 | 9, 11, 115, 117, 125, 126, 135, 145 | climsub 14212 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ ((1 / 𝑀) − 0)) |
147 | 146, 48 | breqtrd 4609 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
148 | | uzssz 11583 |
. . . . . . 7
⊢
(ℤ≥‘(𝐽 − 1)) ⊆
ℤ |
149 | | resmpt 5369 |
. . . . . . 7
⊢
((ℤ≥‘(𝐽 − 1)) ⊆ ℤ → ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
150 | 148, 149 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) |
151 | 150 | breq1i 4590 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
152 | 3, 11 | zsubcld 11363 |
. . . . . 6
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) |
153 | | zex 11263 |
. . . . . . 7
⊢ ℤ
∈ V |
154 | 153 | mptex 6390 |
. . . . . 6
⊢ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V |
155 | | climres 14154 |
. . . . . 6
⊢ (((𝐽 − 1) ∈ ℤ ∧
(𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
156 | 152, 154,
155 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
157 | 151, 156 | syl5bbr 273 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
158 | 9 | reseq2i 5314 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) |
159 | 158 | breq1i 4590 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀)) |
160 | | nnssz 11274 |
. . . . . . 7
⊢ ℕ
⊆ ℤ |
161 | | resmpt 5369 |
. . . . . . 7
⊢ (ℕ
⊆ ℤ → ((𝑘
∈ ℤ ↦ (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
162 | 160, 161 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) |
163 | 162 | breq1i 4590 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
164 | | climres 14154 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ (𝑘
∈ ℤ ↦ (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) ∈ V) → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
165 | 10, 154, 164 | mp2an 704 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
166 | 159, 163,
165 | 3bitr3i 289 |
. . . 4
⊢ ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
167 | 157, 166 | syl6bbr 277 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
168 | 147, 167 | mpbird 246 |
. 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
169 | 8, 168 | eqbrtrd 4605 |
1
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((#‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀)) |