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 ) ) ) )