Step Hyp Ref
Expression 1 1zzd 10920 . . . . . 6
2 hashdvds.3 . . . . . . . . . . . 12
3 eluzelz 11119 . . . . . . . . . . . 12
4 2 , 3 syl 16 . . . . . . . . . . 11
5 hashdvds.4 . . . . . . . . . . 11
6 4 , 5 zsubcld 10999 . . . . . . . . . 10
7 6 zred 10994 . . . . . . . . 9
8 hashdvds.1 . . . . . . . . 9
9 7 , 8 nndivred 10609 . . . . . . . 8
10 9 flcld 11935 . . . . . . 7
11 hashdvds.2 . . . . . . . . . . . 12
12 peano2zm 10932 . . . . . . . . . . . 12
13 11 , 12 syl 16 . . . . . . . . . . 11
14 13 , 5 zsubcld 10999 . . . . . . . . . 10
15 14 zred 10994 . . . . . . . . 9
16 15 , 8 nndivred 10609 . . . . . . . 8
17 16 flcld 11935 . . . . . . 7
18 10 , 17 zsubcld 10999 . . . . . 6
19 fzen 11732 . . . . . 6
20 1 , 18 , 17 , 19 syl3anc 1228 . . . . 5
21 ax-1cn 9571 . . . . . . 7
22 17 zcnd 10995 . . . . . . 7
23 addcom 9787 . . . . . . 7
24 21 , 22 , 23 sylancr 663 . . . . . 6
25 10 zcnd 10995 . . . . . . 7
26 25 , 22 npcand 9958 . . . . . 6
27 24 , 26 oveq12d 6314 . . . . 5
28 20 , 27 breqtrd 4476 . . . 4
29 ovex 6324 . . . . . 6
30 29 a1i 11 . . . . 5
31 fzfi 12082 . . . . . 6
32 rabexg 4602 . . . . . 6
33 31 , 32 mp1i 12 . . . . 5
34 elfzle1 11718 . . . . . . . . . . . . . 14
35 34 adantl 466 . . . . . . . . . . . . 13
36 elfzelz 11717 . . . . . . . . . . . . . 14
37 zltp1le 10938 . . . . . . . . . . . . . 14
38 17 , 36 , 37 syl2an 477 . . . . . . . . . . . . 13
39 35 , 38 mpbird 232 . . . . . . . . . . . 12
40 fllt 11943 . . . . . . . . . . . . 13
41 16 , 36 , 40 syl2an 477 . . . . . . . . . . . 12
42 39 , 41 mpbird 232 . . . . . . . . . . 11
43 15 adantr 465 . . . . . . . . . . . 12
44 36 adantl 466 . . . . . . . . . . . . 13
45 44 zred 10994 . . . . . . . . . . . 12
46 8 nnred 10576 . . . . . . . . . . . . . 14
47 8 nngt0d 10604 . . . . . . . . . . . . . 14
48 46 , 47 jca 532 . . . . . . . . . . . . 13
49 48 adantr 465 . . . . . . . . . . . 12
50 ltdivmul2 10445 . . . . . . . . . . . 12
51 43 , 45 , 49 , 50 syl3anc 1228 . . . . . . . . . . 11
52 42 , 51 mpbid 210 . . . . . . . . . 10
53 13 zred 10994 . . . . . . . . . . . 12
54 53 adantr 465 . . . . . . . . . . 11
55 5 zred 10994 . . . . . . . . . . . 12
56 55 adantr 465 . . . . . . . . . . 11
57 8 nnzd 10993 . . . . . . . . . . . . . 14
58 57 adantr 465 . . . . . . . . . . . . 13
59 44 , 58 zmulcld 11000 . . . . . . . . . . . 12
60 59 zred 10994 . . . . . . . . . . 11
61 54 , 56 , 60 ltsubaddd 10173 . . . . . . . . . 10
62 52 , 61 mpbid 210 . . . . . . . . 9
63 11 adantr 465 . . . . . . . . . 10
64 5 adantr 465 . . . . . . . . . . 11
65 59 , 64 zaddcld 10998 . . . . . . . . . 10
66 zlem1lt 10940 . . . . . . . . . 10
67 63 , 65 , 66 syl2anc 661 . . . . . . . . 9
68 62 , 67 mpbird 232 . . . . . . . 8
69 elfzle2 11719 . . . . . . . . . . . 12
70 69 adantl 466 . . . . . . . . . . 11
71 flge 11942 . . . . . . . . . . . 12
72 9 , 36 , 71 syl2an 477 . . . . . . . . . . 11
73 70 , 72 mpbird 232 . . . . . . . . . 10
74 7 adantr 465 . . . . . . . . . . 11
75 lemuldiv 10449 . . . . . . . . . . 11
76 45 , 74 , 49 , 75 syl3anc 1228 . . . . . . . . . 10
77 73 , 76 mpbird 232 . . . . . . . . 9
78 4 zred 10994 . . . . . . . . . . 11
79 78 adantr 465 . . . . . . . . . 10
80 leaddsub 10053 . . . . . . . . . 10
81 60 , 56 , 79 , 80 syl3anc 1228 . . . . . . . . 9
82 77 , 81 mpbird 232 . . . . . . . 8
83 4 adantr 465 . . . . . . . . 9
84 elfz 11707 . . . . . . . . 9
85 65 , 63 , 83 , 84 syl3anc 1228 . . . . . . . 8
86 68 , 82 , 85 mpbir2and 922 . . . . . . 7
87 dvdsmul2 14006 . . . . . . . . 9
88 44 , 58 , 87 syl2anc 661 . . . . . . . 8
89 59 zcnd 10995 . . . . . . . . 9
90 5 zcnd 10995 . . . . . . . . . 10
91 90 adantr 465 . . . . . . . . 9
92 89 , 91 pncand 9955 . . . . . . . 8
93 88 , 92 breqtrrd 4478 . . . . . . 7
94 oveq1 6303 . . . . . . . . 9
95 94 breq2d 4464 . . . . . . . 8
96 95 elrab 3257 . . . . . . 7
97 86 , 93 , 96 sylanbrc 664 . . . . . 6
98 97 ex 434 . . . . 5
99 oveq1 6303 . . . . . . . 8
100 99 breq2d 4464 . . . . . . 7
101 100 elrab 3257 . . . . . 6
102 53 adantr 465 . . . . . . . . . . . 12
103 elfzelz 11717 . . . . . . . . . . . . . 14
104 103 ad2antrl 727 . . . . . . . . . . . . 13
105 104 zred 10994 . . . . . . . . . . . 12
106 55 adantr 465 . . . . . . . . . . . 12
107 elfzle1 11718 . . . . . . . . . . . . . 14
108 107 ad2antrl 727 . . . . . . . . . . . . 13
109 11 adantr 465 . . . . . . . . . . . . . 14
110 zlem1lt 10940 . . . . . . . . . . . . . 14
111 109 , 104 ,
110 syl2anc 661 . . . . . . . . . . . . 13
112 108 , 111 mpbid 210 . . . . . . . . . . . 12
113 102 , 105 ,
106 , 112 ltsub1dd 10189 . . . . . . . . . . 11
114 15 adantr 465 . . . . . . . . . . . 12
115 5 adantr 465 . . . . . . . . . . . . . 14
116 104 , 115 zsubcld 10999 . . . . . . . . . . . . 13
117 116 zred 10994 . . . . . . . . . . . 12
118 48 adantr 465 . . . . . . . . . . . 12
119 ltdiv1 10431 . . . . . . . . . . . 12
120 114 , 117 ,
118 , 119 syl3anc 1228 . . . . . . . . . . 11
121 113 , 120 mpbid 210 . . . . . . . . . 10
122 16 adantr 465 . . . . . . . . . . 11
123 simprr 757 . . . . . . . . . . . 12
124 57 adantr 465 . . . . . . . . . . . . 13
125 8 nnne0d 10605 . . . . . . . . . . . . . 14
126 125 adantr 465 . . . . . . . . . . . . 13
127 dvdsval2 13989 . . . . . . . . . . . . 13
128 124 , 126 ,
116 , 127 syl3anc 1228 . . . . . . . . . . . 12
129 123 , 128 mpbid 210 . . . . . . . . . . 11
130 fllt 11943 . . . . . . . . . . 11
131 122 , 129 ,
130 syl2anc 661 . . . . . . . . . 10
132 121 , 131 mpbid 210 . . . . . . . . 9
133 17 adantr 465 . . . . . . . . . 10
134 zltp1le 10938 . . . . . . . . . 10
135 133 , 129 ,
134 syl2anc 661 . . . . . . . . 9
136 132 , 135 mpbid 210 . . . . . . . 8
137 78 adantr 465 . . . . . . . . . . 11
138 elfzle2 11719 . . . . . . . . . . . 12
139 138 ad2antrl 727 . . . . . . . . . . 11
140 105 , 137 ,
106 , 139 lesub1dd 10193 . . . . . . . . . 10
141 7 adantr 465 . . . . . . . . . . 11
142 lediv1 10432 . . . . . . . . . . 11
143 117 , 141 ,
118 , 142 syl3anc 1228 . . . . . . . . . 10
144 140 , 143 mpbid 210 . . . . . . . . 9
145 9 adantr 465 . . . . . . . . . 10
146 flge 11942 . . . . . . . . . 10
147 145 , 129 ,
146 syl2anc 661 . . . . . . . . 9
148 144 , 147 mpbid 210 . . . . . . . 8
149 17 peano2zd 10997 . . . . . . . . . 10
150 149 adantr 465 . . . . . . . . 9
151 10 adantr 465 . . . . . . . . 9
152 elfz 11707 . . . . . . . . 9
153 129 , 150 ,
151 , 152 syl3anc 1228 . . . . . . . 8
154 136 , 148 ,
153 mpbir2and 922 . . . . . . 7
155 154 ex 434 . . . . . 6
156 101 , 155 syl5bi 217 . . . . 5
157 101 anbi2i 694 . . . . . . 7
158 116 zcnd 10995 . . . . . . . . . . 11
159 158 adantrl 715 . . . . . . . . . 10
160 44 zcnd 10995 . . . . . . . . . . 11
161 160 adantrr 716 . . . . . . . . . 10
162 8 nncnd 10577 . . . . . . . . . . 11
163 162 adantr 465 . . . . . . . . . 10
164 125 adantr 465 . . . . . . . . . 10
165 159 , 161 ,
163 , 164 divmul3d 10379 . . . . . . . . 9
166 104 zcnd 10995 . . . . . . . . . . 11
167 166 adantrl 715 . . . . . . . . . 10
168 90 adantr 465 . . . . . . . . . 10
169 89 adantrr 716 . . . . . . . . . 10
170 167 , 168 ,
169 subadd2d 9973 . . . . . . . . 9
171 165 , 170 bitrd 253 . . . . . . . 8
172 eqcom 2466 . . . . . . . 8
173 eqcom 2466 . . . . . . . 8
174 171 , 172 ,
173 3bitr4g 288 . . . . . . 7
175 157 , 174 sylan2b 475 . . . . . 6
176 175 ex 434 . . . . 5
177 30 , 33 , 98 , 156 , 176 en3d 7572 . . . 4
178 entr 7587 . . . 4
179 28 , 177 , 178 syl2anc 661 . . 3
180 fzfi 12082 . . . 4
181 ssrab2 3584 . . . . 5
182 ssfi 7760 . . . . 5
183 31 , 181 , 182 mp2an 672 . . . 4
184 hashen 12420 . . . 4
185 180 , 183 ,
184 mp2an 672 . . 3
186 179 , 185 sylibr 212 . 2
187 eluzle 11122 . . . . . . 7
188 2 , 187 syl 16 . . . . . 6
189 zre 10893 . . . . . . . 8
190 zre 10893 . . . . . . . 8
191 zre 10893 . . . . . . . 8
192 lesub1 10071 . . . . . . . 8
193 189 , 190 ,
191 , 192 syl3an 1270 . . . . . . 7
194 13 , 4 , 5 , 193 syl3anc 1228 . . . . . 6
195 188 , 194 mpbid 210 . . . . 5
196 lediv1 10432 . . . . . 6
197 15 , 7 , 48 , 196 syl3anc 1228 . . . . 5
198 195 , 197 mpbid 210 . . . 4
199 flword2 11949 . . . 4
200 16 , 9 , 198 , 199 syl3anc 1228 . . 3
