Step | Hyp | Ref
| Expression |
1 | | flge0nn0 12621 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
2 | | logfac 24347 |
. . 3
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
4 | | fzfid 12772 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(1...(⌊‘𝐴))
∈ Fin) |
5 | | fzfid 12772 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘𝐴)) ∈ Fin) |
6 | | ssrab2 3687 |
. . . . 5
⊢ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ⊆
(1...(⌊‘𝐴)) |
7 | | ssfi 8180 |
. . . . 5
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ⊆ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
8 | 5, 6, 7 | sylancl 694 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ∈ Fin) |
9 | | flcl 12596 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℤ) |
10 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℤ) |
11 | | fznn 12408 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℤ → (𝑘
∈ (1...(⌊‘𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)))) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ (𝑘 ∈ ℕ
∧ 𝑘 ≤
(⌊‘𝐴)))) |
13 | 12 | anbi1d 741 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
14 | | nnre 11027 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
15 | 14 | ad2antlr 763 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℝ) |
16 | | elfznn 12370 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
17 | 16 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℕ) |
18 | 17 | nnred 11035 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ∈ ℝ) |
19 | | reflcl 12597 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
20 | 19 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (⌊‘𝐴) ∈ ℝ) |
21 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∥ 𝑛) |
22 | | nnz 11399 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
23 | 22 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ∈ ℤ) |
24 | | dvdsle 15032 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
25 | 23, 17, 24 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → (𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛)) |
26 | 21, 25 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ 𝑛) |
27 | | elfzle2 12345 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ≤
(⌊‘𝐴)) |
28 | 27 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑛 ≤ (⌊‘𝐴)) |
29 | 15, 18, 20, 26, 28 | letrd 10194 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴)) |
30 | 29 | expl 648 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) → 𝑘 ≤ (⌊‘𝐴))) |
31 | 30 | pm4.71rd 667 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈ ℕ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))))) |
32 | | an12 838 |
. . . . . . 7
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
33 | | anass 681 |
. . . . . . . 8
⊢ (((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ∈ ℕ ∧ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
34 | | an12 838 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
35 | 33, 34 | bitri 264 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) ↔ (𝑘 ≤ (⌊‘𝐴) ∧ (𝑘 ∈ ℕ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
36 | 31, 32, 35 | 3bitr4g 303 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑛 ∈
(1...(⌊‘𝐴))
∧ (𝑘 ∈ ℕ
∧ 𝑘 ∥ 𝑛)) ↔ ((𝑘 ∈ ℕ ∧ 𝑘 ≤ (⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)))) |
37 | 13, 36 | bitr4d 271 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∥ 𝑛)) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)))) |
38 | | breq2 4657 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑘 ∥ 𝑥 ↔ 𝑘 ∥ 𝑛)) |
39 | 38 | elrab 3363 |
. . . . . 6
⊢ (𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛)) |
40 | 39 | anbi2i 730 |
. . . . 5
⊢ ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∥ 𝑛))) |
41 | | breq1 4656 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝑥 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
42 | 41 | elrab 3363 |
. . . . . 6
⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} ↔ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛)) |
43 | 42 | anbi2i 730 |
. . . . 5
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛))) |
44 | 37, 40, 43 | 3bitr4g 303 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ↔ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛}))) |
45 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ 𝑘 ∈
ℕ) |
46 | 45 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝑘 ∈ ℕ) |
47 | | vmacl 24844 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℝ) |
49 | 48 | recnd 10068 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑘) ∈
ℂ) |
50 | 49 | adantrr 753 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥})) → (Λ‘𝑘) ∈
ℂ) |
51 | 4, 4, 8, 44, 50 | fsumcom2 14505 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘)) |
52 | | fsumconst 14522 |
. . . . . 6
⊢ (({𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} ∈ Fin ∧
(Λ‘𝑘) ∈
ℂ) → Σ𝑛
∈ {𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((#‘{𝑥 ∈
(1...(⌊‘𝐴))
∣ 𝑘 ∥ 𝑥}) ·
(Λ‘𝑘))) |
53 | 8, 49, 52 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((#‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) · (Λ‘𝑘))) |
54 | | fzfid 12772 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑘))) ∈ Fin) |
55 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
56 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘(𝐴 /
𝑘))) ↦ (𝑘 · 𝑚)) = (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)) |
57 | 55, 46, 56 | dvdsflf1o 24913 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)):(1...(⌊‘(𝐴 / 𝑘)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) |
58 | | f1oeng 7974 |
. . . . . . . . 9
⊢
(((1...(⌊‘(𝐴 / 𝑘))) ∈ Fin ∧ (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑘))) ↦ (𝑘 · 𝑚)):(1...(⌊‘(𝐴 / 𝑘)))–1-1-onto→{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) → (1...(⌊‘(𝐴 / 𝑘))) ≈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) |
59 | 54, 57, 58 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (1...(⌊‘(𝐴 / 𝑘))) ≈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) |
60 | | hasheni 13136 |
. . . . . . . 8
⊢
((1...(⌊‘(𝐴 / 𝑘))) ≈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} → (#‘(1...(⌊‘(𝐴 / 𝑘)))) = (#‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥})) |
61 | 59, 60 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(#‘(1...(⌊‘(𝐴 / 𝑘)))) = (#‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥})) |
62 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈ ℝ) |
63 | | nndivre 11056 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝐴 / 𝑘) ∈ ℝ) |
64 | 62, 45, 63 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (𝐴 / 𝑘) ∈ ℝ) |
65 | | nngt0 11049 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
66 | 14, 65 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
67 | 45, 66 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ (𝑘 ∈ ℝ
∧ 0 < 𝑘)) |
68 | | divge0 10892 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑘 ∈ ℝ ∧ 0 <
𝑘)) → 0 ≤ (𝐴 / 𝑘)) |
69 | 67, 68 | sylan2 491 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → 0 ≤ (𝐴 / 𝑘)) |
70 | | flge0nn0 12621 |
. . . . . . . . 9
⊢ (((𝐴 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑘)) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
71 | 64, 69, 70 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈
ℕ0) |
72 | | hashfz1 13134 |
. . . . . . . 8
⊢
((⌊‘(𝐴 /
𝑘)) ∈
ℕ0 → (#‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
73 | 71, 72 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) →
(#‘(1...(⌊‘(𝐴 / 𝑘)))) = (⌊‘(𝐴 / 𝑘))) |
74 | 61, 73 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (#‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) = (⌊‘(𝐴 / 𝑘))) |
75 | 74 | oveq1d 6665 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((#‘{𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥}) · (Λ‘𝑘)) = ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘))) |
76 | 64 | flcld 12599 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℤ) |
77 | 76 | zcnd 11483 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → (⌊‘(𝐴 / 𝑘)) ∈ ℂ) |
78 | 77, 49 | mulcomd 10061 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → ((⌊‘(𝐴 / 𝑘)) · (Λ‘𝑘)) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
79 | 53, 75, 78 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑘 ∈ (1...(⌊‘𝐴))) → Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = ((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
80 | 79 | sumeq2dv 14433 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))Σ𝑛 ∈ {𝑥 ∈ (1...(⌊‘𝐴)) ∣ 𝑘 ∥ 𝑥} (Λ‘𝑘) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |
81 | 16 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
82 | | vmasum 24941 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
83 | 81, 82 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = (log‘𝑛)) |
84 | 83 | sumeq2dv 14433 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (Λ‘𝑘) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
85 | 51, 80, 84 | 3eqtr3d 2664 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → Σ𝑘 ∈
(1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
86 | 3, 85 | eqtr4d 2659 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(log‘(!‘(⌊‘𝐴))) = Σ𝑘 ∈ (1...(⌊‘𝐴))((Λ‘𝑘) · (⌊‘(𝐴 / 𝑘)))) |