Metamath Proof Explorer

Theorem lgamgulmlem5

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

Ref Expression
Hypotheses lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamgulm.g ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
lgamgulm.t ⊢ 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
Assertion lgamgulmlem5 ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) ≤ ( 𝑇 ‘ 𝑛 ) )

Proof

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