Step Hyp Ref
Expression 1 oveq2 6304 . . . . . . 7
2 1 iuneq1d 4355 . . . . . 6
3 2 fveq2d 5875 . . . . 5
4 1 sumeq1d 13523 . . . . . 6
5 4 oveq2d 6312 . . . . 5
6 3 , 5 breq12d 4465 . . . 4
7 6 imbi2d 316 . . 3
8 oveq2 6304 . . . . . . 7
9 8 iuneq1d 4355 . . . . . 6
10 9 fveq2d 5875 . . . . 5
11 8 sumeq1d 13523 . . . . . 6
12 11 oveq2d 6312 . . . . 5
13 10 , 12 breq12d 4465 . . . 4
14 13 imbi2d 316 . . 3
15 oveq2 6304 . . . . . . 7
16 15 iuneq1d 4355 . . . . . 6
17 16 fveq2d 5875 . . . . 5
18 15 sumeq1d 13523 . . . . . 6
19 18 oveq2d 6312 . . . . 5
20 17 , 19 breq12d 4465 . . . 4
21 20 imbi2d 316 . . 3
22 oveq2 6304 . . . . . . 7
23 22 iuneq1d 4355 . . . . . 6
24 23 fveq2d 5875 . . . . 5
25 22 sumeq1d 13523 . . . . . 6
26 25 oveq2d 6312 . . . . 5
27 24 , 26 breq12d 4465 . . . 4
28 27 imbi2d 316 . . 3
29 0le0 10650 . . . . . 6
30 prmrec.3 . . . . . . . 8
31 30 nncnd 10577 . . . . . . 7
32 31 mul01d 9800 . . . . . 6
33 29 , 32 syl5breqr 4488 . . . . 5
34 prmrec.2 . . . . . . . . . . . 12
35 34 nnred 10576 . . . . . . . . . . 11
36 35 ltp1d 10501 . . . . . . . . . 10
37 34 nnzd 10993 . . . . . . . . . . . 12
38 37 peano2zd 10997 . . . . . . . . . . 11
39 fzn 11731 . . . . . . . . . . 11
40 38 , 37 , 39 syl2anc 661 . . . . . . . . . 10
41 36 , 40 mpbid 210 . . . . . . . . 9
42 41 iuneq1d 4355 . . . . . . . 8
43 0iun 4387 . . . . . . . 8
44 42 , 43 syl6eq 2514 . . . . . . 7
45 44 fveq2d 5875 . . . . . 6
46 hash0 12437 . . . . . 6
47 45 , 46 syl6eq 2514 . . . . 5
48 41 sumeq1d 13523 . . . . . . 7
49 sum0 13543 . . . . . . 7
50 48 , 49 syl6eq 2514 . . . . . 6
51 50 oveq2d 6312 . . . . 5
52 33 , 47 , 51 3brtr4d 4482 . . . 4
53 52 a1i 11 . . 3
54 fzfi 12082 . . . . . . . . . . 11
55 elfzuz 11713 . . . . . . . . . . . . . . 15
56 34 peano2nnd 10578 . . . . . . . . . . . . . . . . 17
57 eluznn 11181 . . . . . . . . . . . . . . . . 17
58 56 , 57 sylan 471 . . . . . . . . . . . . . . . 16
59 eleq1 2529 . . . . . . . . . . . . . . . . . . . . 21
60 breq1 4455 . . . . . . . . . . . . . . . . . . . . 21
61 59 , 60 anbi12d 710 . . . . . . . . . . . . . . . . . . . 20
62 61 rabbidv 3101 . . . . . . . . . . . . . . . . . . 19
63 prmrec.7 . . . . . . . . . . . . . . . . . . 19
64 ovex 6324 . . . . . . . . . . . . . . . . . . . 20
65 64 rabex 4603 . . . . . . . . . . . . . . . . . . 19
66 62 , 63 , 65 fvmpt 5956 . . . . . . . . . . . . . . . . . 18
67 66 adantl 466 . . . . . . . . . . . . . . . . 17
68 ssrab2 3584 . . . . . . . . . . . . . . . . 17
69 67 , 68 syl6eqss 3553 . . . . . . . . . . . . . . . 16
70 58 , 69 syldan 470 . . . . . . . . . . . . . . 15
71 55 , 70 sylan2 474 . . . . . . . . . . . . . 14
72 71 ralrimiva 2871 . . . . . . . . . . . . 13
73 72 adantr 465 . . . . . . . . . . . 12
74 iunss 4371 . . . . . . . . . . . 12
75 73 , 74 sylibr 212 . . . . . . . . . . 11
76 ssfi 7760 . . . . . . . . . . 11
77 54 , 75 , 76 sylancr 663 . . . . . . . . . 10
78 hashcl 12428 . . . . . . . . . 10
79 77 , 78 syl 16 . . . . . . . . 9
80 79 nn0red 10878 . . . . . . . 8
81 30 nnred 10576 . . . . . . . . . 10
82 81 adantr 465 . . . . . . . . 9
83 fzfid 12083 . . . . . . . . . 10
84 56 adantr 465 . . . . . . . . . . . 12
85 84 , 55 , 57 syl2an 477 . . . . . . . . . . 11
86 nnrecre 10597 . . . . . . . . . . . 12
87 0re 9617 . . . . . . . . . . . 12
88 ifcl 3983 . . . . . . . . . . . 12
89 86 , 87 , 88 sylancl 662 . . . . . . . . . . 11
90 85 , 89 syl 16 . . . . . . . . . 10
91 83 , 90 fsumrecl 13556 . . . . . . . . 9
92 82 , 91 remulcld 9645 . . . . . . . 8
93 prmnn 14220 . . . . . . . . . . . 12
94 nnrecre 10597 . . . . . . . . . . . 12
95 93 , 94 syl 16 . . . . . . . . . . 11
96 95 adantl 466 . . . . . . . . . 10
97 0red 9618 . . . . . . . . . 10
98 96 , 97 ifclda 3973 . . . . . . . . 9
99 82 , 98 remulcld 9645 . . . . . . . 8
100 80 , 92 , 99 leadd1d 10171 . . . . . . 7
101 eluzp1p1 11135 . . . . . . . . . . . . 13
102 101 adantl 466 . . . . . . . . . . . 12
103 simpl 457 . . . . . . . . . . . . 13
104 elfzuz 11713 . . . . . . . . . . . . 13
105 89 recnd 9643 . . . . . . . . . . . . . 14
106 58 , 105 syl 16 . . . . . . . . . . . . 13
107 103 , 104 ,
106 syl2an 477 . . . . . . . . . . . 12
108 eleq1 2529 . . . . . . . . . . . . 13
109 oveq2 6304 . . . . . . . . . . . . 13
110 108 , 109 ifbieq1d 3964 . . . . . . . . . . . 12
111 102 , 107 ,
110 fsumm1 13566 . . . . . . . . . . 11
112 eluzelz 11119 . . . . . . . . . . . . . . . . 17
113 112 adantl 466 . . . . . . . . . . . . . . . 16
114 113 zcnd 10995 . . . . . . . . . . . . . . 15
115 ax-1cn 9571 . . . . . . . . . . . . . . 15
116 pncan 9849 . . . . . . . . . . . . . . 15
117 114 , 115 ,
116 sylancl 662 . . . . . . . . . . . . . 14
118 117 oveq2d 6312 . . . . . . . . . . . . 13
119 118 sumeq1d 13523 . . . . . . . . . . . 12
120 119 oveq1d 6311 . . . . . . . . . . 11
121 111 , 120 eqtrd 2498 . . . . . . . . . 10
122 121 oveq2d 6312 . . . . . . . . 9
123 31 adantr 465 . . . . . . . . . 10
124 91 recnd 9643 . . . . . . . . . 10
125 98 recnd 9643 . . . . . . . . . 10
126 123 , 124 ,
125 adddid 9641 . . . . . . . . 9
127 122 , 126 eqtrd 2498 . . . . . . . 8
128 127 breq2d 4464 . . . . . . 7
129 100 , 128 bitr4d 256 . . . . . 6
130 104 , 70 sylan2 474 . . . . . . . . . . . . . 14
131 130 ralrimiva 2871 . . . . . . . . . . . . 13
132 131 adantr 465 . . . . . . . . . . . 12
133 iunss 4371 . . . . . . . . . . . 12
134 132 , 133 sylibr 212 . . . . . . . . . . 11
135 ssfi 7760 . . . . . . . . . . 11
136 54 , 134 , 135 sylancr 663 . . . . . . . . . 10
137 hashcl 12428 . . . . . . . . . 10
138 136 , 137 syl 16 . . . . . . . . 9
139 138 nn0red 10878 . . . . . . . 8
140 eluznn 11181 . . . . . . . . . . . . . . 15
141 34 , 140 sylan 471 . . . . . . . . . . . . . 14
142 141 peano2nnd 10578 . . . . . . . . . . . . 13
143 69 ralrimiva 2871 . . . . . . . . . . . . . 14
144 143 adantr 465 . . . . . . . . . . . . 13
145 fveq2 5871 . . . . . . . . . . . . . . 15
146 145 sseq1d 3530 . . . . . . . . . . . . . 14
147 146 rspcv 3206 . . . . . . . . . . . . 13
148 142 , 144 ,
147 sylc 60 . . . . . . . . . . . 12
149 ssfi 7760 . . . . . . . . . . . 12
150 54 , 148 , 149 sylancr 663 . . . . . . . . . . 11
151 hashcl 12428 . . . . . . . . . . 11
152 150 , 151 syl 16 . . . . . . . . . 10
153 152 nn0red 10878 . . . . . . . . 9
154 80 , 153 readdcld 9644 . . . . . . . 8
155 80 , 99 readdcld 9644 . . . . . . . 8
156 38 adantr 465 . . . . . . . . . . . . 13
157 simpr 461 . . . . . . . . . . . . . 14
158 34 nncnd 10577 . . . . . . . . . . . . . . . . 17
159 158 adantr 465 . . . . . . . . . . . . . . . 16
160 pncan 9849 . . . . . . . . . . . . . . . 16
161 159 , 115 ,
160 sylancl 662 . . . . . . . . . . . . . . 15
162 161 fveq2d 5875 . . . . . . . . . . . . . 14
163 157 , 162 eleqtrrd 2548 . . . . . . . . . . . . 13
164 fzsuc2 11766 . . . . . . . . . . . . 13
165 156 , 163 ,
164 syl2anc 661 . . . . . . . . . . . 12
166 165 iuneq1d 4355 . . . . . . . . . . 11
167 iunxun 4412 . . . . . . . . . . . 12
168 ovex 6324 . . . . . . . . . . . . . 14
169 168 , 145 iunxsn 4410 . . . . . . . . . . . . 13
170 169 uneq2i 3654 . . . . . . . . . . . 12
171 167 , 170 eqtri 2486 . . . . . . . . . . 11
172 166 , 171 syl6eq 2514 . . . . . . . . . 10
173 172 fveq2d 5875 . . . . . . . . 9
174 hashun2 12451 . . . . . . . . . 10
175 77 , 150 , 174 syl2anc 661 . . . . . . . . 9
176 173 , 175 eqbrtrd 4472 . . . . . . . 8
177 82 , 142 nndivred 10609 . . . . . . . . . . . . . 14
178 flle 11936 . . . . . . . . . . . . . 14
179 177 , 178 syl 16 . . . . . . . . . . . . 13
180 elfznn 11743 . . . . . . . . . . . . . . . . . . 19
181 180 nncnd 10577 . . . . . . . . . . . . . . . . . 18
182 181 subid1d 9943 . . . . . . . . . . . . . . . . 17
183 182 breq2d 4464 . . . . . . . . . . . . . . . 16
184 183 rabbiia 3098 . . . . . . . . . . . . . . 15
185 184 fveq2i 5874 . . . . . . . . . . . . . 14
186 1zzd 10920 . . . . . . . . . . . . . . . 16
187 30 nnnn0d 10877 . . . . . . . . . . . . . . . . . 18
188 nn0uz 11144 . . . . . . . . . . . . . . . . . . 19
189 1m1e0 10629 . . . . . . . . . . . . . . . . . . . 20
190 189 fveq2i 5874 . . . . . . . . . . . . . . . . . . 19
191 188 , 190 eqtr4i 2489 . . . . . . . . . . . . . . . . . 18
192 187 , 191 syl6eleq 2555 . . . . . . . . . . . . . . . . 17
193 192 adantr 465 . . . . . . . . . . . . . . . 16
194 0zd 10901 . . . . . . . . . . . . . . . 16
195 142 , 186 ,
193 , 194 hashdvds 14305 . . . . . . . . . . . . . . 15
196 123 subid1d 9943 . . . . . . . . . . . . . . . . . 18
197 196 oveq1d 6311 . . . . . . . . . . . . . . . . 17
198 197 fveq2d 5875 . . . . . . . . . . . . . . . 16
