Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. 2
|
2 | | ioossre 12235 |
. . . 4
|
3 | | selberg3lem1.1 |
. . . . 5
|
4 | 3 | rpcnd 11874 |
. . . 4
|
5 | | o1const 14350 |
. . . 4
|
6 | 2, 4, 5 | sylancr 695 |
. . 3
|
7 | | fzfid 12772 |
. . . . . . 7
|
8 | | elfznn 12370 |
. . . . . . . . . 10
|
9 | 8 | adantl 482 |
. . . . . . . . 9
|
10 | | vmacl 24844 |
. . . . . . . . 9
Λ |
11 | 9, 10 | syl 17 |
. . . . . . . 8
Λ |
12 | 11, 9 | nndivred 11069 |
. . . . . . 7
Λ |
13 | 7, 12 | fsumrecl 14465 |
. . . . . 6
Λ |
14 | | elioore 12205 |
. . . . . . . . 9
|
15 | | eliooord 12233 |
. . . . . . . . . 10
|
16 | 15 | simpld 475 |
. . . . . . . . 9
|
17 | 14, 16 | rplogcld 24375 |
. . . . . . . 8
|
18 | | rpdivcl 11856 |
. . . . . . . 8
|
19 | 3, 17, 18 | syl2an 494 |
. . . . . . 7
|
20 | 19 | rpred 11872 |
. . . . . 6
|
21 | 13, 20 | remulcld 10070 |
. . . . 5
Λ |
22 | 21 | recnd 10068 |
. . . 4
Λ |
23 | 4 | adantr 481 |
. . . 4
|
24 | 13 | recnd 10068 |
. . . . . . . 8
Λ |
25 | 17 | adantl 482 |
. . . . . . . . 9
|
26 | 25 | rpcnd 11874 |
. . . . . . . 8
|
27 | 19 | rpcnd 11874 |
. . . . . . . 8
|
28 | 24, 26, 27 | subdird 10487 |
. . . . . . 7
Λ Λ |
29 | 25 | rpne0d 11877 |
. . . . . . . . 9
|
30 | 23, 26, 29 | divcan2d 10803 |
. . . . . . . 8
|
31 | 30 | oveq2d 6666 |
. . . . . . 7
Λ Λ |
32 | 28, 31 | eqtrd 2656 |
. . . . . 6
Λ Λ |
33 | 32 | mpteq2dva 4744 |
. . . . 5
Λ Λ |
34 | 25 | rpred 11872 |
. . . . . . 7
|
35 | 13, 34 | resubcld 10458 |
. . . . . 6
Λ |
36 | 14 | adantl 482 |
. . . . . . . . . 10
|
37 | | 0red 10041 |
. . . . . . . . . . 11
|
38 | | 1red 10055 |
. . . . . . . . . . 11
|
39 | | 0lt1 10550 |
. . . . . . . . . . . 12
|
40 | 39 | a1i 11 |
. . . . . . . . . . 11
|
41 | 16 | adantl 482 |
. . . . . . . . . . 11
|
42 | 37, 38, 36, 40, 41 | lttrd 10198 |
. . . . . . . . . 10
|
43 | 36, 42 | elrpd 11869 |
. . . . . . . . 9
|
44 | 43 | ex 450 |
. . . . . . . 8
|
45 | 44 | ssrdv 3609 |
. . . . . . 7
|
46 | | vmadivsum 25171 |
. . . . . . . 8
Λ |
47 | 46 | a1i 11 |
. . . . . . 7
Λ |
48 | 45, 47 | o1res2 14294 |
. . . . . 6
Λ |
49 | 2 | a1i 11 |
. . . . . . 7
|
50 | | ere 14819 |
. . . . . . . 8
|
51 | 50 | a1i 11 |
. . . . . . 7
|
52 | 3 | rpred 11872 |
. . . . . . 7
|
53 | 19 | adantrr 753 |
. . . . . . . . . 10
|
54 | 53 | rprege0d 11879 |
. . . . . . . . 9
|
55 | | absid 14036 |
. . . . . . . . 9
|
56 | 54, 55 | syl 17 |
. . . . . . . 8
|
57 | | loge 24333 |
. . . . . . . . . . 11
|
58 | | simprr 796 |
. . . . . . . . . . . 12
|
59 | | epr 14936 |
. . . . . . . . . . . . 13
|
60 | 43 | adantrr 753 |
. . . . . . . . . . . . 13
|
61 | | logleb 24349 |
. . . . . . . . . . . . 13
|
62 | 59, 60, 61 | sylancr 695 |
. . . . . . . . . . . 12
|
63 | 58, 62 | mpbid 222 |
. . . . . . . . . . 11
|
64 | 57, 63 | syl5eqbrr 4689 |
. . . . . . . . . 10
|
65 | | 1rp 11836 |
. . . . . . . . . . . 12
|
66 | | rpregt0 11846 |
. . . . . . . . . . . 12
|
67 | 65, 66 | mp1i 13 |
. . . . . . . . . . 11
|
68 | 25 | adantrr 753 |
. . . . . . . . . . . 12
|
69 | 68 | rpregt0d 11878 |
. . . . . . . . . . 11
|
70 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
71 | 70 | rpregt0d 11878 |
. . . . . . . . . . 11
|
72 | | lediv2 10913 |
. . . . . . . . . . 11
|
73 | 67, 69, 71, 72 | syl3anc 1326 |
. . . . . . . . . 10
|
74 | 64, 73 | mpbid 222 |
. . . . . . . . 9
|
75 | 4 | adantr 481 |
. . . . . . . . . 10
|
76 | 75 | div1d 10793 |
. . . . . . . . 9
|
77 | 74, 76 | breqtrd 4679 |
. . . . . . . 8
|
78 | 56, 77 | eqbrtrd 4675 |
. . . . . . 7
|
79 | 49, 27, 51, 52, 78 | elo1d 14267 |
. . . . . 6
|
80 | 35, 20, 48, 79 | o1mul2 14355 |
. . . . 5
Λ |
81 | 33, 80 | eqeltrrd 2702 |
. . . 4
Λ |
82 | 22, 23, 81 | o1dif 14360 |
. . 3
Λ |
83 | 6, 82 | mpbird 247 |
. 2
Λ |
84 | | 2re 11090 |
. . . . . . 7
|
85 | | rerpdivcl 11861 |
. . . . . . 7
|
86 | 84, 25, 85 | sylancr 695 |
. . . . . 6
|
87 | | nndivre 11056 |
. . . . . . . . . . 11
|
88 | 36, 8, 87 | syl2an 494 |
. . . . . . . . . 10
|
89 | | chpcl 24850 |
. . . . . . . . . 10
ψ |
90 | 88, 89 | syl 17 |
. . . . . . . . 9
ψ |
91 | 11, 90 | remulcld 10070 |
. . . . . . . 8
Λ ψ |
92 | 9 | nnrpd 11870 |
. . . . . . . . 9
|
93 | 92 | relogcld 24369 |
. . . . . . . 8
|
94 | 91, 93 | remulcld 10070 |
. . . . . . 7
Λ ψ |
95 | 7, 94 | fsumrecl 14465 |
. . . . . 6
Λ ψ
|
96 | 86, 95 | remulcld 10070 |
. . . . 5
Λ ψ
|
97 | 7, 91 | fsumrecl 14465 |
. . . . 5
Λ ψ
|
98 | 96, 97 | resubcld 10458 |
. . . 4
Λ ψ Λ ψ |
99 | 98, 43 | rerpdivcld 11903 |
. . 3
Λ ψ Λ ψ |
100 | 99 | recnd 10068 |
. 2
Λ ψ Λ ψ |
101 | 100 | abscld 14175 |
. . . 4
Λ ψ
Λ ψ |
102 | 22 | abscld 14175 |
. . . 4
Λ |
103 | | 2cnd 11093 |
. . . . . . . . . 10
|
104 | 95 | recnd 10068 |
. . . . . . . . . 10
Λ ψ
|
105 | 103, 104 | mulcld 10060 |
. . . . . . . . 9
Λ ψ
|
106 | 97 | recnd 10068 |
. . . . . . . . . 10
Λ ψ
|
107 | 106, 26 | mulcld 10060 |
. . . . . . . . 9
Λ ψ |
108 | 105, 107 | subcld 10392 |
. . . . . . . 8
Λ ψ Λ ψ
|
109 | 108 | abscld 14175 |
. . . . . . 7
Λ ψ
Λ ψ
|
110 | 42 | gt0ne0d 10592 |
. . . . . . 7
|
111 | 109, 36, 110 | redivcld 10853 |
. . . . . 6
Λ ψ Λ ψ
|
112 | 52 | adantr 481 |
. . . . . . 7
|
113 | 13, 112 | remulcld 10070 |
. . . . . 6
Λ |
114 | 11 | recnd 10068 |
. . . . . . . . . . . 12
Λ |
115 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
116 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . 18
|
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
118 | | vmacl 24844 |
. . . . . . . . . . . . . . . . 17
Λ |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
Λ |
120 | 117 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | relogcld 24369 |
. . . . . . . . . . . . . . . 16
|
122 | 119, 121 | remulcld 10070 |
. . . . . . . . . . . . . . 15
Λ |
123 | 115, 122 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
Λ |
124 | 8 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
|
125 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . 17
|
126 | 43, 124, 125 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
127 | 126 | relogcld 24369 |
. . . . . . . . . . . . . . 15
|
128 | 90, 127 | remulcld 10070 |
. . . . . . . . . . . . . 14
ψ |
129 | 123, 128 | resubcld 10458 |
. . . . . . . . . . . . 13
Λ ψ
|
130 | 129 | recnd 10068 |
. . . . . . . . . . . 12
Λ ψ
|
131 | 114, 130 | mulcld 10060 |
. . . . . . . . . . 11
Λ
Λ ψ |
132 | 7, 131 | fsumcl 14464 |
. . . . . . . . . 10
Λ Λ ψ
|
133 | 132 | abscld 14175 |
. . . . . . . . 9
Λ Λ ψ
|
134 | 131 | abscld 14175 |
. . . . . . . . . 10
Λ Λ ψ
|
135 | 7, 134 | fsumrecl 14465 |
. . . . . . . . 9
Λ Λ ψ |
136 | 112, 36 | remulcld 10070 |
. . . . . . . . . 10
|
137 | 13, 136 | remulcld 10070 |
. . . . . . . . 9
Λ
|
138 | 7, 131 | fsumabs 14533 |
. . . . . . . . 9
Λ Λ ψ
Λ
Λ ψ |
139 | 52 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
140 | 36 | adantr 481 |
. . . . . . . . . . . . 13
|
141 | 139, 140 | remulcld 10070 |
. . . . . . . . . . . 12
|
142 | 12, 141 | remulcld 10070 |
. . . . . . . . . . 11
Λ
|
143 | 130 | abscld 14175 |
. . . . . . . . . . . . 13
Λ ψ |
144 | 141, 9 | nndivred 11069 |
. . . . . . . . . . . . 13
|
145 | | vmage0 24847 |
. . . . . . . . . . . . . 14
Λ |
146 | 9, 145 | syl 17 |
. . . . . . . . . . . . 13
Λ |
147 | 88 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
148 | 126 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . 18
|
149 | 130, 147,
148 | absdivd 14194 |
. . . . . . . . . . . . . . . . 17
Λ ψ
Λ ψ |
150 | 126 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . 19
|
151 | 88, 150 | absidd 14161 |
. . . . . . . . . . . . . . . . . 18
|
152 | 151 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
Λ ψ
Λ ψ |
153 | 149, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
Λ ψ
Λ ψ |
154 | 9 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 154 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | 36, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
158 | 157 | simplbda 654 |
. . . . . . . . . . . . . . . . . . . 20
|
159 | 155, 158 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . 19
|
160 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 160, 140,
92 | lemuldivd 11921 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 159, 161 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
163 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
|
164 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
|
166 | 88, 162, 165 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
|
167 | | selberg3lem1.2 |
. . . . . . . . . . . . . . . . . 18
Λ ψ |
168 | 167 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
Λ ψ |
169 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Λ Λ |
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
171 | 169, 170 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Λ Λ |
172 | 171 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . . . . . 23
Λ
Λ |
173 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
174 | 173 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
175 | 174 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . . . . . 23
Λ
Λ |
176 | 172, 175 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
Λ
Λ |
177 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
ψ ψ |
178 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
179 | 177, 178 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
ψ ψ |
180 | 176, 179 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
Λ ψ Λ ψ |
181 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
182 | 180, 181 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
Λ ψ Λ ψ |
183 | 182 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
Λ ψ Λ ψ |
184 | 183 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
Λ ψ Λ ψ |
185 | 184 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
Λ ψ Λ ψ |
186 | 166, 168,
185 | sylc 65 |
. . . . . . . . . . . . . . . 16
Λ ψ |
187 | 153, 186 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
Λ ψ |
188 | 143, 139,
126 | ledivmul2d 11926 |
. . . . . . . . . . . . . . 15
Λ ψ
Λ ψ
|
189 | 187, 188 | mpbid 222 |
. . . . . . . . . . . . . 14
Λ ψ
|
190 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
|
191 | 140 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
192 | 9 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
|
193 | 190, 191,
154, 192 | divassd 10836 |
. . . . . . . . . . . . . 14
|
194 | 189, 193 | breqtrrd 4681 |
. . . . . . . . . . . . 13
Λ ψ |
195 | 143, 144,
11, 146, 194 | lemul2ad 10964 |
. . . . . . . . . . . 12
Λ Λ ψ
Λ |
196 | 114, 130 | absmuld 14193 |
. . . . . . . . . . . . 13
Λ Λ ψ
Λ
Λ ψ |
197 | 11, 146 | absidd 14161 |
. . . . . . . . . . . . . 14
Λ Λ |
198 | 197 | oveq1d 6665 |
. . . . . . . . . . . . 13
Λ Λ ψ Λ Λ ψ |
199 | 196, 198 | eqtrd 2656 |
. . . . . . . . . . . 12
Λ Λ ψ
Λ Λ ψ |
200 | 141 | recnd 10068 |
. . . . . . . . . . . . 13
|
201 | 114, 154,
200, 192 | div32d 10824 |
. . . . . . . . . . . 12
Λ
Λ |
202 | 195, 199,
201 | 3brtr4d 4685 |
. . . . . . . . . . 11
Λ Λ ψ
Λ |
203 | 7, 134, 142, 202 | fsumle 14531 |
. . . . . . . . . 10
Λ Λ ψ
Λ |
204 | 36 | recnd 10068 |
. . . . . . . . . . . 12
|
205 | 23, 204 | mulcld 10060 |
. . . . . . . . . . 11
|
206 | 114, 154,
192 | divcld 10801 |
. . . . . . . . . . 11
Λ |
207 | 7, 205, 206 | fsummulc1 14517 |
. . . . . . . . . 10
Λ
Λ |
208 | 203, 207 | breqtrrd 4681 |
. . . . . . . . 9
Λ Λ ψ
Λ |
209 | 133, 135,
137, 138, 208 | letrd 10194 |
. . . . . . . 8
Λ Λ ψ
Λ |
210 | 123 | recnd 10068 |
. . . . . . . . . . . . 13
Λ |
211 | 90 | recnd 10068 |
. . . . . . . . . . . . . 14
ψ |
212 | 93 | recnd 10068 |
. . . . . . . . . . . . . 14
|
213 | 211, 212 | mulcld 10060 |
. . . . . . . . . . . . 13
ψ |
214 | 210, 213 | addcld 10059 |
. . . . . . . . . . . 12
Λ ψ
|
215 | 114, 214 | mulcld 10060 |
. . . . . . . . . . 11
Λ
Λ ψ |
216 | 114, 211 | mulcld 10060 |
. . . . . . . . . . . 12
Λ ψ |
217 | 26 | adantr 481 |
. . . . . . . . . . . 12
|
218 | 216, 217 | mulcld 10060 |
. . . . . . . . . . 11
Λ ψ |
219 | 7, 215, 218 | fsumsub 14520 |
. . . . . . . . . 10
Λ Λ ψ
Λ ψ Λ Λ ψ
Λ ψ |
220 | 211, 217 | mulcld 10060 |
. . . . . . . . . . . . 13
ψ |
221 | 114, 214,
220 | subdid 10486 |
. . . . . . . . . . . 12
Λ Λ ψ ψ
Λ Λ ψ
Λ ψ |
222 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
223 | 222, 92 | relogdivd 24372 |
. . . . . . . . . . . . . . . . 17
|
224 | 223 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
ψ ψ
|
225 | 211, 217,
212 | subdid 10486 |
. . . . . . . . . . . . . . . 16
ψ ψ ψ
|
226 | 224, 225 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
ψ ψ ψ
|
227 | 226 | oveq2d 6666 |
. . . . . . . . . . . . . 14
Λ ψ
Λ ψ ψ
|
228 | 210, 220,
213 | subsub3d 10422 |
. . . . . . . . . . . . . 14
Λ ψ ψ
Λ ψ ψ
|
229 | 227, 228 | eqtrd 2656 |
. . . . . . . . . . . . 13
Λ ψ
Λ ψ ψ |
230 | 229 | oveq2d 6666 |
. . . . . . . . . . . 12
Λ
Λ ψ Λ
Λ ψ ψ |
231 | 114, 211,
217 | mulassd 10063 |
. . . . . . . . . . . . 13
Λ ψ Λ ψ |
232 | 231 | oveq2d 6666 |
. . . . . . . . . . . 12
Λ Λ ψ Λ ψ Λ Λ ψ
Λ ψ |
233 | 221, 230,
232 | 3eqtr4d 2666 |
. . . . . . . . . . 11
Λ
Λ ψ Λ
Λ ψ Λ ψ |
234 | 233 | sumeq2dv 14433 |
. . . . . . . . . 10
Λ Λ ψ
Λ Λ ψ Λ ψ |
235 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
Λ Λ |
236 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
237 | 236 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
ψ ψ |
238 | 235, 237 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
Λ ψ Λ ψ
|
239 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
240 | 238, 239 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
Λ ψ Λ ψ
|
241 | 240 | cbvsumv 14426 |
. . . . . . . . . . . . . . 15
Λ ψ
Λ ψ |
242 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . 22
|
243 | 242 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
244 | 243, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
Λ |
245 | 244 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
Λ |
246 | 245 | anasss 679 |
. . . . . . . . . . . . . . . . . 18
Λ |
247 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
248 | 247 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
249 | 248, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
Λ |
250 | 249 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
Λ |
251 | 248 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . 22
|
252 | 251 | relogcld 24369 |
. . . . . . . . . . . . . . . . . . . . 21
|
253 | 252 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
254 | 250, 253 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
Λ |
255 | 254 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
Λ |
256 | 246, 255 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
Λ Λ |
257 | 36, 256 | fsumfldivdiag 24916 |
. . . . . . . . . . . . . . . 16
Λ Λ
Λ Λ |
258 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
259 | 258, 248 | nndivred 11069 |
. . . . . . . . . . . . . . . . . . . . 21
|
260 | | chpcl 24850 |
. . . . . . . . . . . . . . . . . . . . 21
ψ |
261 | 259, 260 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ψ |
262 | 261 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
ψ |
263 | 250, 262,
253 | mul32d 10246 |
. . . . . . . . . . . . . . . . . 18
Λ ψ Λ ψ |
264 | 249, 252 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
Λ |
265 | 264 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
Λ |
266 | 265, 262 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
Λ ψ ψ Λ |
267 | | chpval 24848 |
. . . . . . . . . . . . . . . . . . . . 21
ψ Λ |
268 | 259, 267 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
ψ Λ |
269 | 268 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
ψ Λ Λ Λ |
270 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . 20
|
271 | 270, 265,
245 | fsummulc1 14517 |
. . . . . . . . . . . . . . . . . . 19
Λ Λ Λ Λ |
272 | 269, 271 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
ψ Λ
Λ Λ |
273 | 263, 266,
272 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
Λ ψ Λ Λ |
274 | 273 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
Λ ψ
Λ Λ |
275 | 122 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
Λ |
276 | 115, 114,
275 | fsummulc2 14516 |
. . . . . . . . . . . . . . . . 17
Λ Λ Λ Λ |
277 | 276 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
Λ Λ
Λ Λ |
278 | 257, 274,
277 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
Λ ψ
Λ Λ |
279 | 241, 278 | syl5eq 2668 |
. . . . . . . . . . . . . 14
Λ ψ
Λ Λ |
280 | 114, 211,
212 | mulassd 10063 |
. . . . . . . . . . . . . . 15
Λ ψ Λ ψ |
281 | 280 | sumeq2dv 14433 |
. . . . . . . . . . . . . 14
Λ ψ
Λ ψ |
282 | 279, 281 | oveq12d 6668 |
. . . . . . . . . . . . 13
Λ ψ
Λ ψ Λ Λ Λ ψ |
283 | 104 | 2timesd 11275 |
. . . . . . . . . . . . 13
Λ ψ
Λ ψ
Λ ψ |
284 | 114, 210 | mulcld 10060 |
. . . . . . . . . . . . . 14
Λ Λ |
285 | 114, 213 | mulcld 10060 |
. . . . . . . . . . . . . 14
Λ ψ |
286 | 7, 284, 285 | fsumadd 14470 |
. . . . . . . . . . . . 13
Λ Λ Λ ψ
Λ Λ Λ ψ |
287 | 282, 283,
286 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
Λ ψ
Λ Λ Λ ψ |
288 | 114, 210,
213 | adddid 10064 |
. . . . . . . . . . . . 13
Λ
Λ ψ Λ Λ Λ ψ |
289 | 288 | sumeq2dv 14433 |
. . . . . . . . . . . 12
Λ Λ ψ
Λ Λ Λ ψ |
290 | 287, 289 | eqtr4d 2659 |
. . . . . . . . . . 11
Λ ψ
Λ Λ ψ |
291 | 91 | recnd 10068 |
. . . . . . . . . . . 12
Λ ψ |
292 | 7, 26, 291 | fsummulc1 14517 |
. . . . . . . . . . 11
Λ ψ Λ ψ |
293 | 290, 292 | oveq12d 6668 |
. . . . . . . . . 10
Λ ψ Λ ψ
Λ Λ ψ
Λ ψ |
294 | 219, 234,
293 | 3eqtr4rd 2667 |
. . . . . . . . 9
Λ ψ Λ ψ
Λ Λ ψ |
295 | 294 | fveq2d 6195 |
. . . . . . . 8
Λ ψ
Λ ψ
Λ
Λ ψ |
296 | 24, 23, 204 | mulassd 10063 |
. . . . . . . 8
Λ
Λ
|
297 | 209, 295,
296 | 3brtr4d 4685 |
. . . . . . 7
Λ ψ
Λ ψ
Λ |
298 | 109, 113,
43 | ledivmul2d 11926 |
. . . . . . 7
Λ ψ Λ ψ
Λ
Λ ψ
Λ ψ
Λ |
299 | 297, 298 | mpbird 247 |
. . . . . 6
Λ ψ Λ ψ
Λ |
300 | 111, 113,
25, 299 | lediv1dd 11930 |
. . . . 5
Λ ψ Λ ψ
Λ |
301 | 109 | recnd 10068 |
. . . . . . 7
Λ ψ
Λ ψ
|
302 | 301, 204,
26, 110, 29 | divdiv1d 10832 |
. . . . . 6
Λ ψ Λ ψ
Λ ψ Λ ψ
|
303 | 108, 26, 204, 29, 110 | divdiv32d 10826 |
. . . . . . . . 9
Λ ψ
Λ ψ
Λ ψ
Λ ψ
|
304 | 105, 107,
26, 29 | divsubdird 10840 |
. . . . . . . . . . 11
Λ ψ
Λ ψ
Λ ψ
Λ ψ
|
305 | 103, 104,
26, 29 | div23d 10838 |
. . . . . . . . . . . 12
Λ ψ Λ ψ
|
306 | 106, 26, 29 | divcan4d 10807 |
. . . . . . . . . . . 12
Λ ψ
Λ ψ
|
307 | 305, 306 | oveq12d 6668 |
. . . . . . . . . . 11
Λ ψ
Λ ψ
Λ ψ
Λ ψ |
308 | 304, 307 | eqtrd 2656 |
. . . . . . . . . 10
Λ ψ
Λ ψ
Λ ψ Λ ψ |
309 | 308 | oveq1d 6665 |
. . . . . . . . 9
Λ ψ
Λ ψ
Λ ψ Λ ψ |
310 | 108, 204,
26, 110, 29 | divdiv1d 10832 |
. . . . . . . . 9
Λ ψ
Λ ψ
Λ ψ
Λ ψ
|
311 | 303, 309,
310 | 3eqtr3d 2664 |
. . . . . . . 8
Λ ψ Λ ψ Λ ψ
Λ ψ
|
312 | 311 | fveq2d 6195 |
. . . . . . 7
Λ ψ
Λ ψ Λ ψ
Λ ψ
|
313 | 43, 25 | rpmulcld 11888 |
. . . . . . . . 9
|
314 | 313 | rpcnd 11874 |
. . . . . . . 8
|
315 | 313 | rpne0d 11877 |
. . . . . . . 8
|
316 | 108, 314,
315 | absdivd 14194 |
. . . . . . 7
Λ ψ
Λ ψ
Λ ψ Λ ψ
|
317 | 313 | rpred 11872 |
. . . . . . . . 9
|
318 | 313 | rpge0d 11876 |
. . . . . . . . 9
|
319 | 317, 318 | absidd 14161 |
. . . . . . . 8
|
320 | 319 | oveq2d 6666 |
. . . . . . 7
Λ ψ Λ ψ
Λ ψ
Λ ψ
|
321 | 312, 316,
320 | 3eqtrd 2660 |
. . . . . 6
Λ ψ
Λ ψ Λ ψ
Λ ψ
|
322 | 302, 321 | eqtr4d 2659 |
. . . . 5
Λ ψ Λ ψ
Λ ψ Λ ψ |
323 | 24, 23, 26, 29 | divassd 10836 |
. . . . 5
Λ
Λ |
324 | 300, 322,
323 | 3brtr3d 4684 |
. . . 4
Λ ψ
Λ ψ
Λ |
325 | 21 | leabsd 14153 |
. . . 4
Λ Λ |
326 | 101, 21, 102, 324, 325 | letrd 10194 |
. . 3
Λ ψ
Λ ψ
Λ |
327 | 326 | adantrr 753 |
. 2
Λ ψ
Λ ψ
Λ |
328 | 1, 83, 21, 100, 327 | o1le 14383 |
1
Λ ψ
Λ ψ |