Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . 4
|
2 | | simpl 473 |
. . . . 5
|
3 | | elfznn 12370 |
. . . . 5
|
4 | | rpvmasum2.g |
. . . . . . 7
DChr |
5 | | rpvmasum.z |
. . . . . . 7
ℤ/nℤ |
6 | | rpvmasum2.d |
. . . . . . 7
|
7 | | rpvmasum.l |
. . . . . . 7
RHom |
8 | | rpvmasum2.w |
. . . . . . . . . . 11
|
9 | | ssrab2 3687 |
. . . . . . . . . . 11
|
10 | 8, 9 | eqsstri 3635 |
. . . . . . . . . 10
|
11 | | dchrisum0.b |
. . . . . . . . . 10
|
12 | 10, 11 | sseldi 3601 |
. . . . . . . . 9
|
13 | 12 | eldifad 3586 |
. . . . . . . 8
|
14 | 13 | adantr 481 |
. . . . . . 7
|
15 | | nnz 11399 |
. . . . . . . 8
|
16 | 15 | adantl 482 |
. . . . . . 7
|
17 | 4, 5, 6, 7, 14, 16 | dchrzrhcl 24970 |
. . . . . 6
|
18 | | nnrp 11842 |
. . . . . . . . 9
|
19 | 18 | adantl 482 |
. . . . . . . 8
|
20 | 19 | rpsqrtcld 14150 |
. . . . . . 7
|
21 | 20 | rpcnd 11874 |
. . . . . 6
|
22 | 20 | rpne0d 11877 |
. . . . . 6
|
23 | 17, 21, 22 | divcld 10801 |
. . . . 5
|
24 | 2, 3, 23 | syl2an 494 |
. . . 4
|
25 | 1, 24 | fsumcl 14464 |
. . 3
|
26 | | dchrisum0lem2.u |
. . . . 5
|
27 | | rlimcl 14234 |
. . . . 5
|
28 | 26, 27 | syl 17 |
. . . 4
|
29 | 28 | adantr 481 |
. . 3
|
30 | | 0xr 10086 |
. . . . . . . . 9
|
31 | | 0lt1 10550 |
. . . . . . . . 9
|
32 | | df-ioo 12179 |
. . . . . . . . . 10
|
33 | | df-ico 12181 |
. . . . . . . . . 10
|
34 | | xrltletr 11988 |
. . . . . . . . . 10
|
35 | 32, 33, 34 | ixxss1 12193 |
. . . . . . . . 9
|
36 | 30, 31, 35 | mp2an 708 |
. . . . . . . 8
|
37 | | ioorp 12251 |
. . . . . . . 8
|
38 | 36, 37 | sseqtri 3637 |
. . . . . . 7
|
39 | | resmpt 5449 |
. . . . . . 7
|
40 | 38, 39 | ax-mp 5 |
. . . . . 6
|
41 | 38 | sseli 3599 |
. . . . . . . . 9
|
42 | 3 | adantl 482 |
. . . . . . . . . 10
|
43 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
44 | 43 | fveq2d 6195 |
. . . . . . . . . . . 12
|
45 | | fveq2 6191 |
. . . . . . . . . . . 12
|
46 | 44, 45 | oveq12d 6668 |
. . . . . . . . . . 11
|
47 | | dchrisum0lem1.f |
. . . . . . . . . . 11
|
48 | | ovex 6678 |
. . . . . . . . . . 11
|
49 | 46, 47, 48 | fvmpt3i 6287 |
. . . . . . . . . 10
|
50 | 42, 49 | syl 17 |
. . . . . . . . 9
|
51 | 41, 50 | sylanl2 683 |
. . . . . . . 8
|
52 | | 1re 10039 |
. . . . . . . . . . . 12
|
53 | | elicopnf 12269 |
. . . . . . . . . . . 12
|
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . 11
|
55 | | flge1nn 12622 |
. . . . . . . . . . 11
|
56 | 54, 55 | sylbi 207 |
. . . . . . . . . 10
|
57 | 56 | adantl 482 |
. . . . . . . . 9
|
58 | | nnuz 11723 |
. . . . . . . . 9
|
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . 8
|
60 | 41, 24 | sylanl2 683 |
. . . . . . . 8
|
61 | 51, 59, 60 | fsumser 14461 |
. . . . . . 7
|
62 | 61 | mpteq2dva 4744 |
. . . . . 6
|
63 | 40, 62 | syl5eq 2668 |
. . . . 5
|
64 | | fveq2 6191 |
. . . . . . 7
|
65 | | rpssre 11843 |
. . . . . . . . 9
|
66 | 65 | a1i 11 |
. . . . . . . 8
|
67 | 38, 66 | syl5ss 3614 |
. . . . . . 7
|
68 | | 1zzd 11408 |
. . . . . . 7
|
69 | 46 | cbvmptv 4750 |
. . . . . . . . . . . . 13
|
70 | 47, 69 | eqtri 2644 |
. . . . . . . . . . . 12
|
71 | 23, 70 | fmptd 6385 |
. . . . . . . . . . 11
|
72 | 71 | ffvelrnda 6359 |
. . . . . . . . . 10
|
73 | 58, 68, 72 | serf 12829 |
. . . . . . . . 9
|
74 | 73 | feqmptd 6249 |
. . . . . . . 8
|
75 | | dchrisum0.s |
. . . . . . . 8
|
76 | 74, 75 | eqbrtrrd 4677 |
. . . . . . 7
|
77 | 73 | ffvelrnda 6359 |
. . . . . . 7
|
78 | 54 | simprbi 480 |
. . . . . . . 8
|
79 | 78 | adantl 482 |
. . . . . . 7
|
80 | 58, 64, 67, 68, 76, 77, 79 | climrlim2 14278 |
. . . . . 6
|
81 | | rlimo1 14347 |
. . . . . 6
|
82 | 80, 81 | syl 17 |
. . . . 5
|
83 | 63, 82 | eqeltrd 2701 |
. . . 4
|
84 | | eqid 2622 |
. . . . . 6
|
85 | 25, 84 | fmptd 6385 |
. . . . 5
|
86 | | 1red 10055 |
. . . . 5
|
87 | 85, 66, 86 | o1resb 14297 |
. . . 4
|
88 | 83, 87 | mpbird 247 |
. . 3
|
89 | | o1const 14350 |
. . . 4
|
90 | 65, 28, 89 | sylancr 695 |
. . 3
|
91 | 25, 29, 88, 90 | o1mul2 14355 |
. 2
|
92 | | simpr 477 |
. . . . . . . . 9
|
93 | | 2z 11409 |
. . . . . . . . 9
|
94 | | rpexpcl 12879 |
. . . . . . . . 9
|
95 | 92, 93, 94 | sylancl 694 |
. . . . . . . 8
|
96 | 3 | nnrpd 11870 |
. . . . . . . 8
|
97 | | rpdivcl 11856 |
. . . . . . . 8
|
98 | 95, 96, 97 | syl2an 494 |
. . . . . . 7
|
99 | | dchrisum0lem2.h |
. . . . . . . . 9
|
100 | 99 | divsqrsumf 24707 |
. . . . . . . 8
|
101 | 100 | ffvelrni 6358 |
. . . . . . 7
|
102 | 98, 101 | syl 17 |
. . . . . 6
|
103 | 102 | recnd 10068 |
. . . . 5
|
104 | 24, 103 | mulcld 10060 |
. . . 4
|
105 | 1, 104 | fsumcl 14464 |
. . 3
|
106 | 25, 29 | mulcld 10060 |
. . 3
|
107 | 26 | ad2antrr 762 |
. . . . . . . . 9
|
108 | 107, 27 | syl 17 |
. . . . . . . 8
|
109 | 24, 108 | mulcld 10060 |
. . . . . . 7
|
110 | 1, 104, 109 | fsumsub 14520 |
. . . . . 6
|
111 | 24, 103, 108 | subdid 10486 |
. . . . . . 7
|
112 | 111 | sumeq2dv 14433 |
. . . . . 6
|
113 | 1, 29, 24 | fsummulc1 14517 |
. . . . . . 7
|
114 | 113 | oveq2d 6666 |
. . . . . 6
|
115 | 110, 112,
114 | 3eqtr4d 2666 |
. . . . 5
|
116 | 115 | mpteq2dva 4744 |
. . . 4
|
117 | 103, 108 | subcld 10392 |
. . . . . . 7
|
118 | 24, 117 | mulcld 10060 |
. . . . . 6
|
119 | 1, 118 | fsumcl 14464 |
. . . . 5
|
120 | 119 | abscld 14175 |
. . . . . . 7
|
121 | 118 | abscld 14175 |
. . . . . . . 8
|
122 | 1, 121 | fsumrecl 14465 |
. . . . . . 7
|
123 | | 1red 10055 |
. . . . . . 7
|
124 | 1, 118 | fsumabs 14533 |
. . . . . . 7
|
125 | | rprege0 11847 |
. . . . . . . . . . . 12
|
126 | 125 | adantl 482 |
. . . . . . . . . . 11
|
127 | 126 | simpld 475 |
. . . . . . . . . 10
|
128 | | reflcl 12597 |
. . . . . . . . . 10
|
129 | 127, 128 | syl 17 |
. . . . . . . . 9
|
130 | 129, 92 | rerpdivcld 11903 |
. . . . . . . 8
|
131 | | simplr 792 |
. . . . . . . . . . 11
|
132 | 131 | rprecred 11883 |
. . . . . . . . . 10
|
133 | 24 | abscld 14175 |
. . . . . . . . . . . 12
|
134 | 96 | rpsqrtcld 14150 |
. . . . . . . . . . . . . 14
|
135 | 134 | adantl 482 |
. . . . . . . . . . . . 13
|
136 | 135 | rprecred 11883 |
. . . . . . . . . . . 12
|
137 | 117 | abscld 14175 |
. . . . . . . . . . . 12
|
138 | 135, 131 | rpdivcld 11889 |
. . . . . . . . . . . . 13
|
139 | 65, 138 | sseldi 3601 |
. . . . . . . . . . . 12
|
140 | 24 | absge0d 14183 |
. . . . . . . . . . . 12
|
141 | 117 | absge0d 14183 |
. . . . . . . . . . . 12
|
142 | 2, 3, 17 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
143 | 135 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
144 | 135 | rpne0d 11877 |
. . . . . . . . . . . . . . 15
|
145 | 142, 143,
144 | absdivd 14194 |
. . . . . . . . . . . . . 14
|
146 | 135 | rprege0d 11879 |
. . . . . . . . . . . . . . . 16
|
147 | | absid 14036 |
. . . . . . . . . . . . . . . 16
|
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
|
149 | 148 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
150 | 145, 149 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
151 | 142 | abscld 14175 |
. . . . . . . . . . . . . 14
|
152 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
153 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
154 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
155 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . . 19
|
156 | 155 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
|
157 | 5, 153, 7 | znzrhfo 19896 |
. . . . . . . . . . . . . . . . . 18
|
158 | | fof 6115 |
. . . . . . . . . . . . . . . . . 18
|
159 | 156, 157,
158 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
161 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
162 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
|
163 | 160, 161,
162 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
164 | 4, 6, 5, 153, 154, 163 | dchrabs2 24987 |
. . . . . . . . . . . . . 14
|
165 | 151, 152,
135, 164 | lediv1dd 11930 |
. . . . . . . . . . . . 13
|
166 | 150, 165 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
167 | 99, 107 | divsqrtsum2 24709 |
. . . . . . . . . . . . . 14
|
168 | 98, 167 | mpdan 702 |
. . . . . . . . . . . . 13
|
169 | 95 | rprege0d 11879 |
. . . . . . . . . . . . . . . . 17
|
170 | | sqrtdiv 14006 |
. . . . . . . . . . . . . . . . 17
|
171 | 169, 96, 170 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
172 | 125 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
173 | | sqrtsq 14010 |
. . . . . . . . . . . . . . . . . 18
|
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
175 | 174 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
176 | 171, 175 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
177 | 176 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
178 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . 16
|
179 | 178 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
180 | 135 | rpcnne0d 11881 |
. . . . . . . . . . . . . . 15
|
181 | | recdiv 10731 |
. . . . . . . . . . . . . . 15
|
182 | 179, 180,
181 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
183 | 177, 182 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
184 | 168, 183 | breqtrd 4679 |
. . . . . . . . . . . 12
|
185 | 133, 136,
137, 139, 140, 141, 166, 184 | lemul12ad 10966 |
. . . . . . . . . . 11
|
186 | 24, 117 | absmuld 14193 |
. . . . . . . . . . 11
|
187 | | 1cnd 10056 |
. . . . . . . . . . . . 13
|
188 | | dmdcan 10735 |
. . . . . . . . . . . . 13
|
189 | 180, 179,
187, 188 | syl3anc 1326 |
. . . . . . . . . . . 12
|
190 | 138 | rpcnd 11874 |
. . . . . . . . . . . . 13
|
191 | | reccl 10692 |
. . . . . . . . . . . . . 14
|
192 | 180, 191 | syl 17 |
. . . . . . . . . . . . 13
|
193 | 190, 192 | mulcomd 10061 |
. . . . . . . . . . . 12
|
194 | 189, 193 | eqtr3d 2658 |
. . . . . . . . . . 11
|
195 | 185, 186,
194 | 3brtr4d 4685 |
. . . . . . . . . 10
|
196 | 1, 121, 132, 195 | fsumle 14531 |
. . . . . . . . 9
|
197 | | flge0nn0 12621 |
. . . . . . . . . . . 12
|
198 | | hashfz1 13134 |
. . . . . . . . . . . 12
|
199 | 126, 197,
198 | 3syl 18 |
. . . . . . . . . . 11
|
200 | 199 | oveq1d 6665 |
. . . . . . . . . 10
|
201 | 92 | rpreccld 11882 |
. . . . . . . . . . . 12
|
202 | 201 | rpcnd 11874 |
. . . . . . . . . . 11
|
203 | | fsumconst 14522 |
. . . . . . . . . . 11
|
204 | 1, 202, 203 | syl2anc 693 |
. . . . . . . . . 10
|
205 | 129 | recnd 10068 |
. . . . . . . . . . 11
|
206 | 178 | adantl 482 |
. . . . . . . . . . . 12
|
207 | 206 | simpld 475 |
. . . . . . . . . . 11
|
208 | 206 | simprd 479 |
. . . . . . . . . . 11
|
209 | 205, 207,
208 | divrecd 10804 |
. . . . . . . . . 10
|
210 | 200, 204,
209 | 3eqtr4d 2666 |
. . . . . . . . 9
|
211 | 196, 210 | breqtrd 4679 |
. . . . . . . 8
|
212 | | flle 12600 |
. . . . . . . . . . 11
|
213 | 127, 212 | syl 17 |
. . . . . . . . . 10
|
214 | 127 | recnd 10068 |
. . . . . . . . . . 11
|
215 | 214 | mulid1d 10057 |
. . . . . . . . . 10
|
216 | 213, 215 | breqtrrd 4681 |
. . . . . . . . 9
|
217 | | rpregt0 11846 |
. . . . . . . . . . 11
|
218 | 217 | adantl 482 |
. . . . . . . . . 10
|
219 | | ledivmul 10899 |
. . . . . . . . . 10
|
220 | 129, 123,
218, 219 | syl3anc 1326 |
. . . . . . . . 9
|
221 | 216, 220 | mpbird 247 |
. . . . . . . 8
|
222 | 122, 130,
123, 211, 221 | letrd 10194 |
. . . . . . 7
|
223 | 120, 122,
123, 124, 222 | letrd 10194 |
. . . . . 6
|
224 | 223 | adantrr 753 |
. . . . 5
|
225 | 66, 119, 86, 86, 224 | elo1d 14267 |
. . . 4
|
226 | 116, 225 | eqeltrrd 2702 |
. . 3
|
227 | 105, 106,
226 | o1dif 14360 |
. 2
|
228 | 91, 227 | mpbird 247 |
1
|