Step | Hyp | Ref
| Expression |
1 | | flge0nn0 13395 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
2 | | logfac 25489 |
. . 3
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
4 | | fzfid 13546 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(1...(⌊‘𝐴))
∈ Fin) |
5 | | fzfid 13546 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘𝐴)) ∈ Fin) |
6 | | ssrab2 3993 |
. . . . 5
⊢ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ⊆
(1...(⌊‘𝐴)) |
7 | | ssfi 8851 |
. . . . 5
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ⊆ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
8 | 5, 6, 7 | sylancl 589 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
9 | | flcl 13370 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
10 | 9 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℤ) |
11 | | fznn 13180 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℤ → (𝑘
∈ (1...(⌊‘𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)))) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ (𝑘 ∈ ℕ
∧ 𝑘 ≤
(⌊‘𝐴)))) |
13 | 12 | anbi1d 633 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
14 | | nnre 11837 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
15 | 14 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℝ) |
16 | | elfznn 13141 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
17 | 16 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℕ) |
18 | 17 | nnred 11845 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℝ) |
19 | | reflcl 13371 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
20 | 19 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (⌊‘𝐴) ∈ ℝ) |
21 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∥ 𝑛) |
22 | | nnz 12199 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
23 | 22 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℤ) |
24 | | dvdsle 15871 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
25 | 23, 17, 24 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
26 | 21, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ 𝑛) |
27 | | elfzle2 13116 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ≤
(⌊‘𝐴)) |
28 | 27 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ≤ (⌊‘𝐴)) |
29 | 15, 18, 20, 26, 28 | letrd 10989 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴)) |
30 | 29 | expl 461 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴))) |
31 | 30 | pm4.71rd 566 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))))) |
32 | | an12 645 |
. . . . . . 7
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
33 | | an21 644 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
34 | 31, 32, 33 | 3bitr4g 317 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
35 | 13, 34 | bitr4d 285 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)))) |
36 | | breq2 5057 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑘 ∥ 𝑥 ↔ 𝑘 ∥ 𝑛)) |
37 | 36 | elrab 3602 |
. . . . . 6
⊢ (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) |
38 | 37 | anbi2i 626 |
. . . . 5
⊢ ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
39 | | breq1 5056 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
40 | 39 | elrab 3602 |
. . . . . 6
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)) |
41 | 40 | anbi2i 626 |
. . . . 5
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛))) |
42 | 35, 38, 41 | 3bitr4g 317 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}))) |
43 | | elfznn 13141 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ 𝑘 ∈
ℕ) |
44 | 43 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝑘 ∈ ℕ) |
45 | | vmacl 26000 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℝ) |
47 | 46 | recnd 10861 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℂ) |
48 | 47 | adantrr 717 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥})) → (Λ‘𝑘) ∈
ℂ) |
49 | 4, 4, 8, 42, 48 | fsumcom2 15338 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘)) |
50 | | fsumconst 15354 |
. . . . . 6
⊢ (({𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ∈ Fin ∧
(Λ‘𝑘) ∈
ℂ) → Σ𝑛
∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ·
(Λ‘𝑘))) |
51 | 8, 47, 50 | syl2anc 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) · (Λ‘𝑘))) |
52 | | fzfid 13546 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑘))) ∈ Fin) |
53 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
54 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑘))) ↦ (𝑘 · 𝑚)) = (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)) |
55 | 53, 44, 54 | dvdsflf1o 26069 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)):(1...(⌊‘(𝐴 / 𝑘)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) |
56 | 52, 55 | hasheqf1od 13920 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (♯‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥})) |
57 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℝ) |
58 | | nndivre 11871 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝐴 / 𝑘) ∈ ℝ) |
59 | 57, 43, 58 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑘) ∈ ℝ) |
60 | | nngt0 11861 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
61 | 14, 60 | jca 515 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
62 | 43, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ (𝑘 ∈ ℝ
∧ 0 < 𝑘)) |
63 | | divge0 11701 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝐴 / 𝑘)) |
64 | 62, 63 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 0 ≤ (𝐴 / 𝑘)) |
65 | | flge0nn0 13395 |
. . . . . . . . 9
⊢ (((𝐴 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑘)) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
66 | 59, 64, 65 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
67 | | hashfz1 13912 |
. . . . . . . 8
⊢
((⌊‘(𝐴 /
𝑘)) ∈
ℕ0 → (♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(♯‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
69 | 56, 68 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) = (⌊‘(𝐴 / 𝑘))) |
70 | 69 | oveq1d 7228 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((♯‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ·
(Λ‘𝑘)) =
((⌊‘(𝐴 / 𝑘)) ·
(Λ‘𝑘))) |
71 | 59 | flcld 13373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℤ) |
72 | 71 | zcnd 12283 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℂ) |
73 | 72, 47 | mulcomd 10854 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘)) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
74 | 51, 70, 73 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
75 | 74 | sumeq2dv 15267 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
76 | 16 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
77 | | vmasum 26097 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
78 | 76, 77 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
79 | 78 | sumeq2dv 15267 |
. . 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...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |