Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) |
2 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ ) |
3 |
2
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ ) |
4 |
3
|
nnrecred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ ) |
5 |
1 4
|
fsumrecl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℝ ) |
6 |
|
flge1nn |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ ) |
7 |
6
|
nnrpd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ+ ) |
8 |
7
|
relogcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ) |
9 |
|
peano2re |
⊢ ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ∈ ℝ ) |
10 |
8 9
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ∈ ℝ ) |
11 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ ) |
12 |
|
0red |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ∈ ℝ ) |
13 |
|
1re |
⊢ 1 ∈ ℝ |
14 |
13
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ∈ ℝ ) |
15 |
|
0lt1 |
⊢ 0 < 1 |
16 |
15
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 1 ) |
17 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 ) |
18 |
12 14 11 16 17
|
ltletrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 𝐴 ) |
19 |
11 18
|
elrpd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ ) |
20 |
19
|
relogcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ ) |
21 |
|
peano2re |
⊢ ( ( log ‘ 𝐴 ) ∈ ℝ → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
22 |
20 21
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ ) |
23 |
|
harmonicbnd |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) ) |
24 |
6 23
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) ) |
25 |
|
emre |
⊢ γ ∈ ℝ |
26 |
25 13
|
elicc2i |
⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) ↔ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ℝ ∧ γ ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ) ) |
27 |
26
|
simp3bi |
⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ) |
28 |
24 27
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ) |
29 |
5 8 14
|
lesubadd2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ↔ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ) ) |
30 |
28 29
|
mpbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ) |
31 |
|
flle |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
32 |
31
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
33 |
7 19
|
logled |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ↔ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) ) |
34 |
32 33
|
mpbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) |
35 |
8 20 14 34
|
leadd1dd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) ) |
36 |
5 10 22 30 35
|
letrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) ) |