| Step | Hyp | Ref
| Expression |
| 1 | | flge0nn0 13860 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
| 2 | | logfac 26643 |
. . 3
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 4 | | fzfid 14014 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(1...(⌊‘𝐴))
∈ Fin) |
| 5 | | fzfid 14014 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘𝐴)) ∈ Fin) |
| 6 | | ssrab2 4080 |
. . . . 5
⊢ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ⊆
(1...(⌊‘𝐴)) |
| 7 | | ssfi 9213 |
. . . . 5
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ⊆ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
| 8 | 5, 6, 7 | sylancl 586 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
| 9 | | flcl 13835 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
| 10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℤ) |
| 11 | | fznn 13632 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℤ → (𝑘
∈ (1...(⌊‘𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)))) |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ (𝑘 ∈ ℕ
∧ 𝑘 ≤
(⌊‘𝐴)))) |
| 13 | 12 | anbi1d 631 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
| 14 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 15 | 14 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℝ) |
| 16 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
| 17 | 16 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℕ) |
| 18 | 17 | nnred 12281 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℝ) |
| 19 | | reflcl 13836 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 20 | 19 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (⌊‘𝐴) ∈ ℝ) |
| 21 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∥ 𝑛) |
| 22 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
| 23 | 22 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℤ) |
| 24 | | dvdsle 16347 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
| 25 | 23, 17, 24 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
| 26 | 21, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ 𝑛) |
| 27 | | elfzle2 13568 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ≤
(⌊‘𝐴)) |
| 28 | 27 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ≤ (⌊‘𝐴)) |
| 29 | 15, 18, 20, 26, 28 | letrd 11418 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴)) |
| 30 | 29 | expl 457 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴))) |
| 31 | 30 | pm4.71rd 562 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))))) |
| 32 | | an12 645 |
. . . . . . 7
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
| 33 | | an21 644 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
| 34 | 31, 32, 33 | 3bitr4g 314 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
| 35 | 13, 34 | bitr4d 282 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)))) |
| 36 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑘 ∥ 𝑥 ↔ 𝑘 ∥ 𝑛)) |
| 37 | 36 | elrab 3692 |
. . . . . 6
⊢ (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) |
| 38 | 37 | anbi2i 623 |
. . . . 5
⊢ ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
| 39 | | breq1 5146 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
| 40 | 39 | elrab 3692 |
. . . . . 6
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)) |
| 41 | 40 | anbi2i 623 |
. . . . 5
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛))) |
| 42 | 35, 38, 41 | 3bitr4g 314 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}))) |
| 43 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ 𝑘 ∈
ℕ) |
| 44 | 43 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝑘 ∈ ℕ) |
| 45 | | vmacl 27161 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
| 46 | 44, 45 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℝ) |
| 47 | 46 | recnd 11289 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℂ) |
| 48 | 47 | adantrr 717 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥})) → (Λ‘𝑘) ∈
ℂ) |
| 49 | 4, 4, 8, 42, 48 | fsumcom2 15810 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘)) |
| 50 | | fsumconst 15826 |
. . . . . 6
⊢ (({𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ∈ Fin ∧
(Λ‘𝑘) ∈
ℂ) → Σ𝑛
∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ·
(Λ‘𝑘))) |
| 51 | 8, 47, 50 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) · (Λ‘𝑘))) |
| 52 | | fzfid 14014 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑘))) ∈ Fin) |
| 53 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
| 54 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑘))) ↦ (𝑘 · 𝑚)) = (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)) |
| 55 | 53, 44, 54 | dvdsflf1o 27230 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)):(1...(⌊‘(𝐴 / 𝑘)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) |
| 56 | 52, 55 | hasheqf1od 14392 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥})) |
| 57 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℝ) |
| 58 | | nndivre 12307 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝐴 / 𝑘) ∈ ℝ) |
| 59 | 57, 43, 58 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑘) ∈ ℝ) |
| 60 | | nngt0 12297 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
| 61 | 14, 60 | jca 511 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 62 | 43, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ (𝑘 ∈ ℝ
∧ 0 < 𝑘)) |
| 63 | | divge0 12137 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝐴 / 𝑘)) |
| 64 | 62, 63 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 0 ≤ (𝐴 / 𝑘)) |
| 65 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ (((𝐴 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑘)) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
| 66 | 59, 64, 65 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
| 67 | | hashfz1 14385 |
. . . . . . . 8
⊢
((⌊‘(𝐴 /
𝑘)) ∈
ℕ0 → (♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
| 68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
| 69 | 56, 68 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) = (⌊‘(𝐴 / 𝑘))) |
| 70 | 69 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ·
(Λ‘𝑘)) =
((⌊‘(𝐴 / 𝑘)) ·
(Λ‘𝑘))) |
| 71 | 59 | flcld 13838 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℤ) |
| 72 | 71 | zcnd 12723 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℂ) |
| 73 | 72, 47 | mulcomd 11282 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘)) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
| 74 | 51, 70, 73 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
| 75 | 74 | sumeq2dv 15738 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
| 76 | 16 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
| 77 | | vmasum 27260 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
| 78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
| 79 | 78 | sumeq2dv 15738 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 80 | 49, 75, 79 | 3eqtr3d 2785 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 81 | 3, 80 | eqtr4d 2780 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |