Metamath Proof Explorer

Theorem emcllem2

Description: Lemma for emcl . F is increasing, and G is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses emcl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
emcl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
Assertion emcllem2 ( 𝑁 ∈ ℕ → ( ( 𝐹 ‘ ( 𝑁 + 1 ) ) ≤ ( 𝐹 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 emcl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
2 emcl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
3 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
4 3 nnrecred ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 + 1 ) ) ∈ ℝ )
5 3 nnrpd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ+ )
6 5 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
7 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
8 7 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℝ )
9 6 8 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ∈ ℝ )
10 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
11 elfznn ⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → 𝑚 ∈ ℕ )
12 11 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑚 ∈ ℕ )
13 12 nnrecred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑚 ) ∈ ℝ )
14 10 13 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) ∈ ℝ )
15 5 rpreccld ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 + 1 ) ) ∈ ℝ+ )
16 15 rpge0d ⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 1 / ( 𝑁 + 1 ) ) )
17 1div1e1 ⊢ ( 1 / 1 ) = 1
18 1re ⊢ 1 ∈ ℝ
19 ltaddrp ⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → 1 < ( 1 + 𝑁 ) )
20 18 7 19 sylancr ⊢ ( 𝑁 ∈ ℕ → 1 < ( 1 + 𝑁 ) )
21 ax-1cn ⊢ 1 ∈ ℂ
22 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
23 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 1 + 𝑁 ) = ( 𝑁 + 1 ) )
24 21 22 23 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 1 + 𝑁 ) = ( 𝑁 + 1 ) )
25 20 24 breqtrd ⊢ ( 𝑁 ∈ ℕ → 1 < ( 𝑁 + 1 ) )
26 17 25 eqbrtrid ⊢ ( 𝑁 ∈ ℕ → ( 1 / 1 ) < ( 𝑁 + 1 ) )
27 3 nnred ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
28 3 nngt0d ⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
29 0lt1 ⊢ 0 < 1
30 ltrec1 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 < ( 𝑁 + 1 ) ) ) → ( ( 1 / 1 ) < ( 𝑁 + 1 ) ↔ ( 1 / ( 𝑁 + 1 ) ) < 1 ) )
31 18 29 30 mpanl12 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℝ ∧ 0 < ( 𝑁 + 1 ) ) → ( ( 1 / 1 ) < ( 𝑁 + 1 ) ↔ ( 1 / ( 𝑁 + 1 ) ) < 1 ) )
32 27 28 31 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / 1 ) < ( 𝑁 + 1 ) ↔ ( 1 / ( 𝑁 + 1 ) ) < 1 ) )
33 26 32 mpbid ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 + 1 ) ) < 1 )
34 4 16 33 eflegeo ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( 1 / ( 𝑁 + 1 ) ) ) ≤ ( 1 / ( 1 − ( 1 / ( 𝑁 + 1 ) ) ) ) )
35 27 recnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
36 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
37 3 nnne0d ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≠ 0 )
38 22 35 36 37 recdivd ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 / ( 𝑁 + 1 ) ) ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
39 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
40 35 39 35 37 divsubdird ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) − 1 ) / ( 𝑁 + 1 ) ) = ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) )
41 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
42 22 21 41 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
43 42 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) − 1 ) / ( 𝑁 + 1 ) ) = ( 𝑁 / ( 𝑁 + 1 ) ) )
44 35 37 dividd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) = 1 )
45 44 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / ( 𝑁 + 1 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) = ( 1 − ( 1 / ( 𝑁 + 1 ) ) ) )
46 40 43 45 3eqtr3rd ⊢ ( 𝑁 ∈ ℕ → ( 1 − ( 1 / ( 𝑁 + 1 ) ) ) = ( 𝑁 / ( 𝑁 + 1 ) ) )
47 46 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 1 − ( 1 / ( 𝑁 + 1 ) ) ) ) = ( 1 / ( 𝑁 / ( 𝑁 + 1 ) ) ) )
48 5 7 rpdivcld ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℝ+ )
49 48 reeflogd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
50 38 47 49 3eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 1 − ( 1 / ( 𝑁 + 1 ) ) ) ) = ( exp ‘ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
51 34 50 breqtrd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( 1 / ( 𝑁 + 1 ) ) ) ≤ ( exp ‘ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
52 5 7 relogdivd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
53 52 9 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℝ )
54 efle ⊢ ( ( ( 1 / ( 𝑁 + 1 ) ) ∈ ℝ ∧ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℝ ) → ( ( 1 / ( 𝑁 + 1 ) ) ≤ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ↔ ( exp ‘ ( 1 / ( 𝑁 + 1 ) ) ) ≤ ( exp ‘ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ) )
55 4 53 54 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( 1 / ( 𝑁 + 1 ) ) ≤ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ↔ ( exp ‘ ( 1 / ( 𝑁 + 1 ) ) ) ≤ ( exp ‘ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ) )
56 51 55 mpbird ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 + 1 ) ) ≤ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
57 56 52 breqtrd ⊢ ( 𝑁 ∈ ℕ → ( 1 / ( 𝑁 + 1 ) ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
58 4 9 14 57 leadd2dd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( 1 / ( 𝑁 + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ) )
59 id ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
60 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
61 59 60 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
62 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑚 ∈ ℕ )
63 62 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ℕ )
64 63 nnrecred ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
65 64 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
66 oveq2 ⊢ ( 𝑚 = ( 𝑁 + 1 ) → ( 1 / 𝑚 ) = ( 1 / ( 𝑁 + 1 ) ) )
67 61 65 66 fsump1 ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( 1 / ( 𝑁 + 1 ) ) ) )
68 6 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
69 14 recnd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) ∈ ℂ )
70 8 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℂ )
71 68 69 70 addsub12d ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( 𝑁 + 1 ) ) + ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ) )
72 58 67 71 3brtr4d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) + ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ) )
73 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
74 73 64 fsumrecl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) ∈ ℝ )
75 14 8 resubcld ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ∈ ℝ )
76 74 6 75 lesubadd2d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ↔ Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) + ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ) ) )
77 72 76 mpbird ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) )
78 oveq2 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 1 ... 𝑛 ) = ( 1 ... ( 𝑁 + 1 ) ) )
79 78 sumeq1d ⊢ ( 𝑛 = ( 𝑁 + 1 ) → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) )
80 fveq2 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( log ‘ 𝑛 ) = ( log ‘ ( 𝑁 + 1 ) ) )
81 79 80 oveq12d ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
82 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ V
83 81 1 82 fvmpt ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
84 3 83 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
85 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
86 85 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) )
87 fveq2 ⊢ ( 𝑛 = 𝑁 → ( log ‘ 𝑛 ) = ( log ‘ 𝑁 ) )
88 86 87 oveq12d ⊢ ( 𝑛 = 𝑁 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) )
89 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) ∈ V
90 88 1 89 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ 𝑁 ) ) )
91 77 84 90 3brtr4d ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ ( 𝑁 + 1 ) ) ≤ ( 𝐹 ‘ 𝑁 ) )
92 peano2nn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ )
93 3 92 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) ∈ ℕ )
94 93 nnrpd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) + 1 ) ∈ ℝ+ )
95 94 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ∈ ℝ )
96 95 6 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
97 logdifbnd ⊢ ( ( 𝑁 + 1 ) ∈ ℝ+ → ( ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( 1 / ( 𝑁 + 1 ) ) )
98 5 97 syl ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( 1 / ( 𝑁 + 1 ) ) )
99 96 4 14 98 leadd2dd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) − ( log ‘ ( 𝑁 + 1 ) ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( 1 / ( 𝑁 + 1 ) ) ) )
100 95 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ∈ ℂ )
101 69 68 100 subadd23d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) + ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) + ( ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) − ( log ‘ ( 𝑁 + 1 ) ) ) ) )
102 99 101 67 3brtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) + ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) )
103 14 6 resubcld ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
104 leaddsub ⊢ ( ( ( Σ 𝑚 ∈ ( 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 ) ) ) ) )
105 103 95 74 104 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) + ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) ↔ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) ) )
106 102 105 mpbid ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
107 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝑛 + 1 ) ) = ( log ‘ ( 𝑁 + 1 ) ) )
108 86 107 oveq12d ⊢ ( 𝑛 = 𝑁 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
109 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ V
110 108 2 109 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 ‘ 𝑁 ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
111 fvoveq1 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( log ‘ ( 𝑛 + 1 ) ) = ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) )
112 79 111 oveq12d ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
113 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) ∈ V
114 112 2 113 fvmpt ⊢ ( ( 𝑁 + 1 ) ∈ ℕ → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
115 3 114 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( 𝑁 + 1 ) + 1 ) ) ) )
116 106 110 115 3brtr4d ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 ‘ 𝑁 ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
117 91 116 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 ‘ ( 𝑁 + 1 ) ) ≤ ( 𝐹 ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑁 ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )