Step |
Hyp |
Ref |
Expression |
1 |
|
flge0nn0 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ) |
2 |
|
logfac |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) ) |
3 |
1 2
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) ) |
4 |
|
fzfid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) |
5 |
|
fzfid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) |
6 |
|
ssrab2 |
⊢ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) |
7 |
|
ssfi |
⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin ) |
8 |
5 6 7
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin ) |
9 |
|
flcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
10 |
9
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
11 |
|
fznn |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ) ) |
12 |
10 11
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ) ) |
13 |
12
|
anbi1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) ) |
14 |
|
nnre |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ ) |
15 |
14
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∈ ℝ ) |
16 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ ) |
17 |
16
|
ad2antrl |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ∈ ℕ ) |
18 |
17
|
nnred |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ∈ ℝ ) |
19 |
|
reflcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
20 |
19
|
ad3antrrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
21 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∥ 𝑛 ) |
22 |
|
nnz |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ ) |
23 |
22
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∈ ℤ ) |
24 |
|
dvdsle |
⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛 ) ) |
25 |
23 17 24
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → ( 𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛 ) ) |
26 |
21 25
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ 𝑛 ) |
27 |
|
elfzle2 |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ≤ ( ⌊ ‘ 𝐴 ) ) |
28 |
27
|
ad2antrl |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ≤ ( ⌊ ‘ 𝐴 ) ) |
29 |
15 18 20 26 28
|
letrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) |
30 |
29
|
expl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
31 |
30
|
pm4.71rd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) ) ) |
32 |
|
an12 |
⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) |
33 |
|
an21 |
⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) ) |
34 |
31 32 33
|
3bitr4g |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) ) |
35 |
13 34
|
bitr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ) ) |
36 |
|
breq2 |
⊢ ( 𝑥 = 𝑛 → ( 𝑘 ∥ 𝑥 ↔ 𝑘 ∥ 𝑛 ) ) |
37 |
36
|
elrab |
⊢ ( 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) |
38 |
37
|
anbi2i |
⊢ ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) |
39 |
|
breq1 |
⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛 ) ) |
40 |
39
|
elrab |
⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) |
41 |
40
|
anbi2i |
⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ) |
42 |
35 38 41
|
3bitr4g |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) ) |
43 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ ) |
45 |
|
vmacl |
⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ ) |
46 |
44 45
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℝ ) |
47 |
46
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ ) |
48 |
47
|
adantrr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ ) |
49 |
4 4 8 42 48
|
fsumcom2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) ) |
50 |
|
fsumconst |
⊢ ( ( { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin ∧ ( Λ ‘ 𝑘 ) ∈ ℂ ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) ) |
51 |
8 47 50
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) ) |
52 |
|
fzfid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ∈ Fin ) |
53 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ ) |
54 |
|
eqid |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) ) = ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) ) |
55 |
53 44 54
|
dvdsflf1o |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) ) : ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) –1-1-onto→ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) |
56 |
52 55
|
hasheqf1od |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ) |
57 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ ) |
58 |
|
nndivre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 / 𝑘 ) ∈ ℝ ) |
59 |
57 43 58
|
syl2an |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑘 ) ∈ ℝ ) |
60 |
|
nngt0 |
⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 ) |
61 |
14 60
|
jca |
⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) |
62 |
43 61
|
syl |
⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) |
63 |
|
divge0 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( 𝐴 / 𝑘 ) ) |
64 |
62 63
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ ( 𝐴 / 𝑘 ) ) |
65 |
|
flge0nn0 |
⊢ ( ( ( 𝐴 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝑘 ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 ) |
66 |
59 64 65
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 ) |
67 |
|
hashfz1 |
⊢ ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) |
68 |
66 67
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) |
69 |
56 68
|
eqtr3d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) |
70 |
69
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) · ( Λ ‘ 𝑘 ) ) ) |
71 |
59
|
flcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℤ ) |
72 |
71
|
zcnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℂ ) |
73 |
72 47
|
mulcomd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) · ( Λ ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) |
74 |
51 70 73
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) |
75 |
74
|
sumeq2dv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) |
76 |
16
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ ) |
77 |
|
vmasum |
⊢ ( 𝑛 ∈ ℕ → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = ( log ‘ 𝑛 ) ) |
78 |
76 77
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = ( log ‘ 𝑛 ) ) |
79 |
78
|
sumeq2dv |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) ) |
80 |
49 75 79
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) ) |
81 |
3 80
|
eqtr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) |