| 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 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) → 𝑘 ∈
(ℤ≥‘(𝐽 − 1))) | 
| 6 | 2, 4, 5 | hashnzfz 44344 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) →
(♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) = ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) | 
| 7 | 6 | oveq1d 7447 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐽 − 1))) →
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘) = (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) | 
| 8 | 7 | mpteq2dva 5241 | . 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) | 
| 9 |  | nnuz 12922 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 10 |  | 1z 12649 | . . . . . 6
⊢ 1 ∈
ℤ | 
| 11 | 10 | a1i 11 | . . . . 5
⊢ (𝜑 → 1 ∈
ℤ) | 
| 12 | 1 | nncnd 12283 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 13 | 1 | nnne0d 12317 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) | 
| 14 | 12, 13 | reccld 12037 | . . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℂ) | 
| 15 | 9 | eqimss2i 4044 | . . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℕ | 
| 16 |  | nnex 12273 | . . . . . . . . . 10
⊢ ℕ
∈ V | 
| 17 | 15, 16 | climconst2 15585 | . . . . . . . . 9
⊢ (((1 /
𝑀) ∈ ℂ ∧ 1
∈ ℤ) → (ℕ × {(1 / 𝑀)}) ⇝ (1 / 𝑀)) | 
| 18 | 14, 10, 17 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (ℕ × {(1 /
𝑀)}) ⇝ (1 / 𝑀)) | 
| 19 | 16 | mptex 7244 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ ↦ ((1 /
𝑀) − (1 / 𝑘))) ∈ V | 
| 20 | 19 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ∈ V) | 
| 21 |  | ax-1cn 11214 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 22 |  | divcnv 15890 | . . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑘 ∈
ℕ ↦ (1 / 𝑘))
⇝ 0) | 
| 23 | 21, 22 | mp1i 13 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) ⇝ 0) | 
| 24 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (1 /
𝑀) ∈
V | 
| 25 | 24 | fvconst2 7225 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → ((ℕ
× {(1 / 𝑀)})‘𝑥) = (1 / 𝑀)) | 
| 26 | 25 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) = (1 / 𝑀)) | 
| 27 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℂ) | 
| 28 | 26, 27 | eqeltrd 2840 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((ℕ × {(1
/ 𝑀)})‘𝑥) ∈
ℂ) | 
| 29 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ (1 / 𝑘)) = (𝑘 ∈ ℕ ↦ (1 / 𝑘))) | 
| 30 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑥 → (1 / 𝑘) = (1 / 𝑥)) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (1 / 𝑘) = (1 / 𝑥)) | 
| 32 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ) | 
| 33 |  | ovexd 7467 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈ V) | 
| 34 | 29, 31, 32, 33 | fvmptd 7022 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) = (1 / 𝑥)) | 
| 35 | 32 | nnrecred 12318 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) | 
| 36 | 34, 35 | eqeltrd 2840 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℝ) | 
| 37 | 36 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥) ∈ ℂ) | 
| 38 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) = (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))) | 
| 39 | 30 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑥 → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 40 | 39 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((1 / 𝑀) − (1 / 𝑘)) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 41 |  | ovexd 7467 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈ V) | 
| 42 | 38, 40, 32, 41 | fvmptd 7022 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 43 | 26, 34 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((ℕ ×
{(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 44 | 42, 43 | eqtr4d 2779 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) = (((ℕ × {(1 / 𝑀)})‘𝑥) − ((𝑘 ∈ ℕ ↦ (1 / 𝑘))‘𝑥))) | 
| 45 | 9, 11, 18, 20, 23, 28, 37, 44 | climsub 15671 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ ((1 / 𝑀) − 0)) | 
| 46 | 14 | subid1d 11610 | . . . . . . 7
⊢ (𝜑 → ((1 / 𝑀) − 0) = (1 / 𝑀)) | 
| 47 | 45, 46 | breqtrd 5168 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘))) ⇝ (1 / 𝑀)) | 
| 48 | 16 | mptex 7244 | . . . . . . 7
⊢ (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V | 
| 49 | 48 | a1i 11 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ∈ V) | 
| 50 | 1 | nnrecred 12318 | . . . . . . . . 9
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑀) ∈
ℝ) | 
| 52 |  | nnre 12274 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) | 
| 53 | 52 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ) | 
| 54 |  | nnne0 12301 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) | 
| 55 | 54 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ≠ 0) | 
| 56 | 53, 55 | rereccld 12095 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (1 / 𝑥) ∈
ℝ) | 
| 57 | 51, 56 | resubcld 11692 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ∈
ℝ) | 
| 58 | 42, 57 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ∈ ℝ) | 
| 59 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))) | 
| 60 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) | 
| 61 |  | id 22 | . . . . . . . . . 10
⊢ (𝑘 = 𝑥 → 𝑘 = 𝑥) | 
| 62 | 60, 61 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 63 | 62 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 64 |  | ovexd 7467 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ V) | 
| 65 | 59, 63, 32, 64 | fvmptd 7022 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 66 | 1 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℕ) | 
| 67 | 53, 66 | nndivred 12321 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℝ) | 
| 68 |  | reflcl 13837 | . . . . . . . . 9
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ∈
ℝ) | 
| 69 | 67, 68 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℝ) | 
| 70 | 69, 53, 55 | redivcld 12096 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ∈ ℝ) | 
| 71 | 65, 70 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℝ) | 
| 72 | 67 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) ∈ ℂ) | 
| 73 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℂ) | 
| 74 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℂ) | 
| 76 | 72, 73, 75, 55 | divsubdird 12083 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥))) | 
| 77 | 12 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ∈ ℂ) | 
| 78 | 13 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑀 ≠ 0) | 
| 79 | 75, 77, 78 | divrecd 12047 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) = (𝑥 · (1 / 𝑀))) | 
| 80 | 79 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = ((𝑥 · (1 / 𝑀)) / 𝑥)) | 
| 81 | 27, 75, 55 | divcan3d 12049 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 · (1 / 𝑀)) / 𝑥) = (1 / 𝑀)) | 
| 82 | 80, 81 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) / 𝑥) = (1 / 𝑀)) | 
| 83 | 82 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) / 𝑥) − (1 / 𝑥)) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 84 | 76, 83 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) = ((1 / 𝑀) − (1 / 𝑥))) | 
| 85 |  | 1red 11263 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 1 ∈
ℝ) | 
| 86 | 67, 85 | resubcld 11692 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) ∈
ℝ) | 
| 87 |  | nnrp 13047 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ+) | 
| 88 | 87 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℝ+) | 
| 89 | 69, 85 | readdcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) + 1) ∈
ℝ) | 
| 90 |  | flle 13840 | . . . . . . . . . . . . . 14
⊢ ((𝑥 / 𝑀) ∈ ℝ →
(⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) | 
| 91 | 67, 90 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀)) | 
| 92 |  | flflp1 13848 | . . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑀) ∈ ℝ ∧ (𝑥 / 𝑀) ∈ ℝ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) | 
| 93 | 67, 67, 92 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) ≤ (𝑥 / 𝑀) ↔ (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1))) | 
| 94 | 91, 93 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑥 / 𝑀) < ((⌊‘(𝑥 / 𝑀)) + 1)) | 
| 95 | 67, 89, 85, 94 | ltsub1dd 11876 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (((⌊‘(𝑥 / 𝑀)) + 1) − 1)) | 
| 96 | 69 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (⌊‘(𝑥 / 𝑀)) ∈ ℂ) | 
| 97 | 96, 73 | pncand 11622 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) + 1) − 1) =
(⌊‘(𝑥 / 𝑀))) | 
| 98 | 95, 97 | breqtrd 5168 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑥 / 𝑀) − 1) < (⌊‘(𝑥 / 𝑀))) | 
| 99 | 86, 69, 88, 98 | ltdiv1dd 13135 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑥 / 𝑀) − 1) / 𝑥) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 100 | 84, 99 | eqbrtrrd 5166 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) < ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 101 | 57, 70, 100 | ltled 11410 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((1 / 𝑀) − (1 / 𝑥)) ≤ ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 102 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥) | 
| 103 | 102 | fvoveq1d 7454 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (⌊‘(𝑘 / 𝑀)) = (⌊‘(𝑥 / 𝑀))) | 
| 104 | 103, 102 | oveq12d 7450 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘(𝑘 / 𝑀)) / 𝑘) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 105 | 59, 104, 32, 64 | fvmptd 7022 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘(𝑥 / 𝑀)) / 𝑥)) | 
| 106 | 101, 42, 105 | 3brtr4d 5174 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦ ((1 / 𝑀) − (1 / 𝑘)))‘𝑥) ≤ ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥)) | 
| 107 | 69, 67, 88, 91 | lediv1dd 13136 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ ((𝑥 / 𝑀) / 𝑥)) | 
| 108 | 107, 82 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘(𝑥 / 𝑀)) / 𝑥) ≤ (1 / 𝑀)) | 
| 109 | 105, 108 | eqbrtrd 5164 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ≤ (1 / 𝑀)) | 
| 110 | 9, 11, 47, 49, 58, 71, 106, 109 | climsqz 15678 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 111 | 16 | mptex 7244 | . . . . . 6
⊢ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V | 
| 112 | 111 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) | 
| 113 | 3 | zred 12724 | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℝ) | 
| 114 |  | 1red 11263 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) | 
| 115 | 113, 114 | resubcld 11692 | . . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) | 
| 116 | 115, 1 | nndivred 12321 | . . . . . . . 8
⊢ (𝜑 → ((𝐽 − 1) / 𝑀) ∈ ℝ) | 
| 117 | 116 | flcld 13839 | . . . . . . 7
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℤ) | 
| 118 | 117 | zcnd 12725 | . . . . . 6
⊢ (𝜑 → (⌊‘((𝐽 − 1) / 𝑀)) ∈ ℂ) | 
| 119 |  | divcnv 15890 | . . . . . 6
⊢
((⌊‘((𝐽
− 1) / 𝑀)) ∈
ℂ → (𝑘 ∈
ℕ ↦ ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘)) ⇝ 0) | 
| 120 | 118, 119 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) ⇝ 0) | 
| 121 | 71 | recnd 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) | 
| 122 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘)) = (𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))) | 
| 123 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑘 = 𝑥 → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) | 
| 124 | 123 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑘) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) | 
| 125 |  | ovexd 7467 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈ V) | 
| 126 | 122, 124,
32, 125 | fvmptd 7022 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) = ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥)) | 
| 127 | 118 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(⌊‘((𝐽 −
1) / 𝑀)) ∈
ℂ) | 
| 128 | 127, 75, 55 | divcld 12044 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑥) ∈
ℂ) | 
| 129 | 126, 128 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥) ∈ ℂ) | 
| 130 | 96, 127, 75, 55 | divsubdird 12083 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) | 
| 131 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) | 
| 132 | 60 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝑘 = 𝑥 → ((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) = ((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀)))) | 
| 133 | 132, 61 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = 𝑥 → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) | 
| 134 | 133 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ) ∧ 𝑘 = 𝑥) → (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) | 
| 135 |  | ovexd 7467 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) →
(((⌊‘(𝑥 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑥) ∈ V) | 
| 136 | 131, 134,
32, 135 | fvmptd 7022 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((⌊‘(𝑥 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑥)) | 
| 137 | 65, 126 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥)) = (((⌊‘(𝑥 / 𝑀)) / 𝑥) − ((⌊‘((𝐽 − 1) / 𝑀)) / 𝑥))) | 
| 138 | 130, 136,
137 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))‘𝑥) = (((𝑘 ∈ ℕ ↦
((⌊‘(𝑘 / 𝑀)) / 𝑘))‘𝑥) − ((𝑘 ∈ ℕ ↦
((⌊‘((𝐽 −
1) / 𝑀)) / 𝑘))‘𝑥))) | 
| 139 | 9, 11, 110, 112, 120, 121, 129, 138 | climsub 15671 | . . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ ((1 / 𝑀) − 0)) | 
| 140 | 139, 46 | breqtrd 5168 | . . 3
⊢ (𝜑 → (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 141 |  | uzssz 12900 | . . . . . . 7
⊢
(ℤ≥‘(𝐽 − 1)) ⊆
ℤ | 
| 142 |  | resmpt 6054 | . . . . . . 7
⊢
((ℤ≥‘(𝐽 − 1)) ⊆ ℤ → ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) | 
| 143 | 141, 142 | ax-mp 5 | . . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) = (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) | 
| 144 | 143 | breq1i 5149 | . . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 145 | 3, 11 | zsubcld 12729 | . . . . . 6
⊢ (𝜑 → (𝐽 − 1) ∈ ℤ) | 
| 146 |  | zex 12624 | . . . . . . 7
⊢ ℤ
∈ V | 
| 147 | 146 | mptex 7244 | . . . . . 6
⊢ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V | 
| 148 |  | climres 15612 | . . . . . 6
⊢ (((𝐽 − 1) ∈ ℤ ∧
(𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ∈ V) → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) | 
| 149 | 145, 147,
148 | sylancl 586 | . . . . 5
⊢ (𝜑 → (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘(𝐽 − 1))) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) | 
| 150 | 144, 149 | bitr3id 285 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) | 
| 151 | 9 | reseq2i 5993 | . . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) | 
| 152 | 151 | breq1i 5149 | . . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾
(ℤ≥‘1)) ⇝ (1 / 𝑀)) | 
| 153 |  | nnssz 12637 | . . . . . . 7
⊢ ℕ
⊆ ℤ | 
| 154 |  | resmpt 6054 | . . . . . . 7
⊢ (ℕ
⊆ ℤ → ((𝑘
∈ ℤ ↦ (((⌊‘(𝑘 / 𝑀)) − (⌊‘((𝐽 − 1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘))) | 
| 155 | 153, 154 | ax-mp 5 | . . . . . 6
⊢ ((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) = (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) | 
| 156 | 155 | breq1i 5149 | . . . . 5
⊢ (((𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ↾ ℕ) ⇝ (1 /
𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 157 |  | climres 15612 | . . . . . 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 301 | . . . 4
⊢ ((𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℤ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 160 | 150, 159 | bitr4di 289 | . . 3
⊢ (𝜑 → ((𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀) ↔ (𝑘 ∈ ℕ ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀))) | 
| 161 | 140, 160 | mpbird 257 | . 2
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
(((⌊‘(𝑘 / 𝑀)) −
(⌊‘((𝐽 −
1) / 𝑀))) / 𝑘)) ⇝ (1 / 𝑀)) | 
| 162 | 8, 161 | eqbrtrd 5164 | 1
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝐽 − 1)) ↦
((♯‘(( ∥ “ {𝑀}) ∩ (𝐽...𝑘))) / 𝑘)) ⇝ (1 / 𝑀)) |