Step | Hyp | Ref
| Expression |
1 | | 2re 11090 |
. . . 4
|
2 | | fzfid 12772 |
. . . . 5
|
3 | | elfzuz 12338 |
. . . . . . . . . 10
|
4 | 3 | adantl 482 |
. . . . . . . . 9
|
5 | | nnuz 11723 |
. . . . . . . . 9
|
6 | 4, 5 | syl6eleqr 2712 |
. . . . . . . 8
|
7 | 6 | nnrpd 11870 |
. . . . . . 7
|
8 | 7 | relogcld 24369 |
. . . . . 6
|
9 | 8, 6 | nndivred 11069 |
. . . . 5
|
10 | 2, 9 | fsumrecl 14465 |
. . . 4
|
11 | | remulcl 10021 |
. . . 4
|
12 | 1, 10, 11 | sylancr 695 |
. . 3
|
13 | | elfznn 12370 |
. . . . . . 7
|
14 | 13 | adantl 482 |
. . . . . 6
|
15 | 14 | nnrecred 11066 |
. . . . 5
|
16 | 2, 15 | fsumrecl 14465 |
. . . 4
|
17 | 16 | resqcld 13035 |
. . 3
|
18 | | nnrp 11842 |
. . . . . 6
|
19 | 18 | relogcld 24369 |
. . . . 5
|
20 | | peano2re 10209 |
. . . . 5
|
21 | 19, 20 | syl 17 |
. . . 4
|
22 | 21 | resqcld 13035 |
. . 3
|
23 | 10 | recnd 10068 |
. . . . 5
|
24 | 23 | 2timesd 11275 |
. . . 4
|
25 | | fzfid 12772 |
. . . . . . . . 9
|
26 | | elfznn 12370 |
. . . . . . . . . . 11
|
27 | 26 | adantl 482 |
. . . . . . . . . 10
|
28 | 27 | nnrecred 11066 |
. . . . . . . . 9
|
29 | 25, 28 | fsumrecl 14465 |
. . . . . . . 8
|
30 | 29, 6 | nndivred 11069 |
. . . . . . 7
|
31 | 2, 30 | fsumrecl 14465 |
. . . . . 6
|
32 | | fzfid 12772 |
. . . . . . . . 9
|
33 | | elfznn 12370 |
. . . . . . . . . . 11
|
34 | 33 | adantl 482 |
. . . . . . . . . 10
|
35 | 34 | nnrecred 11066 |
. . . . . . . . 9
|
36 | 32, 35 | fsumrecl 14465 |
. . . . . . . 8
|
37 | 36, 6 | nndivred 11069 |
. . . . . . 7
|
38 | 2, 37 | fsumrecl 14465 |
. . . . . 6
|
39 | 6 | nncnd 11036 |
. . . . . . . . . . . . . . 15
|
40 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
|
41 | | npcan 10290 |
. . . . . . . . . . . . . . 15
|
42 | 39, 40, 41 | sylancl 694 |
. . . . . . . . . . . . . 14
|
43 | 42 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . 12
|
45 | | nnm1nn0 11334 |
. . . . . . . . . . . . 13
|
46 | | harmonicbnd3 24734 |
. . . . . . . . . . . . 13
|
47 | 6, 45, 46 | 3syl 18 |
. . . . . . . . . . . 12
|
48 | 44, 47 | eqeltrrd 2702 |
. . . . . . . . . . 11
|
49 | | 0re 10040 |
. . . . . . . . . . . . 13
|
50 | | emre 24732 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | elicc2i 12239 |
. . . . . . . . . . . 12
|
52 | 51 | simp2bi 1077 |
. . . . . . . . . . 11
|
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
|
54 | 36, 8 | subge0d 10617 |
. . . . . . . . . 10
|
55 | 53, 54 | mpbid 222 |
. . . . . . . . 9
|
56 | 8, 36, 7, 55 | lediv1dd 11930 |
. . . . . . . 8
|
57 | 27 | nnrpd 11870 |
. . . . . . . . . . . 12
|
58 | 57 | rpreccld 11882 |
. . . . . . . . . . 11
|
59 | 58 | rpge0d 11876 |
. . . . . . . . . 10
|
60 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . 13
|
62 | | peano2zm 11420 |
. . . . . . . . . . . . 13
|
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
|
64 | 6 | nnred 11035 |
. . . . . . . . . . . . 13
|
65 | 64 | lem1d 10957 |
. . . . . . . . . . . 12
|
66 | | eluz2 11693 |
. . . . . . . . . . . 12
|
67 | 63, 61, 65, 66 | syl3anbrc 1246 |
. . . . . . . . . . 11
|
68 | | fzss2 12381 |
. . . . . . . . . . 11
|
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
|
70 | 25, 28, 59, 69 | fsumless 14528 |
. . . . . . . . 9
|
71 | 6 | nngt0d 11064 |
. . . . . . . . . 10
|
72 | | lediv1 10888 |
. . . . . . . . . 10
|
73 | 36, 29, 64, 71, 72 | syl112anc 1330 |
. . . . . . . . 9
|
74 | 70, 73 | mpbid 222 |
. . . . . . . 8
|
75 | 9, 37, 30, 56, 74 | letrd 10194 |
. . . . . . 7
|
76 | 2, 9, 30, 75 | fsumle 14531 |
. . . . . 6
|
77 | 2, 9, 37, 56 | fsumle 14531 |
. . . . . 6
|
78 | 10, 10, 31, 38, 76, 77 | le2addd 10646 |
. . . . 5
|
79 | | oveq1 6657 |
. . . . . . . . . . 11
|
80 | 79 | oveq2d 6666 |
. . . . . . . . . 10
|
81 | 80 | sumeq1d 14431 |
. . . . . . . . 9
|
82 | 81, 81 | jca 554 |
. . . . . . . 8
|
83 | | oveq1 6657 |
. . . . . . . . . . 11
|
84 | 83 | oveq2d 6666 |
. . . . . . . . . 10
|
85 | 84 | sumeq1d 14431 |
. . . . . . . . 9
|
86 | 85, 85 | jca 554 |
. . . . . . . 8
|
87 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
88 | | 1m1e0 11089 |
. . . . . . . . . . . . . 14
|
89 | 87, 88 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
90 | 89 | oveq2d 6666 |
. . . . . . . . . . . 12
|
91 | | fz10 12362 |
. . . . . . . . . . . 12
|
92 | 90, 91 | syl6eq 2672 |
. . . . . . . . . . 11
|
93 | 92 | sumeq1d 14431 |
. . . . . . . . . 10
|
94 | | sum0 14452 |
. . . . . . . . . 10
|
95 | 93, 94 | syl6eq 2672 |
. . . . . . . . 9
|
96 | 95, 95 | jca 554 |
. . . . . . . 8
|
97 | | oveq1 6657 |
. . . . . . . . . . 11
|
98 | 97 | oveq2d 6666 |
. . . . . . . . . 10
|
99 | 98 | sumeq1d 14431 |
. . . . . . . . 9
|
100 | 99, 99 | jca 554 |
. . . . . . . 8
|
101 | | peano2nn 11032 |
. . . . . . . . 9
|
102 | 101, 5 | syl6eleq 2711 |
. . . . . . . 8
|
103 | | fzfid 12772 |
. . . . . . . . . 10
|
104 | | elfznn 12370 |
. . . . . . . . . . . 12
|
105 | 104 | adantl 482 |
. . . . . . . . . . 11
|
106 | 105 | nnrecred 11066 |
. . . . . . . . . 10
|
107 | 103, 106 | fsumrecl 14465 |
. . . . . . . . 9
|
108 | 107 | recnd 10068 |
. . . . . . . 8
|
109 | 82, 86, 96, 100, 102, 108, 108 | fsumparts 14538 |
. . . . . . 7
..^
..^
|
110 | | nnz 11399 |
. . . . . . . . . 10
|
111 | | fzval3 12536 |
. . . . . . . . . 10
..^ |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
..^ |
113 | 112 | eqcomd 2628 |
. . . . . . . 8
..^ |
114 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
|
115 | 39, 40, 114 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
117 | 116 | sumeq1d 14431 |
. . . . . . . . . . . . 13
|
118 | 28 | recnd 10068 |
. . . . . . . . . . . . . 14
|
119 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
120 | 4, 118, 119 | fsumm1 14480 |
. . . . . . . . . . . . 13
|
121 | 117, 120 | eqtrd 2656 |
. . . . . . . . . . . 12
|
122 | 121 | oveq1d 6665 |
. . . . . . . . . . 11
|
123 | 36 | recnd 10068 |
. . . . . . . . . . . 12
|
124 | 6 | nnrecred 11066 |
. . . . . . . . . . . . 13
|
125 | 124 | recnd 10068 |
. . . . . . . . . . . 12
|
126 | 123, 125 | pncan2d 10394 |
. . . . . . . . . . 11
|
127 | 122, 126 | eqtrd 2656 |
. . . . . . . . . 10
|
128 | 127 | oveq2d 6666 |
. . . . . . . . 9
|
129 | 6 | nnne0d 11065 |
. . . . . . . . . 10
|
130 | 123, 39, 129 | divrecd 10804 |
. . . . . . . . 9
|
131 | 128, 130 | eqtr4d 2659 |
. . . . . . . 8
|
132 | 113, 131 | sumeq12rdv 14438 |
. . . . . . 7
..^
|
133 | | nncn 11028 |
. . . . . . . . . . . . . . 15
|
134 | | pncan 10287 |
. . . . . . . . . . . . . . 15
|
135 | 133, 40, 134 | sylancl 694 |
. . . . . . . . . . . . . 14
|
136 | 135 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
137 | 136 | sumeq1d 14431 |
. . . . . . . . . . . 12
|
138 | 137, 137 | oveq12d 6668 |
. . . . . . . . . . 11
|
139 | 16 | recnd 10068 |
. . . . . . . . . . . 12
|
140 | 139 | sqvald 13005 |
. . . . . . . . . . 11
|
141 | 138, 140 | eqtr4d 2659 |
. . . . . . . . . 10
|
142 | | 0cn 10032 |
. . . . . . . . . . . 12
|
143 | 142 | mul01i 10226 |
. . . . . . . . . . 11
|
144 | 143 | a1i 11 |
. . . . . . . . . 10
|
145 | 141, 144 | oveq12d 6668 |
. . . . . . . . 9
|
146 | 139 | sqcld 13006 |
. . . . . . . . . 10
|
147 | 146 | subid1d 10381 |
. . . . . . . . 9
|
148 | 145, 147 | eqtrd 2656 |
. . . . . . . 8
|
149 | 127, 117 | oveq12d 6668 |
. . . . . . . . . 10
|
150 | 29 | recnd 10068 |
. . . . . . . . . . 11
|
151 | 150, 39, 129 | divrec2d 10805 |
. . . . . . . . . 10
|
152 | 149, 151 | eqtr4d 2659 |
. . . . . . . . 9
|
153 | 113, 152 | sumeq12rdv 14438 |
. . . . . . . 8
..^
|
154 | 148, 153 | oveq12d 6668 |
. . . . . . 7
..^ |
155 | 109, 132,
154 | 3eqtr3rd 2665 |
. . . . . 6
|
156 | 31 | recnd 10068 |
. . . . . . 7
|
157 | 38 | recnd 10068 |
. . . . . . 7
|
158 | 146, 156,
157 | subaddd 10410 |
. . . . . 6
|
159 | 155, 158 | mpbid 222 |
. . . . 5
|
160 | 78, 159 | breqtrd 4679 |
. . . 4
|
161 | 24, 160 | eqbrtrd 4675 |
. . 3
|
162 | | flid 12609 |
. . . . . . . 8
|
163 | 110, 162 | syl 17 |
. . . . . . 7
|
164 | 163 | oveq2d 6666 |
. . . . . 6
|
165 | 164 | sumeq1d 14431 |
. . . . 5
|
166 | | nnre 11027 |
. . . . . 6
|
167 | | nnge1 11046 |
. . . . . 6
|
168 | | harmonicubnd 24736 |
. . . . . 6
|
169 | 166, 167,
168 | syl2anc 693 |
. . . . 5
|
170 | 165, 169 | eqbrtrrd 4677 |
. . . 4
|
171 | 14 | nnrpd 11870 |
. . . . . . . 8
|
172 | 171 | rpreccld 11882 |
. . . . . . 7
|
173 | 172 | rpge0d 11876 |
. . . . . 6
|
174 | 2, 15, 173 | fsumge0 14527 |
. . . . 5
|
175 | 49 | a1i 11 |
. . . . . 6
|
176 | | log1 24332 |
. . . . . . 7
|
177 | | 1rp 11836 |
. . . . . . . . 9
|
178 | | logleb 24349 |
. . . . . . . . 9
|
179 | 177, 18, 178 | sylancr 695 |
. . . . . . . 8
|
180 | 167, 179 | mpbid 222 |
. . . . . . 7
|
181 | 176, 180 | syl5eqbrr 4689 |
. . . . . 6
|
182 | 19 | lep1d 10955 |
. . . . . 6
|
183 | 175, 19, 21, 181, 182 | letrd 10194 |
. . . . 5
|
184 | 16, 21, 174, 183 | le2sqd 13044 |
. . . 4
|
185 | 170, 184 | mpbid 222 |
. . 3
|
186 | 12, 17, 22, 161, 185 | letrd 10194 |
. 2
|
187 | 1 | a1i 11 |
. . 3
|
188 | | 2pos 11112 |
. . . 4
|
189 | 188 | a1i 11 |
. . 3
|
190 | | lemuldiv2 10904 |
. . 3
|
191 | 10, 22, 187, 189, 190 | syl112anc 1330 |
. 2
|
192 | 186, 191 | mpbid 222 |
1
|