MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  harmonicbnd4 Structured version   Visualization version   GIF version

Theorem harmonicbnd4 26266
Description: The asymptotic behavior of Σ𝑚𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.)
Assertion
Ref Expression
harmonicbnd4 (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴))
Distinct variable group:   𝐴,𝑚

Proof of Theorem harmonicbnd4
StepHypRef Expression
1 fzfid 13799 . . . . . 6 (𝐴 ∈ ℝ+ → (1...(⌊‘𝐴)) ∈ Fin)
2 elfznn 13391 . . . . . . . 8 (𝑚 ∈ (1...(⌊‘𝐴)) → 𝑚 ∈ ℕ)
32adantl 483 . . . . . . 7 ((𝐴 ∈ ℝ+𝑚 ∈ (1...(⌊‘𝐴))) → 𝑚 ∈ ℕ)
43nnrecred 12130 . . . . . 6 ((𝐴 ∈ ℝ+𝑚 ∈ (1...(⌊‘𝐴))) → (1 / 𝑚) ∈ ℝ)
51, 4fsumrecl 15546 . . . . 5 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ∈ ℝ)
65recnd 11109 . . . 4 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ∈ ℂ)
7 relogcl 25837 . . . . 5 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
87recnd 11109 . . . 4 (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℂ)
9 emre 26261 . . . . . 6 γ ∈ ℝ
109a1i 11 . . . . 5 (𝐴 ∈ ℝ+ → γ ∈ ℝ)
1110recnd 11109 . . . 4 (𝐴 ∈ ℝ+ → γ ∈ ℂ)
126, 8, 11subsub4d 11469 . . 3 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ)))
1312fveq2d 6834 . 2 (𝐴 ∈ ℝ+ → (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))))
14 rpreccl 12862 . . . . . 6 (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+)
1514rpred 12878 . . . . 5 (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ)
16 resubcl 11391 . . . . 5 ((γ ∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (γ − (1 / 𝐴)) ∈ ℝ)
179, 15, 16sylancr 588 . . . 4 (𝐴 ∈ ℝ+ → (γ − (1 / 𝐴)) ∈ ℝ)
18 rprege0 12851 . . . . . . . . 9 (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
19 flge0nn0 13646 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
2018, 19syl 17 . . . . . . . 8 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℕ0)
21 nn0p1nn 12378 . . . . . . . 8 ((⌊‘𝐴) ∈ ℕ0 → ((⌊‘𝐴) + 1) ∈ ℕ)
2220, 21syl 17 . . . . . . 7 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) + 1) ∈ ℕ)
2322nnrpd 12876 . . . . . 6 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) + 1) ∈ ℝ+)
24 relogcl 25837 . . . . . 6 (((⌊‘𝐴) + 1) ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈ ℝ)
2523, 24syl 17 . . . . 5 (𝐴 ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈ ℝ)
265, 25resubcld 11509 . . . 4 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ ℝ)
275, 7resubcld 11509 . . . 4 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) ∈ ℝ)
2822nnrecred 12130 . . . . . 6 (𝐴 ∈ ℝ+ → (1 / ((⌊‘𝐴) + 1)) ∈ ℝ)
29 fzfid 13799 . . . . . . . 8 (𝐴 ∈ ℝ+ → (1...((⌊‘𝐴) + 1)) ∈ Fin)
30 elfznn 13391 . . . . . . . . . 10 (𝑚 ∈ (1...((⌊‘𝐴) + 1)) → 𝑚 ∈ ℕ)
3130adantl 483 . . . . . . . . 9 ((𝐴 ∈ ℝ+𝑚 ∈ (1...((⌊‘𝐴) + 1))) → 𝑚 ∈ ℕ)
3231nnrecred 12130 . . . . . . . 8 ((𝐴 ∈ ℝ+𝑚 ∈ (1...((⌊‘𝐴) + 1))) → (1 / 𝑚) ∈ ℝ)
3329, 32fsumrecl 15546 . . . . . . 7 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) ∈ ℝ)
3433, 25resubcld 11509 . . . . . 6 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ ℝ)
35 harmonicbnd 26259 . . . . . . . 8 (((⌊‘𝐴) + 1) ∈ ℕ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1))
3622, 35syl 17 . . . . . . 7 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1))
37 1re 11081 . . . . . . . . 9 1 ∈ ℝ
389, 37elicc2i 13251 . . . . . . . 8 ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) ↔ ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ γ ≤ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤ 1))
3938simp2bi 1146 . . . . . . 7 ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) → γ ≤ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
4036, 39syl 17 . . . . . 6 (𝐴 ∈ ℝ+ → γ ≤ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
41 rpre 12844 . . . . . . . 8 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
42 fllep1 13627 . . . . . . . 8 (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1))
4341, 42syl 17 . . . . . . 7 (𝐴 ∈ ℝ+𝐴 ≤ ((⌊‘𝐴) + 1))
44 rpregt0 12850 . . . . . . . 8 (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4522nnred 12094 . . . . . . . 8 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) + 1) ∈ ℝ)
4622nngt0d 12128 . . . . . . . 8 (𝐴 ∈ ℝ+ → 0 < ((⌊‘𝐴) + 1))
47 lerec 11964 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (((⌊‘𝐴) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝐴) + 1))) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴)))
4844, 45, 46, 47syl12anc 835 . . . . . . 7 (𝐴 ∈ ℝ+ → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴)))
4943, 48mpbid 231 . . . . . 6 (𝐴 ∈ ℝ+ → (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))
5010, 28, 34, 15, 40, 49le2subd 11701 . . . . 5 (𝐴 ∈ ℝ+ → (γ − (1 / 𝐴)) ≤ ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))))
5133recnd 11109 . . . . . . 7 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) ∈ ℂ)
5225recnd 11109 . . . . . . 7 (𝐴 ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈ ℂ)
5328recnd 11109 . . . . . . 7 (𝐴 ∈ ℝ+ → (1 / ((⌊‘𝐴) + 1)) ∈ ℂ)
5451, 52, 53sub32d 11470 . . . . . 6 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (1 / ((⌊‘𝐴) + 1))) − (log‘((⌊‘𝐴) + 1))))
55 nnuz 12727 . . . . . . . . . . 11 ℕ = (ℤ‘1)
5622, 55eleqtrdi 2848 . . . . . . . . . 10 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) + 1) ∈ (ℤ‘1))
5732recnd 11109 . . . . . . . . . 10 ((𝐴 ∈ ℝ+𝑚 ∈ (1...((⌊‘𝐴) + 1))) → (1 / 𝑚) ∈ ℂ)
58 oveq2 7350 . . . . . . . . . 10 (𝑚 = ((⌊‘𝐴) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝐴) + 1)))
5956, 57, 58fsumm1 15563 . . . . . . . . 9 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) = (Σ𝑚 ∈ (1...(((⌊‘𝐴) + 1) − 1))(1 / 𝑚) + (1 / ((⌊‘𝐴) + 1))))
6020nn0cnd 12401 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℂ)
61 ax-1cn 11035 . . . . . . . . . . . . 13 1 ∈ ℂ
62 pncan 11333 . . . . . . . . . . . . 13 (((⌊‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝐴) + 1) − 1) = (⌊‘𝐴))
6360, 61, 62sylancl 587 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) − 1) = (⌊‘𝐴))
6463oveq2d 7358 . . . . . . . . . . 11 (𝐴 ∈ ℝ+ → (1...(((⌊‘𝐴) + 1) − 1)) = (1...(⌊‘𝐴)))
6564sumeq1d 15513 . . . . . . . . . 10 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...(((⌊‘𝐴) + 1) − 1))(1 / 𝑚) = Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))
6665oveq1d 7357 . . . . . . . . 9 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(((⌊‘𝐴) + 1) − 1))(1 / 𝑚) + (1 / ((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) + (1 / ((⌊‘𝐴) + 1))))
6759, 66eqtrd 2777 . . . . . . . 8 (𝐴 ∈ ℝ+ → Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) + (1 / ((⌊‘𝐴) + 1))))
686, 53, 67mvrraddd 11493 . . . . . . 7 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (1 / ((⌊‘𝐴) + 1))) = Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))
6968oveq1d 7357 . . . . . 6 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (1 / ((⌊‘𝐴) + 1))) − (log‘((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
7054, 69eqtrd 2777 . . . . 5 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
7150, 70breqtrd 5123 . . . 4 (𝐴 ∈ ℝ+ → (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
72 logleb 25864 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ ((⌊‘𝐴) + 1) ∈ ℝ+) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1))))
7323, 72mpdan 685 . . . . . 6 (𝐴 ∈ ℝ+ → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1))))
7443, 73mpbid 231 . . . . 5 (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1)))
757, 25, 5, 74lesub2dd 11698 . . . 4 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)))
7617, 26, 27, 71, 75letrd 11238 . . 3 (𝐴 ∈ ℝ+ → (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)))
7727, 15resubcld 11509 . . . . 5 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − (1 / 𝐴)) ∈ ℝ)
7815recnd 11109 . . . . . . 7 (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℂ)
796, 8, 78subsub4d 11469 . . . . . 6 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − (1 / 𝐴)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + (1 / 𝐴))))
807, 15readdcld 11110 . . . . . . 7 (𝐴 ∈ ℝ+ → ((log‘𝐴) + (1 / 𝐴)) ∈ ℝ)
81 id 22 . . . . . . . . . 10 (𝐴 ∈ ℝ+𝐴 ∈ ℝ+)
8223, 81relogdivd 25887 . . . . . . . . 9 (𝐴 ∈ ℝ+ → (log‘(((⌊‘𝐴) + 1) / 𝐴)) = ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)))
83 rerpdivcl 12866 . . . . . . . . . . . . 13 ((((⌊‘𝐴) + 1) ∈ ℝ ∧ 𝐴 ∈ ℝ+) → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ)
8445, 83mpancom 686 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ)
8537a1i 11 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+ → 1 ∈ ℝ)
8685, 15readdcld 11110 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (1 + (1 / 𝐴)) ∈ ℝ)
8715reefcld 15897 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (exp‘(1 / 𝐴)) ∈ ℝ)
8861a1i 11 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ+ → 1 ∈ ℂ)
89 rpcnne0 12854 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
90 divdir 11764 . . . . . . . . . . . . . 14 (((⌊‘𝐴) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (((⌊‘𝐴) + 1) / 𝐴) = (((⌊‘𝐴) / 𝐴) + (1 / 𝐴)))
9160, 88, 89, 90syl3anc 1371 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) / 𝐴) = (((⌊‘𝐴) / 𝐴) + (1 / 𝐴)))
92 reflcl 13622 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ)
9341, 92syl 17 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℝ)
94 rerpdivcl 12866 . . . . . . . . . . . . . . 15 (((⌊‘𝐴) ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((⌊‘𝐴) / 𝐴) ∈ ℝ)
9593, 94mpancom 686 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) / 𝐴) ∈ ℝ)
96 flle 13625 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ 𝐴)
9741, 96syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ≤ 𝐴)
98 rpcn 12846 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℝ+𝐴 ∈ ℂ)
9998mulid1d 11098 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℝ+ → (𝐴 · 1) = 𝐴)
10097, 99breqtrrd 5125 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ≤ (𝐴 · 1))
101 ledivmul 11957 . . . . . . . . . . . . . . . 16 (((⌊‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (((⌊‘𝐴) / 𝐴) ≤ 1 ↔ (⌊‘𝐴) ≤ (𝐴 · 1)))
10293, 85, 44, 101syl3anc 1371 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) / 𝐴) ≤ 1 ↔ (⌊‘𝐴) ≤ (𝐴 · 1)))
103100, 102mpbird 257 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) / 𝐴) ≤ 1)
10495, 85, 15, 103leadd1dd 11695 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) / 𝐴) + (1 / 𝐴)) ≤ (1 + (1 / 𝐴)))
10591, 104eqbrtrd 5119 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) / 𝐴) ≤ (1 + (1 / 𝐴)))
106 efgt1p 15924 . . . . . . . . . . . . . 14 ((1 / 𝐴) ∈ ℝ+ → (1 + (1 / 𝐴)) < (exp‘(1 / 𝐴)))
10714, 106syl 17 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ+ → (1 + (1 / 𝐴)) < (exp‘(1 / 𝐴)))
10886, 87, 107ltled 11229 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (1 + (1 / 𝐴)) ≤ (exp‘(1 / 𝐴)))
10984, 86, 87, 105, 108letrd 11238 . . . . . . . . . . 11 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) / 𝐴) ≤ (exp‘(1 / 𝐴)))
110 rpdivcl 12861 . . . . . . . . . . . . 13 ((((⌊‘𝐴) + 1) ∈ ℝ+𝐴 ∈ ℝ+) → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ+)
11123, 110mpancom 686 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ+)
11215rpefcld 15914 . . . . . . . . . . . 12 (𝐴 ∈ ℝ+ → (exp‘(1 / 𝐴)) ∈ ℝ+)
113111, 112logled 25888 . . . . . . . . . . 11 (𝐴 ∈ ℝ+ → ((((⌊‘𝐴) + 1) / 𝐴) ≤ (exp‘(1 / 𝐴)) ↔ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴)))))
114109, 113mpbid 231 . . . . . . . . . 10 (𝐴 ∈ ℝ+ → (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴))))
11515relogefd 25889 . . . . . . . . . 10 (𝐴 ∈ ℝ+ → (log‘(exp‘(1 / 𝐴))) = (1 / 𝐴))
116114, 115breqtrd 5123 . . . . . . . . 9 (𝐴 ∈ ℝ+ → (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (1 / 𝐴))
11782, 116eqbrtrrd 5121 . . . . . . . 8 (𝐴 ∈ ℝ+ → ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴))
11825, 7, 15lesubadd2d 11680 . . . . . . . 8 (𝐴 ∈ ℝ+ → (((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴) ↔ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴))))
119117, 118mpbid 231 . . . . . . 7 (𝐴 ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴)))
12025, 80, 5, 119lesub2dd 11698 . . . . . 6 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + (1 / 𝐴))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
12179, 120eqbrtrd 5119 . . . . 5 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))))
122 harmonicbnd3 26263 . . . . . . 7 ((⌊‘𝐴) ∈ ℕ0 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ))
12320, 122syl 17 . . . . . 6 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ))
124 0re 11083 . . . . . . . 8 0 ∈ ℝ
125124, 9elicc2i 13251 . . . . . . 7 ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) ↔ ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ 0 ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤ γ))
126125simp3bi 1147 . . . . . 6 ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤ γ)
127123, 126syl 17 . . . . 5 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤ γ)
12877, 26, 10, 121, 127letrd 11238 . . . 4 (𝐴 ∈ ℝ+ → ((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ γ)
12927, 15, 10lesubaddd 11678 . . . 4 (𝐴 ∈ ℝ+ → (((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ γ ↔ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))))
130128, 129mpbid 231 . . 3 (𝐴 ∈ ℝ+ → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴)))
13127, 10, 15absdifled 15246 . . 3 (𝐴 ∈ ℝ+ → ((abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴) ↔ ((γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) ∧ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴)))))
13276, 130, 131mpbir2and 711 . 2 (𝐴 ∈ ℝ+ → (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴))
13313, 132eqbrtrrd 5121 1 (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wne 2941   class class class wbr 5097  cfv 6484  (class class class)co 7342  cc 10975  cr 10976  0cc0 10977  1c1 10978   + caddc 10980   · cmul 10982   < clt 11115  cle 11116  cmin 11311   / cdiv 11738  cn 12079  0cn0 12339  cuz 12688  +crp 12836  [,]cicc 13188  ...cfz 13345  cfl 13616  abscabs 15045  Σcsu 15497  expce 15871  logclog 25816  γcem 26247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-addf 11056  ax-mulf 11057
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-oadd 8376  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-xnn0 12412  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ioc 13190  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-fl 13618  df-mod 13696  df-seq 13828  df-exp 13889  df-fac 14094  df-bc 14123  df-hash 14151  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498  df-ef 15877  df-e 15878  df-sin 15879  df-cos 15880  df-tan 15881  df-pi 15882  df-dvds 16064  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137  df-ulm 25642  df-log 25818  df-atan 26123  df-em 26248
This theorem is referenced by:  mulogsumlem  26785  mulog2sumlem1  26788
  Copyright terms: Public domain W3C validator