Proof of Theorem emcllem2
| Step | Hyp | Ref
| Expression |
| 1 | | peano2nn 12278 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
| 2 | 1 | nnrecred 12317 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 + 1)) ∈
ℝ) |
| 3 | 1 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ+) |
| 4 | 3 | relogcld 26665 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘(𝑁 + 1)) ∈
ℝ) |
| 5 | | nnrp 13046 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
| 6 | 5 | relogcld 26665 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ∈
ℝ) |
| 7 | 4, 6 | resubcld 11691 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((log‘(𝑁 + 1))
− (log‘𝑁))
∈ ℝ) |
| 8 | | fzfid 14014 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
| 9 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1...𝑁) → 𝑚 ∈ ℕ) |
| 10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ∈ ℕ) |
| 11 | 10 | nnrecred 12317 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...𝑁)) → (1 / 𝑚) ∈ ℝ) |
| 12 | 8, 11 | fsumrecl 15770 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) ∈ ℝ) |
| 13 | 3 | rpreccld 13087 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 + 1)) ∈
ℝ+) |
| 14 | 13 | rpge0d 13081 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 ≤ (1
/ (𝑁 +
1))) |
| 15 | | 1div1e1 11958 |
. . . . . . . . . . . 12
⊢ (1 / 1) =
1 |
| 16 | | 1re 11261 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
| 17 | | ltaddrp 13072 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝑁
∈ ℝ+) → 1 < (1 + 𝑁)) |
| 18 | 16, 5, 17 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 1 < (1
+ 𝑁)) |
| 19 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 20 | | nncn 12274 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 21 | | addcom 11447 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ 𝑁
∈ ℂ) → (1 + 𝑁) = (𝑁 + 1)) |
| 22 | 19, 20, 21 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (1 +
𝑁) = (𝑁 + 1)) |
| 23 | 18, 22 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 1 <
(𝑁 + 1)) |
| 24 | 15, 23 | eqbrtrid 5178 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (1 / 1)
< (𝑁 +
1)) |
| 25 | 1 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
| 26 | 1 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
| 27 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 28 | | ltrec1 12155 |
. . . . . . . . . . . . 13
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑁 + 1) ∈ ℝ ∧ 0 < (𝑁 + 1))) → ((1 / 1) <
(𝑁 + 1) ↔ (1 / (𝑁 + 1)) < 1)) |
| 29 | 16, 27, 28 | mpanl12 702 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) ∈ ℝ ∧ 0
< (𝑁 + 1)) → ((1 /
1) < (𝑁 + 1) ↔ (1 /
(𝑁 + 1)) <
1)) |
| 30 | 25, 26, 29 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((1 / 1)
< (𝑁 + 1) ↔ (1 /
(𝑁 + 1)) <
1)) |
| 31 | 24, 30 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 + 1)) <
1) |
| 32 | 2, 14, 31 | eflegeo 16157 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(exp‘(1 / (𝑁 + 1)))
≤ (1 / (1 − (1 / (𝑁 + 1))))) |
| 33 | 25 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
| 34 | | nnne0 12300 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 35 | 1 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0) |
| 36 | 20, 33, 34, 35 | recdivd 12060 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 / (𝑁 + 1))) = ((𝑁 + 1) / 𝑁)) |
| 37 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
| 38 | 33, 37, 33, 35 | divsubdird 12082 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) / (𝑁 + 1)) = (((𝑁 + 1) / (𝑁 + 1)) − (1 / (𝑁 + 1)))) |
| 39 | | pncan 11514 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
| 40 | 20, 19, 39 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
| 41 | 40 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) / (𝑁 + 1)) = (𝑁 / (𝑁 + 1))) |
| 42 | 33, 35 | dividd 12041 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / (𝑁 + 1)) = 1) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / (𝑁 + 1)) − (1 / (𝑁 + 1))) = (1 − (1 / (𝑁 + 1)))) |
| 44 | 38, 41, 43 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (1
− (1 / (𝑁 + 1))) =
(𝑁 / (𝑁 + 1))) |
| 45 | 44 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 / (1
− (1 / (𝑁 + 1)))) =
(1 / (𝑁 / (𝑁 + 1)))) |
| 46 | 3, 5 | rpdivcld 13094 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈
ℝ+) |
| 47 | 46 | reeflogd 26666 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(exp‘(log‘((𝑁 +
1) / 𝑁))) = ((𝑁 + 1) / 𝑁)) |
| 48 | 36, 45, 47 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (1 / (1
− (1 / (𝑁 + 1)))) =
(exp‘(log‘((𝑁 +
1) / 𝑁)))) |
| 49 | 32, 48 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(exp‘(1 / (𝑁 + 1)))
≤ (exp‘(log‘((𝑁 + 1) / 𝑁)))) |
| 50 | 3, 5 | relogdivd 26668 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) / 𝑁)) = ((log‘(𝑁 + 1)) − (log‘𝑁))) |
| 51 | 50, 7 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) / 𝑁)) ∈
ℝ) |
| 52 | | efle 16154 |
. . . . . . . . 9
⊢ (((1 /
(𝑁 + 1)) ∈ ℝ
∧ (log‘((𝑁 + 1) /
𝑁)) ∈ ℝ) →
((1 / (𝑁 + 1)) ≤
(log‘((𝑁 + 1) / 𝑁)) ↔ (exp‘(1 / (𝑁 + 1))) ≤
(exp‘(log‘((𝑁 +
1) / 𝑁))))) |
| 53 | 2, 51, 52 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((1 /
(𝑁 + 1)) ≤
(log‘((𝑁 + 1) / 𝑁)) ↔ (exp‘(1 / (𝑁 + 1))) ≤
(exp‘(log‘((𝑁 +
1) / 𝑁))))) |
| 54 | 49, 53 | mpbird 257 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 + 1)) ≤
(log‘((𝑁 + 1) / 𝑁))) |
| 55 | 54, 50 | breqtrd 5169 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 /
(𝑁 + 1)) ≤
((log‘(𝑁 + 1))
− (log‘𝑁))) |
| 56 | 2, 7, 12, 55 | leadd2dd 11878 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + (1 / (𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + ((log‘(𝑁 + 1)) − (log‘𝑁)))) |
| 57 | | id 22 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
| 58 | | nnuz 12921 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
| 59 | 57, 58 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) |
| 60 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1...(𝑁 + 1)) → 𝑚 ∈ ℕ) |
| 61 | 60 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ) |
| 62 | 61 | nnrecred 12317 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → (1 / 𝑚) ∈ ℝ) |
| 63 | 62 | recnd 11289 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑚 ∈ (1...(𝑁 + 1))) → (1 / 𝑚) ∈ ℂ) |
| 64 | | oveq2 7439 |
. . . . . 6
⊢ (𝑚 = (𝑁 + 1) → (1 / 𝑚) = (1 / (𝑁 + 1))) |
| 65 | 59, 63, 64 | fsump1 15792 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + (1 / (𝑁 + 1)))) |
| 66 | 4 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(𝑁 + 1)) ∈
ℂ) |
| 67 | 12 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) ∈ ℂ) |
| 68 | 6 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘𝑁) ∈
ℂ) |
| 69 | 66, 67, 68 | addsub12d 11643 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((log‘(𝑁 + 1)) +
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁))) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + ((log‘(𝑁 + 1)) − (log‘𝑁)))) |
| 70 | 56, 65, 69 | 3brtr4d 5175 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ≤ ((log‘(𝑁 + 1)) + (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)))) |
| 71 | | fzfid 14014 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 + 1)) ∈
Fin) |
| 72 | 71, 62 | fsumrecl 15770 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ∈ ℝ) |
| 73 | 12, 6 | resubcld 11691 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)) ∈ ℝ) |
| 74 | 72, 4, 73 | lesubadd2d 11862 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((Σ𝑚 ∈
(1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)) ↔ Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ≤ ((log‘(𝑁 + 1)) + (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁))))) |
| 75 | 70, 74 | mpbird 257 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈
(1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁))) |
| 76 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = (𝑁 + 1) → (1...𝑛) = (1...(𝑁 + 1))) |
| 77 | 76 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑛 = (𝑁 + 1) → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚)) |
| 78 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑁 + 1) → (log‘𝑛) = (log‘(𝑁 + 1))) |
| 79 | 77, 78 | oveq12d 7449 |
. . . . 5
⊢ (𝑛 = (𝑁 + 1) → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1)))) |
| 80 | | emcl.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛))) |
| 81 | | ovex 7464 |
. . . . 5
⊢
(Σ𝑚 ∈
(1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1))) ∈
V |
| 82 | 79, 80, 81 | fvmpt 7016 |
. . . 4
⊢ ((𝑁 + 1) ∈ ℕ →
(𝐹‘(𝑁 + 1)) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1)))) |
| 83 | 1, 82 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐹‘(𝑁 + 1)) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘(𝑁 + 1)))) |
| 84 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
| 85 | 84 | sumeq1d 15736 |
. . . . 5
⊢ (𝑛 = 𝑁 → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = Σ𝑚 ∈ (1...𝑁)(1 / 𝑚)) |
| 86 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑁 → (log‘𝑛) = (log‘𝑁)) |
| 87 | 85, 86 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = 𝑁 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁))) |
| 88 | | ovex 7464 |
. . . 4
⊢
(Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘𝑁)) ∈ V |
| 89 | 87, 80, 88 | fvmpt 7016 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁))) |
| 90 | 75, 83, 89 | 3brtr4d 5175 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁)) |
| 91 | | peano2nn 12278 |
. . . . . . . . . 10
⊢ ((𝑁 + 1) ∈ ℕ →
((𝑁 + 1) + 1) ∈
ℕ) |
| 92 | 1, 91 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) ∈
ℕ) |
| 93 | 92 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) ∈
ℝ+) |
| 94 | 93 | relogcld 26665 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) + 1))
∈ ℝ) |
| 95 | 94, 4 | resubcld 11691 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((log‘((𝑁 + 1) + 1))
− (log‘(𝑁 +
1))) ∈ ℝ) |
| 96 | | logdifbnd 27037 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℝ+
→ ((log‘((𝑁 + 1)
+ 1)) − (log‘(𝑁
+ 1))) ≤ (1 / (𝑁 +
1))) |
| 97 | 3, 96 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((log‘((𝑁 + 1) + 1))
− (log‘(𝑁 +
1))) ≤ (1 / (𝑁 +
1))) |
| 98 | 95, 2, 12, 97 | leadd2dd 11878 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + ((log‘((𝑁 + 1) + 1)) − (log‘(𝑁 + 1)))) ≤ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + (1 / (𝑁 + 1)))) |
| 99 | 94 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) + 1))
∈ ℂ) |
| 100 | 67, 66, 99 | subadd23d 11642 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) + (log‘((𝑁 + 1) + 1))) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) + ((log‘((𝑁 + 1) + 1)) − (log‘(𝑁 + 1))))) |
| 101 | 98, 100, 65 | 3brtr4d 5175 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) + (log‘((𝑁 + 1) + 1))) ≤ Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚)) |
| 102 | 12, 4 | resubcld 11691 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ℝ) |
| 103 | | leaddsub 11739 |
. . . . 5
⊢
(((Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ℝ ∧
(log‘((𝑁 + 1) + 1))
∈ ℝ ∧ Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ∈ ℝ) → (((Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) + (log‘((𝑁 + 1) + 1))) ≤ Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ↔ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1))))) |
| 104 | 102, 94, 72, 103 | syl3anc 1373 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(((Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) + (log‘((𝑁 + 1) + 1))) ≤ Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) ↔ (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1))))) |
| 105 | 101, 104 | mpbid 232 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ≤ (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1)))) |
| 106 | | fvoveq1 7454 |
. . . . 5
⊢ (𝑛 = 𝑁 → (log‘(𝑛 + 1)) = (log‘(𝑁 + 1))) |
| 107 | 85, 106 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = 𝑁 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1)))) |
| 108 | | emcl.2 |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) |
| 109 | | ovex 7464 |
. . . 4
⊢
(Σ𝑚 ∈
(1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈
V |
| 110 | 107, 108,
109 | fvmpt 7016 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐺‘𝑁) = (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1)))) |
| 111 | | fvoveq1 7454 |
. . . . . 6
⊢ (𝑛 = (𝑁 + 1) → (log‘(𝑛 + 1)) = (log‘((𝑁 + 1) + 1))) |
| 112 | 77, 111 | oveq12d 7449 |
. . . . 5
⊢ (𝑛 = (𝑁 + 1) → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1)))) |
| 113 | | ovex 7464 |
. . . . 5
⊢
(Σ𝑚 ∈
(1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1))) ∈
V |
| 114 | 112, 108,
113 | fvmpt 7016 |
. . . 4
⊢ ((𝑁 + 1) ∈ ℕ →
(𝐺‘(𝑁 + 1)) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1)))) |
| 115 | 1, 114 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝐺‘(𝑁 + 1)) = (Σ𝑚 ∈ (1...(𝑁 + 1))(1 / 𝑚) − (log‘((𝑁 + 1) + 1)))) |
| 116 | 105, 110,
115 | 3brtr4d 5175 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1))) |
| 117 | 90, 116 | jca 511 |
1
⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1)))) |