Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
|
2 | | fveq2 6191 |
. . . . . . . . . 10
|
3 | 2 | oveq2d 6666 |
. . . . . . . . 9
|
4 | | oveq1 6657 |
. . . . . . . . . . 11
|
5 | 4 | fveq2d 6195 |
. . . . . . . . . 10
|
6 | 5 | sumeq2sdv 14435 |
. . . . . . . . 9
|
7 | 3, 6 | eqeq12d 2637 |
. . . . . . . 8
|
8 | 1, 7 | raleqbidv 3152 |
. . . . . . 7
|
9 | 8 | imbi2d 330 |
. . . . . 6
|
10 | | fveq2 6191 |
. . . . . . . 8
|
11 | | fveq2 6191 |
. . . . . . . . . 10
|
12 | 11 | oveq2d 6666 |
. . . . . . . . 9
|
13 | | oveq1 6657 |
. . . . . . . . . . 11
|
14 | 13 | fveq2d 6195 |
. . . . . . . . . 10
|
15 | 14 | sumeq2sdv 14435 |
. . . . . . . . 9
|
16 | 12, 15 | eqeq12d 2637 |
. . . . . . . 8
|
17 | 10, 16 | raleqbidv 3152 |
. . . . . . 7
|
18 | 17 | imbi2d 330 |
. . . . . 6
|
19 | | fveq2 6191 |
. . . . . . . 8
|
20 | | fveq2 6191 |
. . . . . . . . . 10
|
21 | 20 | oveq2d 6666 |
. . . . . . . . 9
|
22 | | oveq1 6657 |
. . . . . . . . . . 11
|
23 | 22 | fveq2d 6195 |
. . . . . . . . . 10
|
24 | 23 | sumeq2sdv 14435 |
. . . . . . . . 9
|
25 | 21, 24 | eqeq12d 2637 |
. . . . . . . 8
|
26 | 19, 25 | raleqbidv 3152 |
. . . . . . 7
|
27 | 26 | imbi2d 330 |
. . . . . 6
|
28 | | fveq2 6191 |
. . . . . . . 8
|
29 | | fveq2 6191 |
. . . . . . . . . 10
|
30 | 29 | oveq2d 6666 |
. . . . . . . . 9
|
31 | | oveq1 6657 |
. . . . . . . . . . 11
|
32 | 31 | fveq2d 6195 |
. . . . . . . . . 10
|
33 | 32 | sumeq2sdv 14435 |
. . . . . . . . 9
|
34 | 30, 33 | eqeq12d 2637 |
. . . . . . . 8
|
35 | 28, 34 | raleqbidv 3152 |
. . . . . . 7
|
36 | 35 | imbi2d 330 |
. . . . . 6
|
37 | | fzfid 12772 |
. . . . . . . . 9
|
38 | | sumz 14453 |
. . . . . . . . . 10
|
39 | 38 | olcs 410 |
. . . . . . . . 9
|
40 | 37, 39 | syl 17 |
. . . . . . . 8
|
41 | | 0nn0 11307 |
. . . . . . . . . . 11
|
42 | 41 | a1i 11 |
. . . . . . . . . 10
|
43 | | elfznn 12370 |
. . . . . . . . . . . . 13
|
44 | 43 | nnnn0d 11351 |
. . . . . . . . . . . 12
|
45 | | nn0uz 11722 |
. . . . . . . . . . . 12
|
46 | 44, 45 | syl6eleq 2711 |
. . . . . . . . . . 11
|
47 | 46 | adantl 482 |
. . . . . . . . . 10
|
48 | | simpll 790 |
. . . . . . . . . 10
|
49 | | pcfaclem 15602 |
. . . . . . . . . 10
|
50 | 42, 47, 48, 49 | syl3anc 1326 |
. . . . . . . . 9
|
51 | 50 | sumeq2dv 14433 |
. . . . . . . 8
|
52 | | fac0 13063 |
. . . . . . . . . . 11
|
53 | 52 | oveq2i 6661 |
. . . . . . . . . 10
|
54 | | pc1 15560 |
. . . . . . . . . 10
|
55 | 53, 54 | syl5eq 2668 |
. . . . . . . . 9
|
56 | 55 | adantr 481 |
. . . . . . . 8
|
57 | 40, 51, 56 | 3eqtr4rd 2667 |
. . . . . . 7
|
58 | 57 | ralrimiva 2966 |
. . . . . 6
|
59 | | nn0z 11400 |
. . . . . . . . . . . 12
|
60 | 59 | adantr 481 |
. . . . . . . . . . 11
|
61 | | uzid 11702 |
. . . . . . . . . . 11
|
62 | | peano2uz 11741 |
. . . . . . . . . . 11
|
63 | 60, 61, 62 | 3syl 18 |
. . . . . . . . . 10
|
64 | | uzss 11708 |
. . . . . . . . . 10
|
65 | | ssralv 3666 |
. . . . . . . . . 10
|
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . 9
|
67 | | oveq1 6657 |
. . . . . . . . . . 11
|
68 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
69 | | facp1 13065 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
|
71 | 70 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
72 | | simplr 792 |
. . . . . . . . . . . . . 14
|
73 | | faccl 13070 |
. . . . . . . . . . . . . . 15
|
74 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
|
75 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
|
76 | 74, 75 | jca 554 |
. . . . . . . . . . . . . . 15
|
77 | 68, 73, 76 | 3syl 18 |
. . . . . . . . . . . . . 14
|
78 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . 15
|
79 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
|
80 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
|
81 | 79, 80 | jca 554 |
. . . . . . . . . . . . . . 15
|
82 | 68, 78, 81 | 3syl 18 |
. . . . . . . . . . . . . 14
|
83 | | pcmul 15556 |
. . . . . . . . . . . . . 14
|
84 | 72, 77, 82, 83 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
85 | 71, 84 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
86 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
87 | 86 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
|
88 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
90 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . 18
|
91 | 89, 44, 90 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
|
92 | | fldivp1 15601 |
. . . . . . . . . . . . . . . . 17
|
93 | 87, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
94 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 68, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 72, 95 | pccld 15555 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 96 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
|
98 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 94, 97, 98 | syl2anr 495 |
. . . . . . . . . . . . . . . . . 18
|
100 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 86, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
102 | 101 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
104 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 100, 102,
103, 104 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
106 | 99, 105 | bitr2d 269 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
|
108 | 93, 107 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
109 | 108 | sumeq2dv 14433 |
. . . . . . . . . . . . . 14
|
110 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
|
111 | 68 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
115 | 114, 91 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
|
116 | 115 | flcld 12599 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
118 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
119 | 118, 91 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
|
120 | 119 | flcld 12599 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | zcnd 11483 |
. . . . . . . . . . . . . . 15
|
122 | 110, 117,
121 | fsumsub 14520 |
. . . . . . . . . . . . . 14
|
123 | | fzfi 12771 |
. . . . . . . . . . . . . . . 16
|
124 | 96 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . 19
|
125 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 126 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
|
128 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . . . . 22
|
129 | 128 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
|
130 | 95 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . 21
|
131 | | bernneq3 12992 |
. . . . . . . . . . . . . . . . . . . . 21
|
132 | 129, 130,
131 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
133 | 124, 113 | letrid 10189 |
. . . . . . . . . . . . . . . . . . . . . 22
|
134 | 133 | ord 392 |
. . . . . . . . . . . . . . . . . . . . 21
|
135 | 95 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
136 | | pcdvdsb 15573 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
137 | 72, 135, 130, 136 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
|
138 | 89, 130 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
139 | 138 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
140 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
141 | 139, 95, 140 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
142 | 138 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
143 | 142, 113 | lenltd 10183 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
144 | 141, 143 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . . 22
|
145 | 137, 144 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
|
146 | 134, 145 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
|
147 | 132, 146 | mt4d 152 |
. . . . . . . . . . . . . . . . . . 19
|
148 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | 148 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
150 | 124, 113,
127, 147, 149 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
151 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . 19
|
152 | 97, 126, 151 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
153 | 150, 152 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
154 | | fzss2 12381 |
. . . . . . . . . . . . . . . . 17
|
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . 16
|
156 | | sumhash 15600 |
. . . . . . . . . . . . . . . 16
|
157 | 123, 155,
156 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
158 | | hashfz1 13134 |
. . . . . . . . . . . . . . . 16
|
159 | 96, 158 | syl 17 |
. . . . . . . . . . . . . . 15
|
160 | 157, 159 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
161 | 109, 122,
160 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
|
162 | 110, 117 | fsumcl 14464 |
. . . . . . . . . . . . . 14
|
163 | 110, 121 | fsumcl 14464 |
. . . . . . . . . . . . . 14
|
164 | 124 | recnd 10068 |
. . . . . . . . . . . . . 14
|
165 | 162, 163,
164 | subaddd 10410 |
. . . . . . . . . . . . 13
|
166 | 161, 165 | mpbid 222 |
. . . . . . . . . . . 12
|
167 | 85, 166 | eqeq12d 2637 |
. . . . . . . . . . 11
|
168 | 67, 167 | syl5ib 234 |
. . . . . . . . . 10
|
169 | 168 | ralimdva 2962 |
. . . . . . . . 9
|
170 | 66, 169 | syld 47 |
. . . . . . . 8
|
171 | 170 | ex 450 |
. . . . . . 7
|
172 | 171 | a2d 29 |
. . . . . 6
|
173 | 9, 18, 27, 36, 58, 172 | nn0ind 11472 |
. . . . 5
|
174 | 173 | imp 445 |
. . . 4
|
175 | | oveq2 6658 |
. . . . . . 7
|
176 | 175 | sumeq1d 14431 |
. . . . . 6
|
177 | 176 | eqeq2d 2632 |
. . . . 5
|
178 | 177 | rspcv 3305 |
. . . 4
|
179 | 174, 178 | syl5 34 |
. . 3
|
180 | 179 | 3impib 1262 |
. 2
|
181 | 180 | 3com12 1269 |
1
|