Metamath Proof Explorer

Theorem lgamgulmlem3

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.n ⊢φ→N∈ℕ
lgamgulm.a ⊢φ→A∈U
lgamgulm.l ⊢φ→2⁢R≤N
Assertion lgamgulmlem3 ⊢φ→A⁢log⁡N+1N−log⁡AN+1≤R⁢2⁢R+1N2

Proof

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