Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
|
2 | | mulog2sumlem1.2 |
. . . . . . . . 9
|
3 | | elfznn 12370 |
. . . . . . . . . 10
|
4 | 3 | nnrpd 11870 |
. . . . . . . . 9
|
5 | | rpdivcl 11856 |
. . . . . . . . 9
|
6 | 2, 4, 5 | syl2an 494 |
. . . . . . . 8
|
7 | 6 | relogcld 24369 |
. . . . . . 7
|
8 | 3 | adantl 482 |
. . . . . . 7
|
9 | 7, 8 | nndivred 11069 |
. . . . . 6
|
10 | 1, 9 | fsumrecl 14465 |
. . . . 5
|
11 | 2 | relogcld 24369 |
. . . . . . . 8
|
12 | 11 | resqcld 13035 |
. . . . . . 7
|
13 | 12 | rehalfcld 11279 |
. . . . . 6
|
14 | | emre 24732 |
. . . . . . . 8
|
15 | | remulcl 10021 |
. . . . . . . 8
|
16 | 14, 11, 15 | sylancr 695 |
. . . . . . 7
|
17 | | rpsup 12665 |
. . . . . . . . 9
|
18 | 17 | a1i 11 |
. . . . . . . 8
|
19 | | logdivsum.1 |
. . . . . . . . . . . . 13
|
20 | 19 | logdivsum 25222 |
. . . . . . . . . . . 12
|
21 | 20 | simp1i 1070 |
. . . . . . . . . . 11
|
22 | 21 | a1i 11 |
. . . . . . . . . 10
|
23 | 22 | feqmptd 6249 |
. . . . . . . . 9
|
24 | | mulog2sumlem.1 |
. . . . . . . . 9
|
25 | 23, 24 | eqbrtrrd 4677 |
. . . . . . . 8
|
26 | 21 | ffvelrni 6358 |
. . . . . . . . 9
|
27 | 26 | adantl 482 |
. . . . . . . 8
|
28 | 18, 25, 27 | rlimrecl 14311 |
. . . . . . 7
|
29 | 16, 28 | resubcld 10458 |
. . . . . 6
|
30 | 13, 29 | readdcld 10069 |
. . . . 5
|
31 | 10, 30 | resubcld 10458 |
. . . 4
|
32 | 31 | recnd 10068 |
. . 3
|
33 | 32 | abscld 14175 |
. 2
|
34 | | rerpdivcl 11861 |
. . . . . . . 8
|
35 | 11, 4, 34 | syl2an 494 |
. . . . . . 7
|
36 | 35 | recnd 10068 |
. . . . . 6
|
37 | 1, 36 | fsumcl 14464 |
. . . . 5
|
38 | 11 | recnd 10068 |
. . . . . 6
|
39 | | readdcl 10019 |
. . . . . . . 8
|
40 | 11, 14, 39 | sylancl 694 |
. . . . . . 7
|
41 | 40 | recnd 10068 |
. . . . . 6
|
42 | 38, 41 | mulcld 10060 |
. . . . 5
|
43 | 37, 42 | subcld 10392 |
. . . 4
|
44 | 43 | abscld 14175 |
. . 3
|
45 | 8 | nnrpd 11870 |
. . . . . . . . 9
|
46 | 45 | relogcld 24369 |
. . . . . . . 8
|
47 | 46, 8 | nndivred 11069 |
. . . . . . 7
|
48 | 47 | recnd 10068 |
. . . . . 6
|
49 | 1, 48 | fsumcl 14464 |
. . . . 5
|
50 | 13 | recnd 10068 |
. . . . . 6
|
51 | 28 | recnd 10068 |
. . . . . 6
|
52 | 50, 51 | addcld 10059 |
. . . . 5
|
53 | 49, 52 | subcld 10392 |
. . . 4
|
54 | 53 | abscld 14175 |
. . 3
|
55 | 44, 54 | readdcld 10069 |
. 2
|
56 | | 2re 11090 |
. . 3
|
57 | 11, 2 | rerpdivcld 11903 |
. . 3
|
58 | | remulcl 10021 |
. . 3
|
59 | 56, 57, 58 | sylancr 695 |
. 2
|
60 | | relogdiv 24339 |
. . . . . . . . . . 11
|
61 | 2, 4, 60 | syl2an 494 |
. . . . . . . . . 10
|
62 | 61 | oveq1d 6665 |
. . . . . . . . 9
|
63 | 38 | adantr 481 |
. . . . . . . . . 10
|
64 | 46 | recnd 10068 |
. . . . . . . . . 10
|
65 | 45 | rpcnne0d 11881 |
. . . . . . . . . 10
|
66 | | divsubdir 10721 |
. . . . . . . . . 10
|
67 | 63, 64, 65, 66 | syl3anc 1326 |
. . . . . . . . 9
|
68 | 62, 67 | eqtrd 2656 |
. . . . . . . 8
|
69 | 68 | sumeq2dv 14433 |
. . . . . . 7
|
70 | 1, 36, 48 | fsumsub 14520 |
. . . . . . 7
|
71 | 69, 70 | eqtrd 2656 |
. . . . . 6
|
72 | | remulcl 10021 |
. . . . . . . . . . . . 13
|
73 | 11, 14, 72 | sylancl 694 |
. . . . . . . . . . . 12
|
74 | 13, 73 | readdcld 10069 |
. . . . . . . . . . 11
|
75 | 74 | recnd 10068 |
. . . . . . . . . 10
|
76 | 75, 50 | pncand 10393 |
. . . . . . . . 9
|
77 | 14 | recni 10052 |
. . . . . . . . . . . . 13
|
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
|
79 | 38, 38, 78 | adddid 10064 |
. . . . . . . . . . 11
|
80 | 12 | recnd 10068 |
. . . . . . . . . . . . . 14
|
81 | 80 | 2halvesd 11278 |
. . . . . . . . . . . . 13
|
82 | 38 | sqvald 13005 |
. . . . . . . . . . . . 13
|
83 | 81, 82 | eqtrd 2656 |
. . . . . . . . . . . 12
|
84 | 83 | oveq1d 6665 |
. . . . . . . . . . 11
|
85 | 73 | recnd 10068 |
. . . . . . . . . . . 12
|
86 | 50, 50, 85 | add32d 10263 |
. . . . . . . . . . 11
|
87 | 79, 84, 86 | 3eqtr2d 2662 |
. . . . . . . . . 10
|
88 | 87 | oveq1d 6665 |
. . . . . . . . 9
|
89 | | mulcom 10022 |
. . . . . . . . . . 11
|
90 | 77, 38, 89 | sylancr 695 |
. . . . . . . . . 10
|
91 | 90 | oveq2d 6666 |
. . . . . . . . 9
|
92 | 76, 88, 91 | 3eqtr4rd 2667 |
. . . . . . . 8
|
93 | 92 | oveq1d 6665 |
. . . . . . 7
|
94 | 90, 85 | eqeltrd 2701 |
. . . . . . . 8
|
95 | 50, 94, 51 | addsubassd 10412 |
. . . . . . 7
|
96 | 42, 50, 51 | subsub4d 10423 |
. . . . . . 7
|
97 | 93, 95, 96 | 3eqtr3d 2664 |
. . . . . 6
|
98 | 71, 97 | oveq12d 6668 |
. . . . 5
|
99 | 37, 49, 42, 52 | sub4d 10441 |
. . . . 5
|
100 | 98, 99 | eqtrd 2656 |
. . . 4
|
101 | 100 | fveq2d 6195 |
. . 3
|
102 | 43, 53 | abs2dif2d 14197 |
. . 3
|
103 | 101, 102 | eqbrtrd 4675 |
. 2
|
104 | | harmonicbnd4 24737 |
. . . . . . 7
|
105 | 2, 104 | syl 17 |
. . . . . 6
|
106 | 8 | nnrecred 11066 |
. . . . . . . . . . 11
|
107 | 1, 106 | fsumrecl 14465 |
. . . . . . . . . 10
|
108 | 107, 40 | resubcld 10458 |
. . . . . . . . 9
|
109 | 108 | recnd 10068 |
. . . . . . . 8
|
110 | 109 | abscld 14175 |
. . . . . . 7
|
111 | 2 | rprecred 11883 |
. . . . . . 7
|
112 | | 0red 10041 |
. . . . . . . 8
|
113 | | 1red 10055 |
. . . . . . . 8
|
114 | | 0lt1 10550 |
. . . . . . . . 9
|
115 | 114 | a1i 11 |
. . . . . . . 8
|
116 | | loge 24333 |
. . . . . . . . 9
|
117 | | mulog2sumlem1.3 |
. . . . . . . . . 10
|
118 | | epr 14936 |
. . . . . . . . . . 11
|
119 | | logleb 24349 |
. . . . . . . . . . 11
|
120 | 118, 2, 119 | sylancr 695 |
. . . . . . . . . 10
|
121 | 117, 120 | mpbid 222 |
. . . . . . . . 9
|
122 | 116, 121 | syl5eqbrr 4689 |
. . . . . . . 8
|
123 | 112, 113,
11, 115, 122 | ltletrd 10197 |
. . . . . . 7
|
124 | | lemul2 10876 |
. . . . . . 7
|
125 | 110, 111,
11, 123, 124 | syl112anc 1330 |
. . . . . 6
|
126 | 105, 125 | mpbid 222 |
. . . . 5
|
127 | 45 | rpcnd 11874 |
. . . . . . . . . . . 12
|
128 | 45 | rpne0d 11877 |
. . . . . . . . . . . 12
|
129 | 63, 127, 128 | divrecd 10804 |
. . . . . . . . . . 11
|
130 | 129 | sumeq2dv 14433 |
. . . . . . . . . 10
|
131 | 106 | recnd 10068 |
. . . . . . . . . . 11
|
132 | 1, 38, 131 | fsummulc2 14516 |
. . . . . . . . . 10
|
133 | 130, 132 | eqtr4d 2659 |
. . . . . . . . 9
|
134 | 133 | oveq1d 6665 |
. . . . . . . 8
|
135 | 1, 131 | fsumcl 14464 |
. . . . . . . . 9
|
136 | 38, 135, 41 | subdid 10486 |
. . . . . . . 8
|
137 | 134, 136 | eqtr4d 2659 |
. . . . . . 7
|
138 | 137 | fveq2d 6195 |
. . . . . 6
|
139 | 135, 41 | subcld 10392 |
. . . . . . 7
|
140 | 38, 139 | absmuld 14193 |
. . . . . 6
|
141 | 112, 11, 123 | ltled 10185 |
. . . . . . . 8
|
142 | 11, 141 | absidd 14161 |
. . . . . . 7
|
143 | 142 | oveq1d 6665 |
. . . . . 6
|
144 | 138, 140,
143 | 3eqtrd 2660 |
. . . . 5
|
145 | 2 | rpcnd 11874 |
. . . . . 6
|
146 | 2 | rpne0d 11877 |
. . . . . 6
|
147 | 38, 145, 146 | divrecd 10804 |
. . . . 5
|
148 | 126, 144,
147 | 3brtr4d 4685 |
. . . 4
|
149 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
150 | | id 22 |
. . . . . . . . . . . . . 14
|
151 | 149, 150 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
152 | 151 | cbvsumv 14426 |
. . . . . . . . . . . 12
|
153 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
154 | 153 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
155 | 154 | sumeq1d 14431 |
. . . . . . . . . . . 12
|
156 | 152, 155 | syl5eq 2668 |
. . . . . . . . . . 11
|
157 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
158 | 157 | oveq1d 6665 |
. . . . . . . . . . . 12
|
159 | 158 | oveq1d 6665 |
. . . . . . . . . . 11
|
160 | 156, 159 | oveq12d 6668 |
. . . . . . . . . 10
|
161 | | ovex 6678 |
. . . . . . . . . 10
|
162 | 160, 19, 161 | fvmpt 6282 |
. . . . . . . . 9
|
163 | 2, 162 | syl 17 |
. . . . . . . 8
|
164 | 163 | oveq1d 6665 |
. . . . . . 7
|
165 | 49, 50, 51 | subsub4d 10423 |
. . . . . . 7
|
166 | 164, 165 | eqtrd 2656 |
. . . . . 6
|
167 | 166 | fveq2d 6195 |
. . . . 5
|
168 | 20 | simp3i 1072 |
. . . . . 6
|
169 | 24, 2, 117, 168 | syl3anc 1326 |
. . . . 5
|
170 | 167, 169 | eqbrtrrd 4677 |
. . . 4
|
171 | 44, 54, 57, 57, 148, 170 | le2addd 10646 |
. . 3
|
172 | 57 | recnd 10068 |
. . . 4
|
173 | 172 | 2timesd 11275 |
. . 3
|
174 | 171, 173 | breqtrrd 4681 |
. 2
|
175 | 33, 55, 59, 103, 174 | letrd 10194 |
1
|