Proof of Theorem fsumharmonic
Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . 4
|
2 | | fsumharmonic.b |
. . . . 5
|
3 | | elfznn 12370 |
. . . . . . 7
|
4 | 3 | adantl 482 |
. . . . . 6
|
5 | 4 | nncnd 11036 |
. . . . 5
|
6 | 4 | nnne0d 11065 |
. . . . 5
|
7 | 2, 5, 6 | divcld 10801 |
. . . 4
|
8 | 1, 7 | fsumcl 14464 |
. . 3
|
9 | 8 | abscld 14175 |
. 2
|
10 | 2 | abscld 14175 |
. . . 4
|
11 | 10, 4 | nndivred 11069 |
. . 3
|
12 | 1, 11 | fsumrecl 14465 |
. 2
|
13 | | fsumharmonic.c |
. . . 4
|
14 | 1, 13 | fsumrecl 14465 |
. . 3
|
15 | | fsumharmonic.r |
. . . . 5
|
16 | 15 | simpld 475 |
. . . 4
|
17 | | fsumharmonic.t |
. . . . . . . 8
|
18 | 17 | simpld 475 |
. . . . . . 7
|
19 | | 0red 10041 |
. . . . . . . 8
|
20 | | 1red 10055 |
. . . . . . . 8
|
21 | | 0lt1 10550 |
. . . . . . . . 9
|
22 | 21 | a1i 11 |
. . . . . . . 8
|
23 | 17 | simprd 479 |
. . . . . . . 8
|
24 | 19, 20, 18, 22, 23 | ltletrd 10197 |
. . . . . . 7
|
25 | 18, 24 | elrpd 11869 |
. . . . . 6
|
26 | 25 | relogcld 24369 |
. . . . 5
|
27 | 26, 20 | readdcld 10069 |
. . . 4
|
28 | 16, 27 | remulcld 10070 |
. . 3
|
29 | 14, 28 | readdcld 10069 |
. 2
|
30 | 1, 7 | fsumabs 14533 |
. . 3
|
31 | 2, 5, 6 | absdivd 14194 |
. . . . 5
|
32 | 4 | nnrpd 11870 |
. . . . . . . 8
|
33 | 32 | rprege0d 11879 |
. . . . . . 7
|
34 | | absid 14036 |
. . . . . . 7
|
35 | 33, 34 | syl 17 |
. . . . . 6
|
36 | 35 | oveq2d 6666 |
. . . . 5
|
37 | 31, 36 | eqtrd 2656 |
. . . 4
|
38 | 37 | sumeq2dv 14433 |
. . 3
|
39 | 30, 38 | breqtrd 4679 |
. 2
|
40 | | fsumharmonic.a |
. . . . . . . . . 10
|
41 | 40, 25 | rpdivcld 11889 |
. . . . . . . . 9
|
42 | 41 | rprege0d 11879 |
. . . . . . . 8
|
43 | | flge0nn0 12621 |
. . . . . . . 8
|
44 | 42, 43 | syl 17 |
. . . . . . 7
|
45 | 44 | nn0red 11352 |
. . . . . 6
|
46 | 45 | ltp1d 10954 |
. . . . 5
|
47 | | fzdisj 12368 |
. . . . 5
|
48 | 46, 47 | syl 17 |
. . . 4
|
49 | | nn0p1nn 11332 |
. . . . . . 7
|
50 | 44, 49 | syl 17 |
. . . . . 6
|
51 | | nnuz 11723 |
. . . . . 6
|
52 | 50, 51 | syl6eleq 2711 |
. . . . 5
|
53 | 41 | rpred 11872 |
. . . . . 6
|
54 | 40 | rpred 11872 |
. . . . . 6
|
55 | 18, 24 | jca 554 |
. . . . . . . . 9
|
56 | 40 | rpregt0d 11878 |
. . . . . . . . 9
|
57 | | lediv2 10913 |
. . . . . . . . 9
|
58 | 20, 22, 55, 56, 57 | syl211anc 1332 |
. . . . . . . 8
|
59 | 23, 58 | mpbid 222 |
. . . . . . 7
|
60 | 54 | recnd 10068 |
. . . . . . . 8
|
61 | 60 | div1d 10793 |
. . . . . . 7
|
62 | 59, 61 | breqtrd 4679 |
. . . . . 6
|
63 | | flword2 12614 |
. . . . . 6
|
64 | 53, 54, 62, 63 | syl3anc 1326 |
. . . . 5
|
65 | | fzsplit2 12366 |
. . . . 5
|
66 | 52, 64, 65 | syl2anc 693 |
. . . 4
|
67 | 11 | recnd 10068 |
. . . 4
|
68 | 48, 66, 1, 67 | fsumsplit 14471 |
. . 3
|
69 | | fzfid 12772 |
. . . . 5
|
70 | | ssun1 3776 |
. . . . . . . 8
|
71 | 70, 66 | syl5sseqr 3654 |
. . . . . . 7
|
72 | 71 | sselda 3603 |
. . . . . 6
|
73 | 72, 11 | syldan 487 |
. . . . 5
|
74 | 69, 73 | fsumrecl 14465 |
. . . 4
|
75 | | fzfid 12772 |
. . . . 5
|
76 | | ssun2 3777 |
. . . . . . . 8
|
77 | 76, 66 | syl5sseqr 3654 |
. . . . . . 7
|
78 | 77 | sselda 3603 |
. . . . . 6
|
79 | 78, 11 | syldan 487 |
. . . . 5
|
80 | 75, 79 | fsumrecl 14465 |
. . . 4
|
81 | 72, 13 | syldan 487 |
. . . . . 6
|
82 | 69, 81 | fsumrecl 14465 |
. . . . 5
|
83 | | fznnfl 12661 |
. . . . . . . . . . 11
|
84 | 53, 83 | syl 17 |
. . . . . . . . . 10
|
85 | 84 | simplbda 654 |
. . . . . . . . 9
|
86 | 32 | rpred 11872 |
. . . . . . . . . . . 12
|
87 | 54 | adantr 481 |
. . . . . . . . . . . 12
|
88 | 55 | adantr 481 |
. . . . . . . . . . . 12
|
89 | | lemuldiv2 10904 |
. . . . . . . . . . . 12
|
90 | 86, 87, 88, 89 | syl3anc 1326 |
. . . . . . . . . . 11
|
91 | 18 | adantr 481 |
. . . . . . . . . . . 12
|
92 | 91, 87, 32 | lemuldivd 11921 |
. . . . . . . . . . 11
|
93 | 90, 92 | bitr3d 270 |
. . . . . . . . . 10
|
94 | 72, 93 | syldan 487 |
. . . . . . . . 9
|
95 | 85, 94 | mpbid 222 |
. . . . . . . 8
|
96 | | fsumharmonic.1 |
. . . . . . . . . 10
|
97 | 96 | ex 450 |
. . . . . . . . 9
|
98 | 72, 97 | syldan 487 |
. . . . . . . 8
|
99 | 95, 98 | mpd 15 |
. . . . . . 7
|
100 | 72, 2 | syldan 487 |
. . . . . . . . 9
|
101 | 100 | abscld 14175 |
. . . . . . . 8
|
102 | 72, 3 | syl 17 |
. . . . . . . . 9
|
103 | 102 | nnrpd 11870 |
. . . . . . . 8
|
104 | 101, 81, 103 | ledivmul2d 11926 |
. . . . . . 7
|
105 | 99, 104 | mpbird 247 |
. . . . . 6
|
106 | 69, 73, 81, 105 | fsumle 14531 |
. . . . 5
|
107 | | fsumharmonic.0 |
. . . . . 6
|
108 | 1, 13, 107, 71 | fsumless 14528 |
. . . . 5
|
109 | 74, 82, 14, 106, 108 | letrd 10194 |
. . . 4
|
110 | 78, 3 | syl 17 |
. . . . . . . 8
|
111 | 110 | nnrecred 11066 |
. . . . . . 7
|
112 | 75, 111 | fsumrecl 14465 |
. . . . . 6
|
113 | 16, 112 | remulcld 10070 |
. . . . 5
|
114 | 16 | adantr 481 |
. . . . . . . . . 10
|
115 | 114 | recnd 10068 |
. . . . . . . . 9
|
116 | 110 | nncnd 11036 |
. . . . . . . . 9
|
117 | 110 | nnne0d 11065 |
. . . . . . . . 9
|
118 | 115, 116,
117 | divrecd 10804 |
. . . . . . . 8
|
119 | 114, 110 | nndivred 11069 |
. . . . . . . 8
|
120 | 118, 119 | eqeltrrd 2702 |
. . . . . . 7
|
121 | 78, 10 | syldan 487 |
. . . . . . . . 9
|
122 | 78, 32 | syldan 487 |
. . . . . . . . 9
|
123 | | noel 3919 |
. . . . . . . . . . . . . . . 16
|
124 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
125 | 48 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
|
126 | 124, 125 | syl5bbr 274 |
. . . . . . . . . . . . . . . 16
|
127 | 123, 126 | mtbiri 317 |
. . . . . . . . . . . . . . 15
|
128 | | imnan 438 |
. . . . . . . . . . . . . . 15
|
129 | 127, 128 | sylibr 224 |
. . . . . . . . . . . . . 14
|
130 | 129 | con2d 129 |
. . . . . . . . . . . . 13
|
131 | 130 | imp 445 |
. . . . . . . . . . . 12
|
132 | 83 | baibd 948 |
. . . . . . . . . . . . . . 15
|
133 | 53, 3, 132 | syl2an 494 |
. . . . . . . . . . . . . 14
|
134 | 133, 93 | bitrd 268 |
. . . . . . . . . . . . 13
|
135 | 78, 134 | syldan 487 |
. . . . . . . . . . . 12
|
136 | 131, 135 | mtbid 314 |
. . . . . . . . . . 11
|
137 | 54 | adantr 481 |
. . . . . . . . . . . . 13
|
138 | 137, 110 | nndivred 11069 |
. . . . . . . . . . . 12
|
139 | 18 | adantr 481 |
. . . . . . . . . . . 12
|
140 | 138, 139 | ltnled 10184 |
. . . . . . . . . . 11
|
141 | 136, 140 | mpbird 247 |
. . . . . . . . . 10
|
142 | | fsumharmonic.2 |
. . . . . . . . . . . 12
|
143 | 142 | ex 450 |
. . . . . . . . . . 11
|
144 | 78, 143 | syldan 487 |
. . . . . . . . . 10
|
145 | 141, 144 | mpd 15 |
. . . . . . . . 9
|
146 | 121, 114,
122, 145 | lediv1dd 11930 |
. . . . . . . 8
|
147 | 146, 118 | breqtrd 4679 |
. . . . . . 7
|
148 | 75, 79, 120, 147 | fsumle 14531 |
. . . . . 6
|
149 | 16 | recnd 10068 |
. . . . . . 7
|
150 | 111 | recnd 10068 |
. . . . . . 7
|
151 | 75, 149, 150 | fsummulc2 14516 |
. . . . . 6
|
152 | 148, 151 | breqtrrd 4681 |
. . . . 5
|
153 | 4 | nnrecred 11066 |
. . . . . . . . . . 11
|
154 | 153 | recnd 10068 |
. . . . . . . . . 10
|
155 | 48, 66, 1, 154 | fsumsplit 14471 |
. . . . . . . . 9
|
156 | 155 | oveq1d 6665 |
. . . . . . . 8
|
157 | 102 | nnrecred 11066 |
. . . . . . . . . . 11
|
158 | 69, 157 | fsumrecl 14465 |
. . . . . . . . . 10
|
159 | 158 | recnd 10068 |
. . . . . . . . 9
|
160 | 112 | recnd 10068 |
. . . . . . . . 9
|
161 | 159, 160 | pncan2d 10394 |
. . . . . . . 8
|
162 | 156, 161 | eqtrd 2656 |
. . . . . . 7
|
163 | 1, 153 | fsumrecl 14465 |
. . . . . . . . . . 11
|
164 | 163 | adantr 481 |
. . . . . . . . . 10
|
165 | 158 | adantr 481 |
. . . . . . . . . 10
|
166 | 164, 165 | resubcld 10458 |
. . . . . . . . 9
|
167 | | 0red 10041 |
. . . . . . . . 9
|
168 | 27 | adantr 481 |
. . . . . . . . 9
|
169 | | fzfid 12772 |
. . . . . . . . . . 11
|
170 | 103 | adantlr 751 |
. . . . . . . . . . . . 13
|
171 | 170 | rpreccld 11882 |
. . . . . . . . . . . 12
|
172 | 171 | rpred 11872 |
. . . . . . . . . . 11
|
173 | 171 | rpge0d 11876 |
. . . . . . . . . . 11
|
174 | 40 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
175 | 174 | rpge0d 11876 |
. . . . . . . . . . . . . . 15
|
176 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
177 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . 16
|
178 | 176, 177 | syl6breqr 4695 |
. . . . . . . . . . . . . . 15
|
179 | 54 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
180 | | 0z 11388 |
. . . . . . . . . . . . . . . 16
|
181 | | flbi 12617 |
. . . . . . . . . . . . . . . 16
|
182 | 179, 180,
181 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
183 | 175, 178,
182 | mpbir2and 957 |
. . . . . . . . . . . . . 14
|
184 | 183 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
185 | | fz10 12362 |
. . . . . . . . . . . . 13
|
186 | 184, 185 | syl6eq 2672 |
. . . . . . . . . . . 12
|
187 | | 0ss 3972 |
. . . . . . . . . . . 12
|
188 | 186, 187 | syl6eqss 3655 |
. . . . . . . . . . 11
|
189 | 169, 172,
173, 188 | fsumless 14528 |
. . . . . . . . . 10
|
190 | 164, 165 | suble0d 10618 |
. . . . . . . . . 10
|
191 | 189, 190 | mpbird 247 |
. . . . . . . . 9
|
192 | 18, 23 | logge0d 24376 |
. . . . . . . . . . 11
|
193 | | 0le1 10551 |
. . . . . . . . . . . 12
|
194 | 193 | a1i 11 |
. . . . . . . . . . 11
|
195 | 26, 20, 192, 194 | addge0d 10603 |
. . . . . . . . . 10
|
196 | 195 | adantr 481 |
. . . . . . . . 9
|
197 | 166, 167,
168, 191, 196 | letrd 10194 |
. . . . . . . 8
|
198 | | harmonicubnd 24736 |
. . . . . . . . . . 11
|
199 | 54, 198 | sylan 488 |
. . . . . . . . . 10
|
200 | | harmoniclbnd 24735 |
. . . . . . . . . . . 12
|
201 | 41, 200 | syl 17 |
. . . . . . . . . . 11
|
202 | 201 | adantr 481 |
. . . . . . . . . 10
|
203 | 40 | relogcld 24369 |
. . . . . . . . . . . . 13
|
204 | | peano2re 10209 |
. . . . . . . . . . . . 13
|
205 | 203, 204 | syl 17 |
. . . . . . . . . . . 12
|
206 | 41 | relogcld 24369 |
. . . . . . . . . . . 12
|
207 | | le2sub 10527 |
. . . . . . . . . . . 12
|
208 | 163, 158,
205, 206, 207 | syl22anc 1327 |
. . . . . . . . . . 11
|
209 | 208 | adantr 481 |
. . . . . . . . . 10
|
210 | 199, 202,
209 | mp2and 715 |
. . . . . . . . 9
|
211 | 203 | recnd 10068 |
. . . . . . . . . . . 12
|
212 | 20 | recnd 10068 |
. . . . . . . . . . . 12
|
213 | 26 | recnd 10068 |
. . . . . . . . . . . 12
|
214 | 211, 212,
213 | pnncand 10431 |
. . . . . . . . . . 11
|
215 | 40, 25 | relogdivd 24372 |
. . . . . . . . . . . 12
|
216 | 215 | oveq2d 6666 |
. . . . . . . . . . 11
|
217 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
218 | | addcom 10222 |
. . . . . . . . . . . 12
|
219 | 213, 217,
218 | sylancl 694 |
. . . . . . . . . . 11
|
220 | 214, 216,
219 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
221 | 220 | adantr 481 |
. . . . . . . . 9
|
222 | 210, 221 | breqtrd 4679 |
. . . . . . . 8
|
223 | 197, 222,
54, 20 | ltlecasei 10145 |
. . . . . . 7
|
224 | 162, 223 | eqbrtrrd 4677 |
. . . . . 6
|
225 | | lemul2a 10878 |
. . . . . 6
|
226 | 112, 27, 15, 224, 225 | syl31anc 1329 |
. . . . 5
|
227 | 80, 113, 28, 152, 226 | letrd 10194 |
. . . 4
|
228 | 74, 80, 14, 28, 109, 227 | le2addd 10646 |
. . 3
|
229 | 68, 228 | eqbrtrd 4675 |
. 2
|
230 | 9, 12, 29, 39, 229 | letrd 10194 |
1
|