Metamath Proof Explorer

Theorem lgamgulmlem3

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

Ref Expression
Hypotheses lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamgulm.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lgamgulm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
lgamgulm.l ⊢ ( 𝜑 → ( 2 · 𝑅 ) ≤ 𝑁 )
Assertion lgamgulmlem3 ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3 lgamgulm.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 lgamgulm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
5 lgamgulm.l ⊢ ( 𝜑 → ( 2 · 𝑅 ) ≤ 𝑁 )
6 1 2 lgamgulmlem1 ⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
7 6 4 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
8 7 eldifad ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
9 3 peano2nnd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
10 9 nnrpd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ+ )
11 3 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
12 10 11 rpdivcld ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℝ+ )
13 12 relogcld ⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℝ )
14 13 recnd ⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ∈ ℂ )
15 8 14 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ∈ ℂ )
16 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
17 3 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
18 8 16 17 divcld ⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) ∈ ℂ )
19 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
20 18 19 addcld ⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ∈ ℂ )
21 7 3 dmgmdivn0 ⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) + 1 ) ≠ 0 )
22 20 21 logcld ⊢ ( 𝜑 → ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ∈ ℂ )
23 15 22 subcld ⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ ℂ )
24 23 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ∈ ℝ )
25 15 18 subcld ⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ∈ ℂ )
26 25 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) ∈ ℝ )
27 18 22 subcld ⊢ ( 𝜑 → ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ∈ ℂ )
28 27 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ∈ ℝ )
29 26 28 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ∈ ℝ )
30 1 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
31 2re ⊢ 2 ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
33 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
34 30 33 readdcld ⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℝ )
35 32 34 remulcld ⊢ ( 𝜑 → ( 2 · ( 𝑅 + 1 ) ) ∈ ℝ )
36 3 nnsqcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
37 35 36 nndivred ⊢ ( 𝜑 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ∈ ℝ )
38 30 37 remulcld ⊢ ( 𝜑 → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) ∈ ℝ )
39 15 22 18 abs3difd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) )
40 3 nnrecred ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
41 9 nnrecred ⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ∈ ℝ )
42 40 41 resubcld ⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ∈ ℝ )
43 30 42 remulcld ⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) ∈ ℝ )
44 32 30 remulcld ⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ )
45 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
46 1 nnrpd ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
47 30 46 ltaddrpd ⊢ ( 𝜑 → 𝑅 < ( 𝑅 + 𝑅 ) )
48 1 nncnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
49 48 2timesd ⊢ ( 𝜑 → ( 2 · 𝑅 ) = ( 𝑅 + 𝑅 ) )
50 47 49 breqtrrd ⊢ ( 𝜑 → 𝑅 < ( 2 · 𝑅 ) )
51 30 44 45 50 5 ltletrd ⊢ ( 𝜑 → 𝑅 < 𝑁 )
52 difrp ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) )
53 30 45 52 syl2anc ⊢ ( 𝜑 → ( 𝑅 < 𝑁 ↔ ( 𝑁 − 𝑅 ) ∈ ℝ+ ) )
54 51 53 mpbid ⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℝ+ )
55 54 rprecred ⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℝ )
56 55 40 resubcld ⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℝ )
57 30 56 remulcld ⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ )
58 43 57 readdcld ⊢ ( 𝜑 → ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ∈ ℝ )
59 8 16 17 divrecd ⊢ ( 𝜑 → ( 𝐴 / 𝑁 ) = ( 𝐴 · ( 1 / 𝑁 ) ) )
60 59 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 · ( 1 / 𝑁 ) ) ) )
61 40 recnd ⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℂ )
62 8 14 61 subdid ⊢ ( 𝜑 → ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 · ( 1 / 𝑁 ) ) ) )
63 60 62 eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) = ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) )
64 63 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) = ( abs ‘ ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
65 14 61 subcld ⊢ ( 𝜑 → ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ )
66 8 65 absmuld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 · ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
67 64 66 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) )
68 8 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
69 65 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ∈ ℝ )
70 8 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
71 65 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) )
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 4 79 syl ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝐴 + 𝑘 ) ) ) )
81 80 simpld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 𝑅 )
82 10 11 relogdivd ⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
83 logdifbnd ⊢ ( 𝑁 ∈ ℝ+ → ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
84 11 83 syl ⊢ ( 𝜑 → ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
85 82 84 eqbrtrd ⊢ ( 𝜑 → ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ≤ ( 1 / 𝑁 ) )
86 13 40 85 abssuble0d ⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 1 / 𝑁 ) − ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
87 logdiflbnd ⊢ ( 𝑁 ∈ ℝ+ → ( 1 / ( 𝑁 + 1 ) ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
88 11 87 syl ⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ≤ ( ( log ‘ ( 𝑁 + 1 ) ) − ( log ‘ 𝑁 ) ) )
89 88 82 breqtrrd ⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ≤ ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) )
90 41 13 40 89 lesub2dd ⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) ≤ ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) )
91 86 90 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ≤ ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) )
92 68 30 69 42 70 71 81 91 lemul12ad ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( abs ‘ ( ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) − ( 1 / 𝑁 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
93 67 92 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) ≤ ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
94 1 2 3 4 5 lgamgulmlem2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) )
95 26 28 43 57 93 94 le2addd ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ≤ ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
96 16 48 subcld ⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℂ )
97 16 19 addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℂ )
98 30 51 gtned ⊢ ( 𝜑 → 𝑁 ≠ 𝑅 )
99 16 48 98 subne0d ⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ≠ 0 )
100 9 nnne0d ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
101 96 97 99 100 subrecd ⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) = ( ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) )
102 16 19 48 pnncand ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) = ( 1 + 𝑅 ) )
103 19 48 102 comraddd ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) = ( 𝑅 + 1 ) )
104 103 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) − ( 𝑁 − 𝑅 ) ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) = ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) )
105 101 104 eqtr2d ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) = ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) )
106 105 oveq2d ⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) = ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) ) )
107 97 100 reccld ⊢ ( 𝜑 → ( 1 / ( 𝑁 + 1 ) ) ∈ ℂ )
108 96 99 reccld ⊢ ( 𝜑 → ( 1 / ( 𝑁 − 𝑅 ) ) ∈ ℂ )
109 61 107 108 npncan3d ⊢ ( 𝜑 → ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) = ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) )
110 109 eqcomd ⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) = ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) )
111 110 oveq2d ⊢ ( 𝜑 → ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / ( 𝑁 + 1 ) ) ) ) = ( 𝑅 · ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
112 42 recnd ⊢ ( 𝜑 → ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ∈ ℂ )
113 56 recnd ⊢ ( 𝜑 → ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ∈ ℂ )
114 48 112 113 adddid ⊢ ( 𝜑 → ( 𝑅 · ( ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) + ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) = ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
115 106 111 114 3eqtrd ⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) = ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) )
116 54 10 rpmulcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ∈ ℝ+ )
117 34 116 rerpdivcld ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ∈ ℝ )
118 46 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑅 )
119 2z ⊢ 2 ∈ ℤ
120 119 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
121 11 120 rpexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ+ )
122 121 rphalfcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) ∈ ℝ+ )
123 0le1 ⊢ 0 ≤ 1
124 123 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
125 30 33 118 124 addge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑅 + 1 ) )
126 16 sqvald ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
127 126 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) = ( ( 𝑁 · 𝑁 ) / 2 ) )
128 32 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
129 2ne0 ⊢ 2 ≠ 0
130 129 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
131 16 16 128 130 div23d ⊢ ( 𝜑 → ( ( 𝑁 · 𝑁 ) / 2 ) = ( ( 𝑁 / 2 ) · 𝑁 ) )
132 127 131 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) = ( ( 𝑁 / 2 ) · 𝑁 ) )
133 45 rehalfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ )
134 45 30 resubcld ⊢ ( 𝜑 → ( 𝑁 − 𝑅 ) ∈ ℝ )
135 45 33 readdcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
136 2rp ⊢ 2 ∈ ℝ+
137 136 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
138 11 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
139 45 137 138 divge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 / 2 ) )
140 30 45 137 lemuldiv2d ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) ≤ 𝑁 ↔ 𝑅 ≤ ( 𝑁 / 2 ) ) )
141 5 140 mpbid ⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 / 2 ) )
142 16 2halvesd ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = 𝑁 )
143 133 recnd ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℂ )
144 16 143 143 subaddd ⊢ ( 𝜑 → ( ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) ↔ ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = 𝑁 ) )
145 142 144 mpbird ⊢ ( 𝜑 → ( 𝑁 − ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
146 141 145 breqtrrd ⊢ ( 𝜑 → 𝑅 ≤ ( 𝑁 − ( 𝑁 / 2 ) ) )
147 30 45 133 146 lesubd ⊢ ( 𝜑 → ( 𝑁 / 2 ) ≤ ( 𝑁 − 𝑅 ) )
148 45 lep1d ⊢ ( 𝜑 → 𝑁 ≤ ( 𝑁 + 1 ) )
149 133 134 45 135 139 138 147 148 lemul12ad ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) · 𝑁 ) ≤ ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) )
150 132 149 eqbrtrd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / 2 ) ≤ ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) )
151 122 116 34 125 150 lediv2ad ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ≤ ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) )
152 1 peano2nnd ⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℕ )
153 152 nncnd ⊢ ( 𝜑 → ( 𝑅 + 1 ) ∈ ℂ )
154 36 nncnd ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
155 36 nnne0d ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ≠ 0 )
156 153 154 128 155 130 divdiv2d ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) = ( ( ( 𝑅 + 1 ) · 2 ) / ( 𝑁 ↑ 2 ) ) )
157 153 128 mulcomd ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) · 2 ) = ( 2 · ( 𝑅 + 1 ) ) )
158 157 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑅 + 1 ) · 2 ) / ( 𝑁 ↑ 2 ) ) = ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) )
159 156 158 eqtr2d ⊢ ( 𝜑 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) = ( ( 𝑅 + 1 ) / ( ( 𝑁 ↑ 2 ) / 2 ) ) )
160 151 159 breqtrrd ⊢ ( 𝜑 → ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ≤ ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) )
161 117 37 30 118 160 lemul2ad ⊢ ( 𝜑 → ( 𝑅 · ( ( 𝑅 + 1 ) / ( ( 𝑁 − 𝑅 ) · ( 𝑁 + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
162 115 161 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝑅 · ( ( 1 / 𝑁 ) − ( 1 / ( 𝑁 + 1 ) ) ) ) + ( 𝑅 · ( ( 1 / ( 𝑁 − 𝑅 ) ) − ( 1 / 𝑁 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
163 29 58 38 95 162 letrd ⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( 𝐴 / 𝑁 ) ) ) + ( abs ‘ ( ( 𝐴 / 𝑁 ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
164 24 29 38 39 163 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 · ( log ‘ ( ( 𝑁 + 1 ) / 𝑁 ) ) ) − ( log ‘ ( ( 𝐴 / 𝑁 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )