Metamath Proof Explorer

Theorem emcllem7

Description: Lemma for emcl and harmonicbnd . Derive bounds on gamma as F ( 1 ) and G ( 1 ) . (Contributed by Mario Carneiro, 11-Jul-2014) (Revised by Mario Carneiro, 9-Apr-2016)

Ref Expression
Hypotheses emcl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
emcl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
emcl.3 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
emcl.4 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
Assertion emcllem7 ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ∧ 𝐹 : ℕ ⟶ ( γ [,] 1 ) ∧ 𝐺 : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )

Proof

Step Hyp Ref Expression
1 emcl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
2 emcl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
3 emcl.3 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
4 emcl.4 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
7 1 2 3 4 emcllem6 ⊢ ( 𝐹 ⇝ γ ∧ 𝐺 ⇝ γ )
8 7 simpri ⊢ 𝐺 ⇝ γ
9 8 a1i ⊢ ( ⊤ → 𝐺 ⇝ γ )
10 1 2 emcllem1 ⊢ ( 𝐹 : ℕ ⟶ ℝ ∧ 𝐺 : ℕ ⟶ ℝ )
11 10 simpri ⊢ 𝐺 : ℕ ⟶ ℝ
12 11 ffvelcdmi ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
13 12 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
14 5 6 9 13 climrecl ⊢ ( ⊤ → γ ∈ ℝ )
15 1nn ⊢ 1 ∈ ℕ
16 simpr ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
17 8 a1i ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → 𝐺 ⇝ γ )
18 12 adantl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
19 1 2 emcllem2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
20 19 simprd ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
21 20 adantl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
22 5 16 17 18 21 climub ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ 𝑖 ) ≤ γ )
23 22 ralrimiva ⊢ ( ⊤ → ∀ 𝑖 ∈ ℕ ( 𝐺 ‘ 𝑖 ) ≤ γ )
24 fveq2 ⊢ ( 𝑖 = 1 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 1 ) )
25 oveq2 ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = ( 1 ... 1 ) )
26 25 sumeq1d ⊢ ( 𝑛 = 1 → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... 1 ) ( 1 / 𝑚 ) )
27 1z ⊢ 1 ∈ ℤ
28 ax-1cn ⊢ 1 ∈ ℂ
29 oveq2 ⊢ ( 𝑚 = 1 → ( 1 / 𝑚 ) = ( 1 / 1 ) )
30 1div1e1 ⊢ ( 1 / 1 ) = 1
31 29 30 eqtrdi ⊢ ( 𝑚 = 1 → ( 1 / 𝑚 ) = 1 )
32 31 fsum1 ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℂ ) → Σ 𝑚 ∈ ( 1 ... 1 ) ( 1 / 𝑚 ) = 1 )
33 27 28 32 mp2an ⊢ Σ 𝑚 ∈ ( 1 ... 1 ) ( 1 / 𝑚 ) = 1
34 26 33 eqtrdi ⊢ ( 𝑛 = 1 → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = 1 )
35 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = ( 1 + 1 ) )
36 df-2 ⊢ 2 = ( 1 + 1 )
37 35 36 eqtr4di ⊢ ( 𝑛 = 1 → ( 𝑛 + 1 ) = 2 )
38 37 fveq2d ⊢ ( 𝑛 = 1 → ( log ‘ ( 𝑛 + 1 ) ) = ( log ‘ 2 ) )
39 34 38 oveq12d ⊢ ( 𝑛 = 1 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) = ( 1 − ( log ‘ 2 ) ) )
40 1re ⊢ 1 ∈ ℝ
41 2rp ⊢ 2 ∈ ℝ+
42 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
43 41 42 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
44 40 43 resubcli ⊢ ( 1 − ( log ‘ 2 ) ) ∈ ℝ
45 44 elexi ⊢ ( 1 − ( log ‘ 2 ) ) ∈ V
46 39 2 45 fvmpt ⊢ ( 1 ∈ ℕ → ( 𝐺 ‘ 1 ) = ( 1 − ( log ‘ 2 ) ) )
47 15 46 ax-mp ⊢ ( 𝐺 ‘ 1 ) = ( 1 − ( log ‘ 2 ) )
48 24 47 eqtrdi ⊢ ( 𝑖 = 1 → ( 𝐺 ‘ 𝑖 ) = ( 1 − ( log ‘ 2 ) ) )
49 48 breq1d ⊢ ( 𝑖 = 1 → ( ( 𝐺 ‘ 𝑖 ) ≤ γ ↔ ( 1 − ( log ‘ 2 ) ) ≤ γ ) )
50 49 rspcva ⊢ ( ( 1 ∈ ℕ ∧ ∀ 𝑖 ∈ ℕ ( 𝐺 ‘ 𝑖 ) ≤ γ ) → ( 1 − ( log ‘ 2 ) ) ≤ γ )
51 15 23 50 sylancr ⊢ ( ⊤ → ( 1 − ( log ‘ 2 ) ) ≤ γ )
52 fveq2 ⊢ ( 𝑥 = 𝑖 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑖 ) )
53 52 negeqd ⊢ ( 𝑥 = 𝑖 → - ( 𝐹 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑖 ) )
54 eqid ⊢ ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) )
55 negex ⊢ - ( 𝐹 ‘ 𝑖 ) ∈ V
56 53 54 55 fvmpt ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑖 ) = - ( 𝐹 ‘ 𝑖 ) )
57 56 adantl ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑖 ) = - ( 𝐹 ‘ 𝑖 ) )
58 7 simpli ⊢ 𝐹 ⇝ γ
59 58 a1i ⊢ ( ⊤ → 𝐹 ⇝ γ )
60 0cnd ⊢ ( ⊤ → 0 ∈ ℂ )
61 nnex ⊢ ℕ ∈ V
62 61 mptex ⊢ ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ∈ V
63 62 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ∈ V )
64 10 simpli ⊢ 𝐹 : ℕ ⟶ ℝ
65 64 ffvelcdmi ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
66 65 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
67 66 recnd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
68 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
69 68 negeqd ⊢ ( 𝑥 = 𝑘 → - ( 𝐹 ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑘 ) )
70 negex ⊢ - ( 𝐹 ‘ 𝑘 ) ∈ V
71 69 54 70 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
72 71 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) = - ( 𝐹 ‘ 𝑘 ) )
73 df-neg ⊢ - ( 𝐹 ‘ 𝑘 ) = ( 0 − ( 𝐹 ‘ 𝑘 ) )
74 72 73 eqtrdi ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) = ( 0 − ( 𝐹 ‘ 𝑘 ) ) )
75 5 6 59 60 63 67 74 climsubc2 ⊢ ( ⊤ → ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ⇝ ( 0 − γ ) )
76 75 adantr ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ⇝ ( 0 − γ ) )
77 66 renegcld ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → - ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
78 72 77 eqeltrd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℝ )
79 78 adantlr ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) ∈ ℝ )
80 19 simpld ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
81 80 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
82 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
83 82 adantl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
84 64 ffvelcdmi ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
85 83 84 syl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
86 85 66 lenegd ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ - ( 𝐹 ‘ 𝑘 ) ≤ - ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
87 81 86 mpbid ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → - ( 𝐹 ‘ 𝑘 ) ≤ - ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
88 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
89 88 negeqd ⊢ ( 𝑥 = ( 𝑘 + 1 ) → - ( 𝐹 ‘ 𝑥 ) = - ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
90 negex ⊢ - ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ V
91 89 54 90 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ ( 𝑘 + 1 ) ) = - ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
92 83 91 syl ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ ( 𝑘 + 1 ) ) = - ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
93 87 72 92 3brtr4d ⊢ ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) ≤ ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ ( 𝑘 + 1 ) ) )
94 93 adantlr ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑘 ) ≤ ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ ( 𝑘 + 1 ) ) )
95 5 16 76 79 94 climub ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ - ( 𝐹 ‘ 𝑥 ) ) ‘ 𝑖 ) ≤ ( 0 − γ ) )
96 57 95 eqbrtrrd ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → - ( 𝐹 ‘ 𝑖 ) ≤ ( 0 − γ ) )
97 df-neg ⊢ - γ = ( 0 − γ )
98 96 97 breqtrrdi ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → - ( 𝐹 ‘ 𝑖 ) ≤ - γ )
99 14 mptru ⊢ γ ∈ ℝ
100 64 ffvelcdmi ⊢ ( 𝑖 ∈ ℕ → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
101 100 adantl ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
102 leneg ⊢ ( ( γ ∈ ℝ ∧ ( 𝐹 ‘ 𝑖 ) ∈ ℝ ) → ( γ ≤ ( 𝐹 ‘ 𝑖 ) ↔ - ( 𝐹 ‘ 𝑖 ) ≤ - γ ) )
103 99 101 102 sylancr ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( γ ≤ ( 𝐹 ‘ 𝑖 ) ↔ - ( 𝐹 ‘ 𝑖 ) ≤ - γ ) )
104 98 103 mpbird ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → γ ≤ ( 𝐹 ‘ 𝑖 ) )
105 104 ralrimiva ⊢ ( ⊤ → ∀ 𝑖 ∈ ℕ γ ≤ ( 𝐹 ‘ 𝑖 ) )
106 fveq2 ⊢ ( 𝑖 = 1 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 1 ) )
107 fveq2 ⊢ ( 𝑛 = 1 → ( log ‘ 𝑛 ) = ( log ‘ 1 ) )
108 log1 ⊢ ( log ‘ 1 ) = 0
109 107 108 eqtrdi ⊢ ( 𝑛 = 1 → ( log ‘ 𝑛 ) = 0 )
110 34 109 oveq12d ⊢ ( 𝑛 = 1 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) = ( 1 − 0 ) )
111 1m0e1 ⊢ ( 1 − 0 ) = 1
112 110 111 eqtrdi ⊢ ( 𝑛 = 1 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) = 1 )
113 40 elexi ⊢ 1 ∈ V
114 112 1 113 fvmpt ⊢ ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) = 1 )
115 15 114 ax-mp ⊢ ( 𝐹 ‘ 1 ) = 1
116 106 115 eqtrdi ⊢ ( 𝑖 = 1 → ( 𝐹 ‘ 𝑖 ) = 1 )
117 116 breq2d ⊢ ( 𝑖 = 1 → ( γ ≤ ( 𝐹 ‘ 𝑖 ) ↔ γ ≤ 1 ) )
118 117 rspcva ⊢ ( ( 1 ∈ ℕ ∧ ∀ 𝑖 ∈ ℕ γ ≤ ( 𝐹 ‘ 𝑖 ) ) → γ ≤ 1 )
119 15 105 118 sylancr ⊢ ( ⊤ → γ ≤ 1 )
120 44 40 elicc2i ⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ↔ ( γ ∈ ℝ ∧ ( 1 − ( log ‘ 2 ) ) ≤ γ ∧ γ ≤ 1 ) )
121 14 51 119 120 syl3anbrc ⊢ ( ⊤ → γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) )
122 ffn ⊢ ( 𝐹 : ℕ ⟶ ℝ → 𝐹 Fn ℕ )
123 64 122 mp1i ⊢ ( ⊤ → 𝐹 Fn ℕ )
124 16 5 eleqtrdi ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ( ℤ≥ ‘ 1 ) )
125 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑖 ) → 𝑘 ∈ ℕ )
126 125 adantl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑖 ) ) → 𝑘 ∈ ℕ )
127 126 65 syl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
128 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑖 − 1 ) ) → 𝑘 ∈ ℕ )
129 128 adantl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑖 − 1 ) ) ) → 𝑘 ∈ ℕ )
130 129 80 syl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑖 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
131 124 127 130 monoord2 ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐹 ‘ 1 ) )
132 131 115 breqtrdi ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ≤ 1 )
133 99 40 elicc2i ⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ ( γ [,] 1 ) ↔ ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ ∧ γ ≤ ( 𝐹 ‘ 𝑖 ) ∧ ( 𝐹 ‘ 𝑖 ) ≤ 1 ) )
134 101 104 132 133 syl3anbrc ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ∈ ( γ [,] 1 ) )
135 134 ralrimiva ⊢ ( ⊤ → ∀ 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) ∈ ( γ [,] 1 ) )
136 ffnfv ⊢ ( 𝐹 : ℕ ⟶ ( γ [,] 1 ) ↔ ( 𝐹 Fn ℕ ∧ ∀ 𝑖 ∈ ℕ ( 𝐹 ‘ 𝑖 ) ∈ ( γ [,] 1 ) ) )
137 123 135 136 sylanbrc ⊢ ( ⊤ → 𝐹 : ℕ ⟶ ( γ [,] 1 ) )
138 ffn ⊢ ( 𝐺 : ℕ ⟶ ℝ → 𝐺 Fn ℕ )
139 11 138 mp1i ⊢ ( ⊤ → 𝐺 Fn ℕ )
140 11 ffvelcdmi ⊢ ( 𝑖 ∈ ℕ → ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
141 140 adantl ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
142 126 12 syl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑖 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
143 129 20 syl ⊢ ( ( ( ⊤ ∧ 𝑖 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑖 − 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
144 124 142 143 monoord ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ 𝑖 ) )
145 47 144 eqbrtrrid ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 1 − ( log ‘ 2 ) ) ≤ ( 𝐺 ‘ 𝑖 ) )
146 44 99 elicc2i ⊢ ( ( 𝐺 ‘ 𝑖 ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ↔ ( ( 𝐺 ‘ 𝑖 ) ∈ ℝ ∧ ( 1 − ( log ‘ 2 ) ) ≤ ( 𝐺 ‘ 𝑖 ) ∧ ( 𝐺 ‘ 𝑖 ) ≤ γ ) )
147 141 145 22 146 syl3anbrc ⊢ ( ( ⊤ ∧ 𝑖 ∈ ℕ ) → ( 𝐺 ‘ 𝑖 ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
148 147 ralrimiva ⊢ ( ⊤ → ∀ 𝑖 ∈ ℕ ( 𝐺 ‘ 𝑖 ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
149 ffnfv ⊢ ( 𝐺 : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ↔ ( 𝐺 Fn ℕ ∧ ∀ 𝑖 ∈ ℕ ( 𝐺 ‘ 𝑖 ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ) )
150 139 148 149 sylanbrc ⊢ ( ⊤ → 𝐺 : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
151 121 137 150 3jca ⊢ ( ⊤ → ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ∧ 𝐹 : ℕ ⟶ ( γ [,] 1 ) ∧ 𝐺 : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ) )
152 151 mptru ⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ∧ 𝐹 : ℕ ⟶ ( γ [,] 1 ) ∧ 𝐺 : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )