Step | Hyp | Ref
| Expression |
1 | | hashnzfzclim.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝑀 ∈
ℕ) |
3 | | hashnzfzclim.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
4 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝐽 ∈
ℤ) |
5 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝑘 ∈
(ℤ≥‘(𝐽 − 1))) |
6 | 2, 4, 5 | hashnzfz 41517 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) →
(♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) = ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) |
7 | 6 | oveq1d 7198 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) →
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘) = (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) |
8 | 7 | mpteq2dva 5135 |
. 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
9 | | nnuz 12376 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
10 | | 1z 12106 |
. . . . . 6
⊢ 1 ∈
ℤ |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
12 | 1 | nncnd 11745 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
13 | 1 | nnne0d 11779 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) |
14 | 12, 13 | reccld 11500 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℂ) |
15 | 9 | eqimss2i 3946 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ |
16 | | nnex 11735 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
17 | 15, 16 | climconst2 15008 |
. . . . . . . . 9
⊢ (((1 /
𝑀) ∈ ℂ ∧ 1
∈ ℤ) → (ℕ × {(1 / 𝑀)}) ⇝ (1 / 𝑀)) |
18 | 14, 10, 17 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → (ℕ × {(1 /
𝑀)}) ⇝ (1 / 𝑀)) |
19 | 16 | mptex 7009 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ ↦ ((1 /
𝑀) − (1 / 𝑘))) ∈ V |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ∈ V) |
21 | | ax-1cn 10686 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
22 | | divcnv 15314 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑘 ∈
ℕ ↦ (1 / 𝑘))
⇝ 0) |
23 | 21, 22 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) ⇝ 0) |
24 | | ovex 7216 |
. . . . . . . . . . 11
⊢ (1 /
𝑀) ∈
V |
25 | 24 | fvconst2 6989 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → ((ℕ
× {(1 / 𝑀)})‘𝑥) = (1 / 𝑀)) |
26 | 25 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) = (1 / 𝑀)) |
27 | 14 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℂ) |
28 | 26, 27 | eqeltrd 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) ∈
ℂ) |
29 | | eqidd 2740 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) = (𝑘 ∈ ℕ ↦ (1 / 𝑘))) |
30 | | oveq2 7191 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (1 / 𝑘) = (1 / 𝑥)) |
31 | 30 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (1 / 𝑘) = (1 / 𝑥)) |
32 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ) |
33 | | ovexd 7218 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈ V) |
34 | 29, 31, 32, 33 | fvmptd 6795 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) = (1 / 𝑥)) |
35 | 32 | nnrecred 11780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) |
36 | 34, 35 | eqeltrd 2834 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℝ) |
37 | 36 | recnd 10760 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℂ) |
38 | | eqidd 2740 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) = (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))) |
39 | 30 | oveq2d 7199 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) |
40 | 39 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) |
41 | | ovexd 7218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈ V) |
42 | 38, 40, 32, 41 | fvmptd 6795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = ((1 / 𝑀) − (1 / 𝑥))) |
43 | 26, 34 | oveq12d 7201 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((ℕ ×
{(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) |
44 | 42, 43 | eqtr4d 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = (((ℕ × {(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥))) |
45 | 9, 11, 18, 20, 23, 28, 37, 44 | climsub 15094 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ ((1 / 𝑀) − 0)) |
46 | 14 | subid1d 11077 |
. . . . . . 7
⊢ (𝜑 → ((1 / 𝑀) − 0) = (1 / 𝑀)) |
47 | 45, 46 | breqtrd 5066 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ (1 / 𝑀)) |
48 | 16 | mptex 7009 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V |
49 | 48 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V) |
50 | 1 | nnrecred 11780 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℝ) |
52 | | nnre 11736 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
53 | 52 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ) |
54 | | nnne0 11763 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
55 | 54 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ≠ 0) |
56 | 53, 55 | rereccld 11558 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) |
57 | 51, 56 | resubcld 11159 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈
ℝ) |
58 | 42, 57 | eqeltrd 2834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ∈ ℝ) |
59 | | eqidd 2740 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))) |
60 | | fvoveq1 7206 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) |
61 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → 𝑘 = 𝑥) |
62 | 60, 61 | oveq12d 7201 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
63 | 62 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
64 | | ovexd 7218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ V) |
65 | 59, 63, 32, 64 | fvmptd 6795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
66 | 1 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℕ) |
67 | 53, 66 | nndivred 11783 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℝ) |
68 | | reflcl 13270 |
. . . . . . . . 9
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ∈
ℝ) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℝ) |
70 | 69, 53, 55 | redivcld 11559 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ ℝ) |
71 | 65, 70 | eqeltrd 2834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℝ) |
72 | 67 | recnd 10760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℂ) |
73 | | 1cnd 10727 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℂ) |
74 | | nncn 11737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
75 | 74 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℂ) |
76 | 72, 73, 75, 55 | divsubdird 11546 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥))) |
77 | 12 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℂ) |
78 | 13 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ≠ 0) |
79 | 75, 77, 78 | divrecd 11510 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) = (𝑥 · (1 / 𝑀))) |
80 | 79 | oveq1d 7198 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = ((𝑥 · (1 / 𝑀)) / 𝑥)) |
81 | 27, 75, 55 | divcan3d 11512 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 · (1 / 𝑀)) / 𝑥) = (1 / 𝑀)) |
82 | 80, 81 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = (1 / 𝑀)) |
83 | 82 | oveq1d 7198 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) |
84 | 76, 83 | eqtrd 2774 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = ((1 / 𝑀) − (1 / 𝑥))) |
85 | | 1red 10733 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℝ) |
86 | 67, 85 | resubcld 11159 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) ∈
ℝ) |
87 | | nnrp 12496 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) |
88 | 87 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ+) |
89 | 69, 85 | readdcld 10761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) + 1) ∈
ℝ) |
90 | | flle 13273 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) |
91 | 67, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) |
92 | | flflp1 13281 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑀) ∈ ℝ ∧ (𝑥 / 𝑀) ∈ ℝ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) |
93 | 67, 67, 92 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) |
94 | 91, 93 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1)) |
95 | 67, 89, 85, 94 | ltsub1dd 11343 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (((⌊‘(𝑥 / 𝑀)) + 1) − 1)) |
96 | 69 | recnd 10760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℂ) |
97 | 96, 73 | pncand 11089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) + 1) − 1) =
(⌊‘(𝑥 / 𝑀))) |
98 | 95, 97 | breqtrd 5066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (⌊‘(𝑥 / 𝑀))) |
99 | 86, 69, 88, 98 | ltdiv1dd 12584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
100 | 84, 99 | eqbrtrrd 5064 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
101 | 57, 70, 100 | ltled 10879 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ≤ ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
102 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥) |
103 | 102 | fvoveq1d 7205 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) |
104 | 103, 102 | oveq12d 7201 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
105 | 59, 104, 32, 64 | fvmptd 6795 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) |
106 | 101, 42, 105 | 3brtr4d 5072 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ≤ ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥)) |
107 | 69, 67, 88, 91 | lediv1dd 12585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ ((𝑥 / 𝑀) / 𝑥)) |
108 | 107, 82 | breqtrd 5066 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ (1 / 𝑀)) |
109 | 105, 108 | eqbrtrd 5062 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ≤ (1 / 𝑀)) |
110 | 9, 11, 47, 49, 58, 71, 106, 109 | climsqz 15101 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ⇝ (1 / 𝑀)) |
111 | 16 | mptex 7009 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V |
112 | 111 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) |
113 | 3 | zred 12181 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℝ) |
114 | | 1red 10733 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
115 | 113, 114 | resubcld 11159 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) |
116 | 115, 1 | nndivred 11783 |
. . . . . . . 8
⊢ (𝜑 → ((𝐽 − 1) / 𝑀) ∈ ℝ) |
117 | 116 | flcld 13272 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℤ) |
118 | 117 | zcnd 12182 |
. . . . . 6
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℂ) |
119 | | divcnv 15314 |
. . . . . 6
⊢
((⌊‘((𝐽
− 1) / 𝑀)) ∈
ℂ → (𝑘 ∈
ℕ ↦ ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘)) ⇝ 0) |
120 | 118, 119 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) ⇝ 0) |
121 | 71 | recnd 10760 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) |
122 | | eqidd 2740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))) |
123 | | oveq2 7191 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
124 | 123 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
125 | | ovexd 7218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈ V) |
126 | 122, 124,
32, 125 | fvmptd 6795 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) |
127 | 118 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(⌊‘((𝐽 −
1) / 𝑀)) ∈
ℂ) |
128 | 127, 75, 55 | divcld 11507 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈
ℂ) |
129 | 126, 128 | eqeltrd 2834 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) |
130 | 96, 127, 75, 55 | divsubdird 11546 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) |
131 | | eqidd 2740 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
132 | 60 | oveq1d 7198 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) = ((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) |
133 | 132, 61 | oveq12d 7201 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
134 | 133 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
135 | | ovexd 7218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) ∈ V) |
136 | 131, 134,
32, 135 | fvmptd 6795 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) |
137 | 65, 126 | oveq12d 7201 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥)) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) |
138 | 130, 136,
137 | 3eqtr4d 2784 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥))) |
139 | 9, 11, 110, 112, 120, 121, 129, 138 | climsub 15094 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ ((1 / 𝑀) − 0)) |
140 | 139, 46 | breqtrd 5066 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
141 | | uzssz 12358 |
. . . . . . 7
⊢
(ℤ≥‘(𝐽 − 1)) ⊆
ℤ |
142 | | resmpt 5889 |
. . . . . . 7
⊢
((ℤ≥‘(𝐽 − 1)) ⊆ ℤ → ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
143 | 141, 142 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) |
144 | 143 | breq1i 5047 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
145 | 3, 11 | zsubcld 12186 |
. . . . . 6
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) |
146 | | zex 12084 |
. . . . . . 7
⊢ ℤ
∈ V |
147 | 146 | mptex 7009 |
. . . . . 6
⊢ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V |
148 | | climres 15035 |
. . . . . 6
⊢ (((𝐽 − 1) ∈ ℤ ∧
(𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
149 | 145, 147,
148 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
150 | 144, 149 | bitr3id 288 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
151 | 9 | reseq2i 5832 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) |
152 | 151 | breq1i 5047 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀)) |
153 | | nnssz 12096 |
. . . . . . 7
⊢ ℕ
⊆ ℤ |
154 | | resmpt 5889 |
. . . . . . 7
⊢ (ℕ
⊆ ℤ → ((𝑘
∈ ℤ ↦ (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) |
155 | 153, 154 | ax-mp 5 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) |
156 | 155 | breq1i 5047 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
157 | | climres 15035 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ (𝑘
∈ ℤ ↦ (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) ∈ V) → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
158 | 10, 147, 157 | mp2an 692 |
. . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
159 | 152, 156,
158 | 3bitr3i 304 |
. . . 4
⊢ ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
160 | 150, 159 | bitr4di 292 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) |
161 | 140, 160 | mpbird 260 |
. 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) |
162 | 8, 161 | eqbrtrd 5062 |
1
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀)) |