Metamath Proof Explorer

Theorem lgamgulmlem5

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r ⊢φ→R∈ℕ
lgamgulm.u ⊢U=x∈ℂ|x≤R∧∀k∈ℕ01R≤x+k
lgamgulm.g ⊢G=m∈ℕ⟼z∈U⟼z⁢log⁡m+1m−log⁡zm+1
lgamgulm.t ⊢T=m∈ℕ⟼if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π
Assertion lgamgulmlem5 ⊢φ∧n∈ℕ∧y∈U→G⁡n⁡y≤T⁡n

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢φ→R∈ℕ
2 lgamgulm.u ⊢U=x∈ℂ|x≤R∧∀k∈ℕ01R≤x+k
3 lgamgulm.g ⊢G=m∈ℕ⟼z∈U⟼z⁢log⁡m+1m−log⁡zm+1
4 lgamgulm.t ⊢T=m∈ℕ⟼if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π
5 breq2 ⊢R⁢2⁢R+1n2=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π→y⁢log⁡n+1n−log⁡yn+1≤R⁢2⁢R+1n2↔y⁢log⁡n+1n−log⁡yn+1≤if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
6 breq2 ⊢R⁢log⁡n+1n+log⁡R+1⁢n+π=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π→y⁢log⁡n+1n−log⁡yn+1≤R⁢log⁡n+1n+log⁡R+1⁢n+π↔y⁢log⁡n+1n−log⁡yn+1≤if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
7 1 adantr ⊢φ∧n∈ℕ∧y∈U→R∈ℕ
8 7 adantr ⊢φ∧n∈ℕ∧y∈U∧2⁢R≤n→R∈ℕ
9 fveq2 ⊢x=t→x=t
10 9 breq1d ⊢x=t→x≤R↔t≤R
11 fvoveq1 ⊢x=t→x+k=t+k
12 11 breq2d ⊢x=t→1R≤x+k↔1R≤t+k
13 12 ralbidv ⊢x=t→∀k∈ℕ01R≤x+k↔∀k∈ℕ01R≤t+k
14 10 13 anbi12d ⊢x=t→x≤R∧∀k∈ℕ01R≤x+k↔t≤R∧∀k∈ℕ01R≤t+k
15 14 cbvrabv ⊢x∈ℂ|x≤R∧∀k∈ℕ01R≤x+k=t∈ℂ|t≤R∧∀k∈ℕ01R≤t+k
16 2 15 eqtri ⊢U=t∈ℂ|t≤R∧∀k∈ℕ01R≤t+k
17 simplrl ⊢φ∧n∈ℕ∧y∈U∧2⁢R≤n→n∈ℕ
18 simprr ⊢φ∧n∈ℕ∧y∈U→y∈U
19 18 adantr ⊢φ∧n∈ℕ∧y∈U∧2⁢R≤n→y∈U
20 simpr ⊢φ∧n∈ℕ∧y∈U∧2⁢R≤n→2⁢R≤n
21 8 16 17 19 20 lgamgulmlem3 ⊢φ∧n∈ℕ∧y∈U∧2⁢R≤n→y⁢log⁡n+1n−log⁡yn+1≤R⁢2⁢R+1n2
22 1 2 lgamgulmlem1 ⊢φ→U⊆ℂ∖ℤ∖ℕ
23 22 adantr ⊢φ∧n∈ℕ∧y∈U→U⊆ℂ∖ℤ∖ℕ
24 23 18 sseldd ⊢φ∧n∈ℕ∧y∈U→y∈ℂ∖ℤ∖ℕ
25 24 eldifad ⊢φ∧n∈ℕ∧y∈U→y∈ℂ
26 simprl ⊢φ∧n∈ℕ∧y∈U→n∈ℕ
27 26 peano2nnd ⊢φ∧n∈ℕ∧y∈U→n+1∈ℕ
28 27 nnrpd ⊢φ∧n∈ℕ∧y∈U→n+1∈ℝ+
29 26 nnrpd ⊢φ∧n∈ℕ∧y∈U→n∈ℝ+
30 28 29 rpdivcld ⊢φ∧n∈ℕ∧y∈U→n+1n∈ℝ+
31 30 relogcld ⊢φ∧n∈ℕ∧y∈U→log⁡n+1n∈ℝ
32 31 recnd ⊢φ∧n∈ℕ∧y∈U→log⁡n+1n∈ℂ
33 25 32 mulcld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n∈ℂ
34 26 nncnd ⊢φ∧n∈ℕ∧y∈U→n∈ℂ
35 26 nnne0d ⊢φ∧n∈ℕ∧y∈U→n≠0
36 25 34 35 divcld ⊢φ∧n∈ℕ∧y∈U→yn∈ℂ
37 1cnd ⊢φ∧n∈ℕ∧y∈U→1∈ℂ
38 36 37 addcld ⊢φ∧n∈ℕ∧y∈U→yn+1∈ℂ
39 24 26 dmgmdivn0 ⊢φ∧n∈ℕ∧y∈U→yn+1≠0
40 38 39 logcld ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1∈ℂ
41 33 40 subcld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n−log⁡yn+1∈ℂ
42 41 abscld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n−log⁡yn+1∈ℝ
43 33 abscld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n∈ℝ
44 40 abscld ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1∈ℝ
45 43 44 readdcld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n+log⁡yn+1∈ℝ
46 7 nnred ⊢φ∧n∈ℕ∧y∈U→R∈ℝ
47 46 31 remulcld ⊢φ∧n∈ℕ∧y∈U→R⁢log⁡n+1n∈ℝ
48 7 peano2nnd ⊢φ∧n∈ℕ∧y∈U→R+1∈ℕ
49 48 nnrpd ⊢φ∧n∈ℕ∧y∈U→R+1∈ℝ+
50 49 29 rpmulcld ⊢φ∧n∈ℕ∧y∈U→R+1⁢n∈ℝ+
51 50 relogcld ⊢φ∧n∈ℕ∧y∈U→log⁡R+1⁢n∈ℝ
52 pire ⊢π∈ℝ
53 52 a1i ⊢φ∧n∈ℕ∧y∈U→π∈ℝ
54 51 53 readdcld ⊢φ∧n∈ℕ∧y∈U→log⁡R+1⁢n+π∈ℝ
55 47 54 readdcld ⊢φ∧n∈ℕ∧y∈U→R⁢log⁡n+1n+log⁡R+1⁢n+π∈ℝ
56 33 40 abs2dif2d ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n−log⁡yn+1≤y⁢log⁡n+1n+log⁡yn+1
57 25 32 absmuld ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n=y⁢log⁡n+1n
58 30 rpred ⊢φ∧n∈ℕ∧y∈U→n+1n∈ℝ
59 34 mullidd ⊢φ∧n∈ℕ∧y∈U→1⁢n=n
60 26 nnred ⊢φ∧n∈ℕ∧y∈U→n∈ℝ
61 60 lep1d ⊢φ∧n∈ℕ∧y∈U→n≤n+1
62 59 61 eqbrtrd ⊢φ∧n∈ℕ∧y∈U→1⁢n≤n+1
63 1red ⊢φ∧n∈ℕ∧y∈U→1∈ℝ
64 60 63 readdcld ⊢φ∧n∈ℕ∧y∈U→n+1∈ℝ
65 63 64 29 lemuldivd ⊢φ∧n∈ℕ∧y∈U→1⁢n≤n+1↔1≤n+1n
66 62 65 mpbid ⊢φ∧n∈ℕ∧y∈U→1≤n+1n
67 58 66 logge0d ⊢φ∧n∈ℕ∧y∈U→0≤log⁡n+1n
68 31 67 absidd ⊢φ∧n∈ℕ∧y∈U→log⁡n+1n=log⁡n+1n
69 68 oveq2d ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n=y⁢log⁡n+1n
70 57 69 eqtrd ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n=y⁢log⁡n+1n
71 25 abscld ⊢φ∧n∈ℕ∧y∈U→y∈ℝ
72 fveq2 ⊢x=y→x=y
73 72 breq1d ⊢x=y→x≤R↔y≤R
74 fvoveq1 ⊢x=y→x+k=y+k
75 74 breq2d ⊢x=y→1R≤x+k↔1R≤y+k
76 75 ralbidv ⊢x=y→∀k∈ℕ01R≤x+k↔∀k∈ℕ01R≤y+k
77 73 76 anbi12d ⊢x=y→x≤R∧∀k∈ℕ01R≤x+k↔y≤R∧∀k∈ℕ01R≤y+k
78 77 2 elrab2 ⊢y∈U↔y∈ℂ∧y≤R∧∀k∈ℕ01R≤y+k
79 78 simprbi ⊢y∈U→y≤R∧∀k∈ℕ01R≤y+k
80 79 ad2antll ⊢φ∧n∈ℕ∧y∈U→y≤R∧∀k∈ℕ01R≤y+k
81 80 simpld ⊢φ∧n∈ℕ∧y∈U→y≤R
82 71 46 31 67 81 lemul1ad ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n≤R⁢log⁡n+1n
83 70 82 eqbrtrd ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n≤R⁢log⁡n+1n
84 38 39 absrpcld ⊢φ∧n∈ℕ∧y∈U→yn+1∈ℝ+
85 84 relogcld ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1∈ℝ
86 85 recnd ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1∈ℂ
87 86 abscld ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1∈ℝ
88 87 53 readdcld ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1+π∈ℝ
89 abslogle ⊢yn+1∈ℂ∧yn+1≠0→log⁡yn+1≤log⁡yn+1+π
90 38 39 89 syl2anc ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1≤log⁡yn+1+π
91 1rp ⊢1∈ℝ+
92 relogdiv ⊢1∈ℝ+∧R+1⁢n∈ℝ+→log⁡1R+1⁢n=log⁡1−log⁡R+1⁢n
93 91 50 92 sylancr ⊢φ∧n∈ℕ∧y∈U→log⁡1R+1⁢n=log⁡1−log⁡R+1⁢n
94 log1 ⊢log⁡1=0
95 94 oveq1i ⊢log⁡1−log⁡R+1⁢n=0−log⁡R+1⁢n
96 df-neg ⊢−log⁡R+1⁢n=0−log⁡R+1⁢n
97 95 96 eqtr4i ⊢log⁡1−log⁡R+1⁢n=−log⁡R+1⁢n
98 93 97 eqtr2di ⊢φ∧n∈ℕ∧y∈U→−log⁡R+1⁢n=log⁡1R+1⁢n
99 48 nnrecred ⊢φ∧n∈ℕ∧y∈U→1R+1∈ℝ
100 25 34 addcld ⊢φ∧n∈ℕ∧y∈U→y+n∈ℂ
101 100 abscld ⊢φ∧n∈ℕ∧y∈U→y+n∈ℝ
102 7 nnrecred ⊢φ∧n∈ℕ∧y∈U→1R∈ℝ
103 7 nnrpd ⊢φ∧n∈ℕ∧y∈U→R∈ℝ+
104 0le1 ⊢0≤1
105 104 a1i ⊢φ∧n∈ℕ∧y∈U→0≤1
106 46 lep1d ⊢φ∧n∈ℕ∧y∈U→R≤R+1
107 103 49 63 105 106 lediv2ad ⊢φ∧n∈ℕ∧y∈U→1R+1≤1R
108 oveq2 ⊢k=n→y+k=y+n
109 108 fveq2d ⊢k=n→y+k=y+n
110 109 breq2d ⊢k=n→1R≤y+k↔1R≤y+n
111 80 simprd ⊢φ∧n∈ℕ∧y∈U→∀k∈ℕ01R≤y+k
112 26 nnnn0d ⊢φ∧n∈ℕ∧y∈U→n∈ℕ0
113 110 111 112 rspcdva ⊢φ∧n∈ℕ∧y∈U→1R≤y+n
114 99 102 101 107 113 letrd ⊢φ∧n∈ℕ∧y∈U→1R+1≤y+n
115 99 101 29 114 lediv1dd ⊢φ∧n∈ℕ∧y∈U→1R+1n≤y+nn
116 48 nncnd ⊢φ∧n∈ℕ∧y∈U→R+1∈ℂ
117 48 nnne0d ⊢φ∧n∈ℕ∧y∈U→R+1≠0
118 116 34 117 35 recdiv2d ⊢φ∧n∈ℕ∧y∈U→1R+1n=1R+1⁢n
119 25 34 34 35 divdird ⊢φ∧n∈ℕ∧y∈U→y+nn=yn+nn
120 34 35 dividd ⊢φ∧n∈ℕ∧y∈U→nn=1
121 120 oveq2d ⊢φ∧n∈ℕ∧y∈U→yn+nn=yn+1
122 119 121 eqtr2d ⊢φ∧n∈ℕ∧y∈U→yn+1=y+nn
123 122 fveq2d ⊢φ∧n∈ℕ∧y∈U→yn+1=y+nn
124 100 34 35 absdivd ⊢φ∧n∈ℕ∧y∈U→y+nn=y+nn
125 29 rpge0d ⊢φ∧n∈ℕ∧y∈U→0≤n
126 60 125 absidd ⊢φ∧n∈ℕ∧y∈U→n=n
127 126 oveq2d ⊢φ∧n∈ℕ∧y∈U→y+nn=y+nn
128 123 124 127 3eqtrrd ⊢φ∧n∈ℕ∧y∈U→y+nn=yn+1
129 115 118 128 3brtr3d ⊢φ∧n∈ℕ∧y∈U→1R+1⁢n≤yn+1
130 50 rpreccld ⊢φ∧n∈ℕ∧y∈U→1R+1⁢n∈ℝ+
131 130 84 logled ⊢φ∧n∈ℕ∧y∈U→1R+1⁢n≤yn+1↔log⁡1R+1⁢n≤log⁡yn+1
132 129 131 mpbid ⊢φ∧n∈ℕ∧y∈U→log⁡1R+1⁢n≤log⁡yn+1
133 98 132 eqbrtrd ⊢φ∧n∈ℕ∧y∈U→−log⁡R+1⁢n≤log⁡yn+1
134 38 abscld ⊢φ∧n∈ℕ∧y∈U→yn+1∈ℝ
135 46 63 readdcld ⊢φ∧n∈ℕ∧y∈U→R+1∈ℝ
136 50 rpred ⊢φ∧n∈ℕ∧y∈U→R+1⁢n∈ℝ
137 36 abscld ⊢φ∧n∈ℕ∧y∈U→yn∈ℝ
138 137 63 readdcld ⊢φ∧n∈ℕ∧y∈U→yn+1∈ℝ
139 36 37 abstrid ⊢φ∧n∈ℕ∧y∈U→yn+1≤yn+1
140 abs1 ⊢1=1
141 140 oveq2i ⊢yn+1=yn+1
142 139 141 breqtrdi ⊢φ∧n∈ℕ∧y∈U→yn+1≤yn+1
143 91 a1i ⊢φ∧n∈ℕ∧y∈U→1∈ℝ+
144 25 absge0d ⊢φ∧n∈ℕ∧y∈U→0≤y
145 26 nnge1d ⊢φ∧n∈ℕ∧y∈U→1≤n
146 71 46 143 60 144 81 145 lediv12ad ⊢φ∧n∈ℕ∧y∈U→yn≤R1
147 25 34 35 absdivd ⊢φ∧n∈ℕ∧y∈U→yn=yn
148 126 oveq2d ⊢φ∧n∈ℕ∧y∈U→yn=yn
149 147 148 eqtr2d ⊢φ∧n∈ℕ∧y∈U→yn=yn
150 7 nncnd ⊢φ∧n∈ℕ∧y∈U→R∈ℂ
151 150 div1d ⊢φ∧n∈ℕ∧y∈U→R1=R
152 146 149 151 3brtr3d ⊢φ∧n∈ℕ∧y∈U→yn≤R
153 137 46 63 152 leadd1dd ⊢φ∧n∈ℕ∧y∈U→yn+1≤R+1
154 134 138 135 142 153 letrd ⊢φ∧n∈ℕ∧y∈U→yn+1≤R+1
155 49 rpge0d ⊢φ∧n∈ℕ∧y∈U→0≤R+1
156 135 60 155 145 lemulge11d ⊢φ∧n∈ℕ∧y∈U→R+1≤R+1⁢n
157 134 135 136 154 156 letrd ⊢φ∧n∈ℕ∧y∈U→yn+1≤R+1⁢n
158 84 50 logled ⊢φ∧n∈ℕ∧y∈U→yn+1≤R+1⁢n↔log⁡yn+1≤log⁡R+1⁢n
159 157 158 mpbid ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1≤log⁡R+1⁢n
160 85 51 absled ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1≤log⁡R+1⁢n↔−log⁡R+1⁢n≤log⁡yn+1∧log⁡yn+1≤log⁡R+1⁢n
161 133 159 160 mpbir2and ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1≤log⁡R+1⁢n
162 87 51 53 161 leadd1dd ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1+π≤log⁡R+1⁢n+π
163 44 88 54 90 162 letrd ⊢φ∧n∈ℕ∧y∈U→log⁡yn+1≤log⁡R+1⁢n+π
164 43 44 47 54 83 163 le2addd ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n+log⁡yn+1≤R⁢log⁡n+1n+log⁡R+1⁢n+π
165 42 45 55 56 164 letrd ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n−log⁡yn+1≤R⁢log⁡n+1n+log⁡R+1⁢n+π
166 165 adantr ⊢φ∧n∈ℕ∧y∈U∧¬2⁢R≤n→y⁢log⁡n+1n−log⁡yn+1≤R⁢log⁡n+1n+log⁡R+1⁢n+π
167 5 6 21 166 ifbothda ⊢φ∧n∈ℕ∧y∈U→y⁢log⁡n+1n−log⁡yn+1≤if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
168 oveq1 ⊢m=n→m+1=n+1
169 id ⊢m=n→m=n
170 168 169 oveq12d ⊢m=n→m+1m=n+1n
171 170 fveq2d ⊢m=n→log⁡m+1m=log⁡n+1n
172 171 oveq2d ⊢m=n→z⁢log⁡m+1m=z⁢log⁡n+1n
173 oveq2 ⊢m=n→zm=zn
174 173 fvoveq1d ⊢m=n→log⁡zm+1=log⁡zn+1
175 172 174 oveq12d ⊢m=n→z⁢log⁡m+1m−log⁡zm+1=z⁢log⁡n+1n−log⁡zn+1
176 175 mpteq2dv ⊢m=n→z∈U⟼z⁢log⁡m+1m−log⁡zm+1=z∈U⟼z⁢log⁡n+1n−log⁡zn+1
177 cnex ⊢ℂ∈V
178 2 177 rabex2 ⊢U∈V
179 178 mptex ⊢z∈U⟼z⁢log⁡n+1n−log⁡zn+1∈V
180 176 3 179 fvmpt ⊢n∈ℕ→G⁡n=z∈U⟼z⁢log⁡n+1n−log⁡zn+1
181 180 ad2antrl ⊢φ∧n∈ℕ∧y∈U→G⁡n=z∈U⟼z⁢log⁡n+1n−log⁡zn+1
182 181 fveq1d ⊢φ∧n∈ℕ∧y∈U→G⁡n⁡y=z∈U⟼z⁢log⁡n+1n−log⁡zn+1⁡y
183 oveq1 ⊢z=y→z⁢log⁡n+1n=y⁢log⁡n+1n
184 oveq1 ⊢z=y→zn=yn
185 184 fvoveq1d ⊢z=y→log⁡zn+1=log⁡yn+1
186 183 185 oveq12d ⊢z=y→z⁢log⁡n+1n−log⁡zn+1=y⁢log⁡n+1n−log⁡yn+1
187 eqid ⊢z∈U⟼z⁢log⁡n+1n−log⁡zn+1=z∈U⟼z⁢log⁡n+1n−log⁡zn+1
188 ovex ⊢y⁢log⁡n+1n−log⁡yn+1∈V
189 186 187 188 fvmpt ⊢y∈U→z∈U⟼z⁢log⁡n+1n−log⁡zn+1⁡y=y⁢log⁡n+1n−log⁡yn+1
190 189 ad2antll ⊢φ∧n∈ℕ∧y∈U→z∈U⟼z⁢log⁡n+1n−log⁡zn+1⁡y=y⁢log⁡n+1n−log⁡yn+1
191 182 190 eqtrd ⊢φ∧n∈ℕ∧y∈U→G⁡n⁡y=y⁢log⁡n+1n−log⁡yn+1
192 191 fveq2d ⊢φ∧n∈ℕ∧y∈U→G⁡n⁡y=y⁢log⁡n+1n−log⁡yn+1
193 breq2 ⊢m=n→2⁢R≤m↔2⁢R≤n
194 oveq1 ⊢m=n→m2=n2
195 194 oveq2d ⊢m=n→2⁢R+1m2=2⁢R+1n2
196 195 oveq2d ⊢m=n→R⁢2⁢R+1m2=R⁢2⁢R+1n2
197 171 oveq2d ⊢m=n→R⁢log⁡m+1m=R⁢log⁡n+1n
198 oveq2 ⊢m=n→R+1⁢m=R+1⁢n
199 198 fveq2d ⊢m=n→log⁡R+1⁢m=log⁡R+1⁢n
200 199 oveq1d ⊢m=n→log⁡R+1⁢m+π=log⁡R+1⁢n+π
201 197 200 oveq12d ⊢m=n→R⁢log⁡m+1m+log⁡R+1⁢m+π=R⁢log⁡n+1n+log⁡R+1⁢n+π
202 193 196 201 ifbieq12d ⊢m=n→if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
203 ovex ⊢R⁢2⁢R+1n2∈V
204 ovex ⊢R⁢log⁡n+1n+log⁡R+1⁢n+π∈V
205 203 204 ifex ⊢if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π∈V
206 202 4 205 fvmpt ⊢n∈ℕ→T⁡n=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
207 206 ad2antrl ⊢φ∧n∈ℕ∧y∈U→T⁡n=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
208 167 192 207 3brtr4d ⊢φ∧n∈ℕ∧y∈U→G⁡n⁡y≤T⁡n