Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . . . . 9
|
2 | | elfznn 12370 |
. . . . . . . . . . . . 13
|
3 | 2 | adantl 482 |
. . . . . . . . . . . 12
|
4 | 3 | nnrpd 11870 |
. . . . . . . . . . 11
|
5 | 4 | relogcld 24369 |
. . . . . . . . . 10
|
6 | 5, 3 | nndivred 11069 |
. . . . . . . . 9
|
7 | 1, 6 | fsumrecl 14465 |
. . . . . . . 8
|
8 | 7 | recnd 10068 |
. . . . . . 7
|
9 | | elioore 12205 |
. . . . . . . . . . . . 13
|
10 | 9 | adantl 482 |
. . . . . . . . . . . 12
|
11 | | 1rp 11836 |
. . . . . . . . . . . . 13
|
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
|
13 | | 1red 10055 |
. . . . . . . . . . . . 13
|
14 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
|
15 | 14 | adantl 482 |
. . . . . . . . . . . . . 14
|
16 | 15 | simpld 475 |
. . . . . . . . . . . . 13
|
17 | 13, 10, 16 | ltled 10185 |
. . . . . . . . . . . 12
|
18 | 10, 12, 17 | rpgecld 11911 |
. . . . . . . . . . 11
|
19 | 18 | relogcld 24369 |
. . . . . . . . . 10
|
20 | 19 | resqcld 13035 |
. . . . . . . . 9
|
21 | 20 | rehalfcld 11279 |
. . . . . . . 8
|
22 | 21 | recnd 10068 |
. . . . . . 7
|
23 | 19 | recnd 10068 |
. . . . . . 7
|
24 | 10, 16 | rplogcld 24375 |
. . . . . . . 8
|
25 | 24 | rpne0d 11877 |
. . . . . . 7
|
26 | 8, 22, 23, 25 | divsubdird 10840 |
. . . . . 6
|
27 | 7, 21 | resubcld 10458 |
. . . . . . . 8
|
28 | 27 | recnd 10068 |
. . . . . . 7
|
29 | 28, 23, 25 | divrecd 10804 |
. . . . . 6
|
30 | 20 | recnd 10068 |
. . . . . . . . 9
|
31 | | 2cnd 11093 |
. . . . . . . . 9
|
32 | | 2ne0 11113 |
. . . . . . . . . 10
|
33 | 32 | a1i 11 |
. . . . . . . . 9
|
34 | 30, 31, 23, 33, 25 | divdiv32d 10826 |
. . . . . . . 8
|
35 | 23 | sqvald 13005 |
. . . . . . . . . . 11
|
36 | 35 | oveq1d 6665 |
. . . . . . . . . 10
|
37 | 23, 23, 25 | divcan3d 10806 |
. . . . . . . . . 10
|
38 | 36, 37 | eqtrd 2656 |
. . . . . . . . 9
|
39 | 38 | oveq1d 6665 |
. . . . . . . 8
|
40 | 34, 39 | eqtrd 2656 |
. . . . . . 7
|
41 | 40 | oveq2d 6666 |
. . . . . 6
|
42 | 26, 29, 41 | 3eqtr3rd 2665 |
. . . . 5
|
43 | 42 | mpteq2dva 4744 |
. . . 4
|
44 | 24 | rprecred 11883 |
. . . . 5
|
45 | 18 | ex 450 |
. . . . . . 7
|
46 | 45 | ssrdv 3609 |
. . . . . 6
|
47 | | eqid 2622 |
. . . . . . . . 9
|
48 | 47 | logdivsum 25222 |
. . . . . . . 8
|
49 | 48 | simp2i 1071 |
. . . . . . 7
|
50 | | rlimdmo1 14348 |
. . . . . . 7
|
51 | 49, 50 | mp1i 13 |
. . . . . 6
|
52 | 46, 51 | o1res2 14294 |
. . . . 5
|
53 | | divlogrlim 24381 |
. . . . . 6
|
54 | | rlimo1 14347 |
. . . . . 6
|
55 | 53, 54 | mp1i 13 |
. . . . 5
|
56 | 27, 44, 52, 55 | o1mul2 14355 |
. . . 4
|
57 | 43, 56 | eqeltrd 2701 |
. . 3
|
58 | 8, 23, 25 | divcld 10801 |
. . . . 5
|
59 | 23 | halfcld 11277 |
. . . . 5
|
60 | 58, 59 | subcld 10392 |
. . . 4
|
61 | | elfznn 12370 |
. . . . . . . . . . . 12
|
62 | 61 | adantl 482 |
. . . . . . . . . . 11
|
63 | | vmacl 24844 |
. . . . . . . . . . 11
Λ |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
Λ |
65 | 64, 62 | nndivred 11069 |
. . . . . . . . 9
Λ |
66 | 18 | adantr 481 |
. . . . . . . . . . 11
|
67 | 62 | nnrpd 11870 |
. . . . . . . . . . 11
|
68 | 66, 67 | rpdivcld 11889 |
. . . . . . . . . 10
|
69 | 68 | relogcld 24369 |
. . . . . . . . 9
|
70 | 65, 69 | remulcld 10070 |
. . . . . . . 8
Λ |
71 | 1, 70 | fsumrecl 14465 |
. . . . . . 7
Λ |
72 | 71 | recnd 10068 |
. . . . . 6
Λ |
73 | 24 | rpcnd 11874 |
. . . . . 6
|
74 | 72, 73, 25 | divcld 10801 |
. . . . 5
Λ |
75 | 73 | halfcld 11277 |
. . . . 5
|
76 | 74, 75 | subcld 10392 |
. . . 4
Λ |
77 | 58, 74, 59 | nnncan2d 10427 |
. . . . . . 7
Λ Λ |
78 | 8, 72, 23, 25 | divsubdird 10840 |
. . . . . . 7
Λ Λ |
79 | | fzfid 12772 |
. . . . . . . . . . . 12
|
80 | 64 | adantr 481 |
. . . . . . . . . . . . 13
Λ |
81 | 62 | adantr 481 |
. . . . . . . . . . . . . 14
|
82 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
|
83 | 82 | adantl 482 |
. . . . . . . . . . . . . 14
|
84 | 81, 83 | nnmulcld 11068 |
. . . . . . . . . . . . 13
|
85 | 80, 84 | nndivred 11069 |
. . . . . . . . . . . 12
Λ |
86 | 79, 85 | fsumrecl 14465 |
. . . . . . . . . . 11
Λ |
87 | 86 | recnd 10068 |
. . . . . . . . . 10
Λ |
88 | 70 | recnd 10068 |
. . . . . . . . . 10
Λ |
89 | 1, 87, 88 | fsumsub 14520 |
. . . . . . . . 9
Λ Λ
Λ Λ |
90 | 64 | recnd 10068 |
. . . . . . . . . . . . 13
Λ |
91 | 62 | nncnd 11036 |
. . . . . . . . . . . . 13
|
92 | 62 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
93 | 90, 91, 92 | divcld 10801 |
. . . . . . . . . . . 12
Λ |
94 | 83 | nnrecred 11066 |
. . . . . . . . . . . . . 14
|
95 | 79, 94 | fsumrecl 14465 |
. . . . . . . . . . . . 13
|
96 | 95 | recnd 10068 |
. . . . . . . . . . . 12
|
97 | 69 | recnd 10068 |
. . . . . . . . . . . 12
|
98 | 93, 96, 97 | subdid 10486 |
. . . . . . . . . . 11
Λ
Λ Λ |
99 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
Λ |
100 | 91 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
101 | 83 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
|
102 | 92 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
103 | 83 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
|
104 | 99, 100, 101, 102, 103 | divdiv1d 10832 |
. . . . . . . . . . . . . . 15
Λ Λ |
105 | 99, 100, 102 | divcld 10801 |
. . . . . . . . . . . . . . . 16
Λ |
106 | 105, 101,
103 | divrecd 10804 |
. . . . . . . . . . . . . . 15
Λ Λ |
107 | 104, 106 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
Λ Λ |
108 | 107 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
Λ Λ |
109 | 101, 103 | reccld 10794 |
. . . . . . . . . . . . . 14
|
110 | 79, 93, 109 | fsummulc2 14516 |
. . . . . . . . . . . . 13
Λ Λ |
111 | 108, 110 | eqtr4d 2659 |
. . . . . . . . . . . 12
Λ Λ |
112 | 111 | oveq1d 6665 |
. . . . . . . . . . 11
Λ Λ Λ Λ |
113 | 98, 112 | eqtr4d 2659 |
. . . . . . . . . 10
Λ
Λ Λ |
114 | 113 | sumeq2dv 14433 |
. . . . . . . . 9
Λ Λ Λ |
115 | | vmasum 24941 |
. . . . . . . . . . . . . . 15
Λ |
116 | 3, 115 | syl 17 |
. . . . . . . . . . . . . 14
Λ |
117 | 116 | oveq1d 6665 |
. . . . . . . . . . . . 13
Λ |
118 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
119 | | dvdsssfz1 15040 |
. . . . . . . . . . . . . . . 16
|
120 | 3, 119 | syl 17 |
. . . . . . . . . . . . . . 15
|
121 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
|
122 | 118, 120,
121 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
123 | 3 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
124 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
|
125 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
126 | 124, 125 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
127 | 126, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
Λ |
128 | 127 | recnd 10068 |
. . . . . . . . . . . . . . 15
Λ |
129 | 128 | anassrs 680 |
. . . . . . . . . . . . . 14
Λ |
130 | 3 | nnne0d 11065 |
. . . . . . . . . . . . . 14
|
131 | 122, 123,
129, 130 | fsumdivc 14518 |
. . . . . . . . . . . . 13
Λ
Λ |
132 | 117, 131 | eqtr3d 2658 |
. . . . . . . . . . . 12
Λ |
133 | 132 | sumeq2dv 14433 |
. . . . . . . . . . 11
Λ |
134 | | oveq2 6658 |
. . . . . . . . . . . 12
Λ Λ |
135 | 2 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
136 | 135 | nncnd 11036 |
. . . . . . . . . . . . 13
|
137 | 135 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
138 | 128, 136,
137 | divcld 10801 |
. . . . . . . . . . . 12
Λ |
139 | 134, 10, 138 | dvdsflsumcom 24914 |
. . . . . . . . . . 11
Λ Λ |
140 | 133, 139 | eqtrd 2656 |
. . . . . . . . . 10
Λ |
141 | 140 | oveq1d 6665 |
. . . . . . . . 9
Λ
Λ Λ |
142 | 89, 114, 141 | 3eqtr4rd 2667 |
. . . . . . . 8
Λ
Λ |
143 | 142 | oveq1d 6665 |
. . . . . . 7
Λ
Λ |
144 | 77, 78, 143 | 3eqtr2d 2662 |
. . . . . 6
Λ Λ |
145 | 144 | mpteq2dva 4744 |
. . . . 5
Λ Λ |
146 | | 1red 10055 |
. . . . . . 7
|
147 | 1, 65 | fsumrecl 14465 |
. . . . . . . . 9
Λ |
148 | 147, 24 | rerpdivcld 11903 |
. . . . . . . 8
Λ |
149 | | ioossre 12235 |
. . . . . . . . . . 11
|
150 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
151 | | o1const 14350 |
. . . . . . . . . . 11
|
152 | 149, 150,
151 | mp2an 708 |
. . . . . . . . . 10
|
153 | 152 | a1i 11 |
. . . . . . . . 9
|
154 | 148 | recnd 10068 |
. . . . . . . . . 10
Λ |
155 | 12 | rpcnd 11874 |
. . . . . . . . . 10
|
156 | 147 | recnd 10068 |
. . . . . . . . . . . . . 14
Λ |
157 | 156, 23, 23, 25 | divsubdird 10840 |
. . . . . . . . . . . . 13
Λ Λ |
158 | 156, 23 | subcld 10392 |
. . . . . . . . . . . . . 14
Λ |
159 | 158, 23, 25 | divrecd 10804 |
. . . . . . . . . . . . 13
Λ Λ |
160 | 23, 25 | dividd 10799 |
. . . . . . . . . . . . . 14
|
161 | 160 | oveq2d 6666 |
. . . . . . . . . . . . 13
Λ Λ |
162 | 157, 159,
161 | 3eqtr3rd 2665 |
. . . . . . . . . . . 12
Λ
Λ |
163 | 162 | mpteq2dva 4744 |
. . . . . . . . . . 11
Λ Λ |
164 | 147, 19 | resubcld 10458 |
. . . . . . . . . . . 12
Λ |
165 | | vmadivsum 25171 |
. . . . . . . . . . . . . 14
Λ |
166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
Λ |
167 | 46, 166 | o1res2 14294 |
. . . . . . . . . . . 12
Λ |
168 | 164, 44, 167, 55 | o1mul2 14355 |
. . . . . . . . . . 11
Λ |
169 | 163, 168 | eqeltrd 2701 |
. . . . . . . . . 10
Λ |
170 | 154, 155,
169 | o1dif 14360 |
. . . . . . . . 9
Λ |
171 | 153, 170 | mpbird 247 |
. . . . . . . 8
Λ |
172 | 148, 171 | o1lo1d 14270 |
. . . . . . 7
Λ |
173 | 95, 69 | resubcld 10458 |
. . . . . . . . . 10
|
174 | 65, 173 | remulcld 10070 |
. . . . . . . . 9
Λ
|
175 | 1, 174 | fsumrecl 14465 |
. . . . . . . 8
Λ |
176 | 175, 24 | rerpdivcld 11903 |
. . . . . . 7
Λ |
177 | | 1red 10055 |
. . . . . . . . . . . 12
|
178 | | vmage0 24847 |
. . . . . . . . . . . . . 14
Λ |
179 | 62, 178 | syl 17 |
. . . . . . . . . . . . 13
Λ |
180 | 64, 67, 179 | divge0d 11912 |
. . . . . . . . . . . 12
Λ |
181 | 68 | rpred 11872 |
. . . . . . . . . . . . . 14
|
182 | 91 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
183 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . . 18
|
184 | 10, 183 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
185 | 184 | simplbda 654 |
. . . . . . . . . . . . . . . 16
|
186 | 182, 185 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
187 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
188 | 177, 187,
67 | lemuldivd 11921 |
. . . . . . . . . . . . . . 15
|
189 | 186, 188 | mpbid 222 |
. . . . . . . . . . . . . 14
|
190 | | harmonicubnd 24736 |
. . . . . . . . . . . . . 14
|
191 | 181, 189,
190 | syl2anc 693 |
. . . . . . . . . . . . 13
|
192 | 95, 69, 177 | lesubadd2d 10626 |
. . . . . . . . . . . . 13
|
193 | 191, 192 | mpbird 247 |
. . . . . . . . . . . 12
|
194 | 173, 177,
65, 180, 193 | lemul2ad 10964 |
. . . . . . . . . . 11
Λ
Λ |
195 | 93 | mulid1d 10057 |
. . . . . . . . . . 11
Λ Λ |
196 | 194, 195 | breqtrd 4679 |
. . . . . . . . . 10
Λ
Λ |
197 | 1, 174, 65, 196 | fsumle 14531 |
. . . . . . . . 9
Λ Λ |
198 | 175, 147,
24, 197 | lediv1dd 11930 |
. . . . . . . 8
Λ Λ |
199 | 198 | adantrr 753 |
. . . . . . 7
Λ Λ |
200 | 146, 172,
148, 176, 199 | lo1le 14382 |
. . . . . 6
Λ |
201 | | 0red 10041 |
. . . . . . 7
|
202 | | harmoniclbnd 24735 |
. . . . . . . . . . . 12
|
203 | 68, 202 | syl 17 |
. . . . . . . . . . 11
|
204 | 95, 69 | subge0d 10617 |
. . . . . . . . . . 11
|
205 | 203, 204 | mpbird 247 |
. . . . . . . . . 10
|
206 | 65, 173, 180, 205 | mulge0d 10604 |
. . . . . . . . 9
Λ |
207 | 1, 174, 206 | fsumge0 14527 |
. . . . . . . 8
Λ |
208 | 175, 24, 207 | divge0d 11912 |
. . . . . . 7
Λ |
209 | 176, 201,
208 | o1lo12 14269 |
. . . . . 6
Λ Λ |
210 | 200, 209 | mpbird 247 |
. . . . 5
Λ |
211 | 145, 210 | eqeltrd 2701 |
. . . 4
Λ |
212 | 60, 76, 211 | o1dif 14360 |
. . 3
Λ |
213 | 57, 212 | mpbid 222 |
. 2
Λ |
214 | 213 | trud 1493 |
1
Λ |