Step | Hyp | Ref
| Expression |
1 | | 1zzd 9269 |
. . . . . 6
   |
2 | | hashdvds.3 |
. . . . . . . . . . 11
    
    |
3 | | eluzelz 9526 |
. . . . . . . . . . 11
    
 
  |
4 | 2, 3 | syl 14 |
. . . . . . . . . 10
   |
5 | | hashdvds.4 |
. . . . . . . . . 10
   |
6 | 4, 5 | zsubcld 9369 |
. . . . . . . . 9
     |
7 | | hashdvds.1 |
. . . . . . . . 9
   |
8 | | znq 9613 |
. . . . . . . . 9
   
       |
9 | 6, 7, 8 | syl2anc 411 |
. . . . . . . 8
       |
10 | 9 | flqcld 10263 |
. . . . . . 7
           |
11 | | hashdvds.2 |
. . . . . . . . . . 11
   |
12 | | peano2zm 9280 |
. . . . . . . . . . 11
 
   |
13 | 11, 12 | syl 14 |
. . . . . . . . . 10
     |
14 | 13, 5 | zsubcld 9369 |
. . . . . . . . 9
       |
15 | | znq 9613 |
. . . . . . . . 9
     
         |
16 | 14, 7, 15 | syl2anc 411 |
. . . . . . . 8
         |
17 | 16 | flqcld 10263 |
. . . . . . 7
             |
18 | 10, 17 | zsubcld 9369 |
. . . . . 6
                       |
19 | | fzen 10029 |
. . . . . 6
                                                                                                           |
20 | 1, 18, 17, 19 | syl3anc 1238 |
. . . . 5
                                                                           |
21 | | ax-1cn 7895 |
. . . . . . 7
 |
22 | 17 | zcnd 9365 |
. . . . . . 7
             |
23 | | addcom 8084 |
. . . . . . 7
                                       |
24 | 21, 22, 23 | sylancr 414 |
. . . . . 6
                           |
25 | 10 | zcnd 9365 |
. . . . . . 7
           |
26 | 25, 22 | npcand 8262 |
. . . . . 6
                                           |
27 | 24, 26 | oveq12d 5887 |
. . . . 5
                                                                           |
28 | 20, 27 | breqtrd 4026 |
. . . 4
                                                   |
29 | 17 | peano2zd 9367 |
. . . . . . 7
               |
30 | 29, 10 | fzfigd 10417 |
. . . . . 6
                           |
31 | 30 | elexd 2750 |
. . . . 5
                           |
32 | 11, 4 | fzfigd 10417 |
. . . . . . 7
       |
33 | | elfzelz 10011 |
. . . . . . . . . . . 12
       |
34 | 33 | adantl 277 |
. . . . . . . . . . 11
 
    
  |
35 | 5 | adantr 276 |
. . . . . . . . . . 11
 
    
  |
36 | 34, 35 | zsubcld 9369 |
. . . . . . . . . 10
 
    
    |
37 | | dvdsdc 11789 |
. . . . . . . . . 10
     DECID
    |
38 | 7, 36, 37 | syl2an2r 595 |
. . . . . . . . 9
 
    
DECID
    |
39 | 38 | ralrimiva 2550 |
. . . . . . . 8
      DECID     |
40 | | oveq1 5876 |
. . . . . . . . . . 11
       |
41 | 40 | breq2d 4012 |
. . . . . . . . . 10
   
     |
42 | 41 | dcbid 838 |
. . . . . . . . 9
 DECID   DECID      |
43 | 42 | cbvralv 2703 |
. . . . . . . 8
 
    DECID  
     DECID
    |
44 | 39, 43 | sylibr 134 |
. . . . . . 7
      DECID     |
45 | 32, 44 | ssfirab 6927 |
. . . . . 6
           |
46 | 45 | elexd 2750 |
. . . . 5
           |
47 | | elfzle1 10013 |
. . . . . . . . . . . . . 14
                                       |
48 | 47 | adantl 277 |
. . . . . . . . . . . . 13
 
                        
              |
49 | | elfzelz 10011 |
. . . . . . . . . . . . . 14
                           |
50 | | zltp1le 9296 |
. . . . . . . . . . . . . 14
           
                           |
51 | 17, 49, 50 | syl2an 289 |
. . . . . . . . . . . . 13
 
                        
                          |
52 | 48, 51 | mpbird 167 |
. . . . . . . . . . . 12
 
                        
            |
53 | | flqlt 10269 |
. . . . . . . . . . . . 13
       
                     |
54 | 16, 49, 53 | syl2an 289 |
. . . . . . . . . . . 12
 
                        
      
             |
55 | 52, 54 | mpbird 167 |
. . . . . . . . . . 11
 
                        
        |
56 | 14 | zred 9364 |
. . . . . . . . . . . . 13
       |
57 | 56 | adantr 276 |
. . . . . . . . . . . 12
 
                        
 
    |
58 | 49 | adantl 277 |
. . . . . . . . . . . . 13
 
                        
  |
59 | 58 | zred 9364 |
. . . . . . . . . . . 12
 
                        
  |
60 | 7 | nnred 8921 |
. . . . . . . . . . . . . 14
   |
61 | 7 | nngt0d 8952 |
. . . . . . . . . . . . . 14
   |
62 | 60, 61 | jca 306 |
. . . . . . . . . . . . 13
     |
63 | 62 | adantr 276 |
. . . . . . . . . . . 12
 
                        
    |
64 | | ltdivmul2 8824 |
. . . . . . . . . . . 12
     

                  |
65 | 57, 59, 63, 64 | syl3anc 1238 |
. . . . . . . . . . 11
 
                        
      
 
       |
66 | 55, 65 | mpbid 147 |
. . . . . . . . . 10
 
                        
 
      |
67 | 13 | zred 9364 |
. . . . . . . . . . . 12
     |
68 | 67 | adantr 276 |
. . . . . . . . . . 11
 
                        
    |
69 | 5 | zred 9364 |
. . . . . . . . . . . 12
   |
70 | 69 | adantr 276 |
. . . . . . . . . . 11
 
                        
  |
71 | 7 | nnzd 9363 |
. . . . . . . . . . . . . 14
   |
72 | 71 | adantr 276 |
. . . . . . . . . . . . 13
 
                        
  |
73 | 58, 72 | zmulcld 9370 |
. . . . . . . . . . . 12
 
                        
    |
74 | 73 | zred 9364 |
. . . . . . . . . . 11
 
                        
    |
75 | 68, 70, 74 | ltsubaddd 8488 |
. . . . . . . . . 10
 
                        
      
         |
76 | 66, 75 | mpbid 147 |
. . . . . . . . 9
 
                        
        |
77 | 5 | adantr 276 |
. . . . . . . . . . 11
 
                        
  |
78 | 73, 77 | zaddcld 9368 |
. . . . . . . . . 10
 
                        
      |
79 | | zlem1lt 9298 |
. . . . . . . . . 10
                     |
80 | 11, 78, 79 | syl2an2r 595 |
. . . . . . . . 9
 
                        
              |
81 | 76, 80 | mpbird 167 |
. . . . . . . 8
 
                        
      |
82 | | elfzle2 10014 |
. . . . . . . . . . . 12
                                   |
83 | 82 | adantl 277 |
. . . . . . . . . . 11
 
                        
          |
84 | | flqge 10268 |
. . . . . . . . . . . 12
     
     
           |
85 | 9, 49, 84 | syl2an 289 |
. . . . . . . . . . 11
 
                        
                |
86 | 83, 85 | mpbird 167 |
. . . . . . . . . 10
 
                        
      |
87 | 6 | zred 9364 |
. . . . . . . . . . . 12
     |
88 | 87 | adantr 276 |
. . . . . . . . . . 11
 
                        
    |
89 | | lemuldiv 8827 |
. . . . . . . . . . 11
  
 
 
    
       |
90 | 59, 88, 63, 89 | syl3anc 1238 |
. . . . . . . . . 10
 
                        
    
       |
91 | 86, 90 | mpbird 167 |
. . . . . . . . 9
 
                        
  
   |
92 | 4 | zred 9364 |
. . . . . . . . . . 11
   |
93 | 92 | adantr 276 |
. . . . . . . . . 10
 
                        
  |
94 | | leaddsub 8385 |
. . . . . . . . . 10
   
     
  
    |
95 | 74, 70, 93, 94 | syl3anc 1238 |
. . . . . . . . 9
 
                        
    
  
    |
96 | 91, 95 | mpbird 167 |
. . . . . . . 8
 
                        
      |
97 | 11 | adantr 276 |
. . . . . . . . 9
 
                        
  |
98 | 4 | adantr 276 |
. . . . . . . . 9
 
                        
  |
99 | | elfz 10001 |
. . . . . . . . 9
     
         
    
        |
100 | 78, 97, 98, 99 | syl3anc 1238 |
. . . . . . . 8
 
                        
        
    
        |
101 | 81, 96, 100 | mpbir2and 944 |
. . . . . . 7
 
                        
          |
102 | | dvdsmul2 11805 |
. . . . . . . . 9
 
     |
103 | 58, 72, 102 | syl2anc 411 |
. . . . . . . 8
 
                        
    |
104 | 73 | zcnd 9365 |
. . . . . . . . 9
 
                        
    |
105 | 5 | zcnd 9365 |
. . . . . . . . . 10
   |
106 | 105 | adantr 276 |
. . . . . . . . 9
 
                        
  |
107 | 104, 106 | pncand 8259 |
. . . . . . . 8
 
                        
          |
108 | 103, 107 | breqtrrd 4028 |
. . . . . . 7
 
                        
        |
109 | | oveq1 5876 |
. . . . . . . . 9
               |
110 | 109 | breq2d 4012 |
. . . . . . . 8
       
         |
111 | 110 | elrab 2893 |
. . . . . . 7
          
 
                  |
112 | 101, 108,
111 | sylanbrc 417 |
. . . . . 6
 
                        
              |
113 | 112 | ex 115 |
. . . . 5
                                         |
114 | | oveq1 5876 |
. . . . . . . 8
       |
115 | 114 | breq2d 4012 |
. . . . . . 7
   
     |
116 | 115 | elrab 2893 |
. . . . . 6
      
 
    
     |
117 | 67 | adantr 276 |
. . . . . . . . . . . 12
 
    
    
   |
118 | | elfzelz 10011 |
. . . . . . . . . . . . . 14
       |
119 | 118 | ad2antrl 490 |
. . . . . . . . . . . . 13
 
    
      |
120 | 119 | zred 9364 |
. . . . . . . . . . . 12
 
    
      |
121 | 69 | adantr 276 |
. . . . . . . . . . . 12
 
    
      |
122 | | elfzle1 10013 |
. . . . . . . . . . . . . 14
       |
123 | 122 | ad2antrl 490 |
. . . . . . . . . . . . 13
 
    
      |
124 | | zlem1lt 9298 |
. . . . . . . . . . . . . 14
 
       |
125 | 11, 119, 124 | syl2an2r 595 |
. . . . . . . . . . . . 13
 
    
    
     |
126 | 123, 125 | mpbid 147 |
. . . . . . . . . . . 12
 
    
    
   |
127 | 117, 120,
121, 126 | ltsub1dd 8504 |
. . . . . . . . . . 11
 
    
            |
128 | 56 | adantr 276 |
. . . . . . . . . . . 12
 
    
          |
129 | 5 | adantr 276 |
. . . . . . . . . . . . . 14
 
    
      |
130 | 119, 129 | zsubcld 9369 |
. . . . . . . . . . . . 13
 
    
        |
131 | 130 | zred 9364 |
. . . . . . . . . . . 12
 
    
        |
132 | 62 | adantr 276 |
. . . . . . . . . . . 12
 
    
    
   |
133 | | ltdiv1 8814 |
. . . . . . . . . . . 12
        
 
      
             |
134 | 128, 131,
132, 133 | syl3anc 1238 |
. . . . . . . . . . 11
 
    
        
 
             |
135 | 127, 134 | mpbid 147 |
. . . . . . . . . 10
 
    
                |
136 | | simprr 531 |
. . . . . . . . . . . 12
 
    
        |
137 | 71 | adantr 276 |
. . . . . . . . . . . . 13
 
    
      |
138 | 7 | nnne0d 8953 |
. . . . . . . . . . . . . 14
   |
139 | 138 | adantr 276 |
. . . . . . . . . . . . 13
 
    
      |
140 | | dvdsval2 11781 |
. . . . . . . . . . . . 13
               |
141 | 137, 139,
130, 140 | syl3anc 1238 |
. . . . . . . . . . . 12
 
    
      
       |
142 | 136, 141 | mpbid 147 |
. . . . . . . . . . 11
 
    
          |
143 | | flqlt 10269 |
. . . . . . . . . . 11
                                         |
144 | 16, 142, 143 | syl2an2r 595 |
. . . . . . . . . 10
 
    
          
   
                 |
145 | 135, 144 | mpbid 147 |
. . . . . . . . 9
 
    
                    |
146 | | zltp1le 9296 |
. . . . . . . . . 10
                                                   |
147 | 17, 142, 146 | syl2an2r 595 |
. . . . . . . . 9
 
    
                  
                   |
148 | 145, 147 | mpbid 147 |
. . . . . . . 8
 
    
                      |
149 | 92 | adantr 276 |
. . . . . . . . . . 11
 
    
      |
150 | | elfzle2 10014 |
. . . . . . . . . . . 12
       |
151 | 150 | ad2antrl 490 |
. . . . . . . . . . 11
 
    
      |
152 | 120, 149,
121, 151 | lesub1dd 8508 |
. . . . . . . . . 10
 
    
          |
153 | 87 | adantr 276 |
. . . . . . . . . . 11
 
    
    
   |
154 | | lediv1 8815 |
. . . . . . . . . . 11
    
 
 
    
           |
155 | 131, 153,
132, 154 | syl3anc 1238 |
. . . . . . . . . 10
 
    
      
 
           |
156 | 152, 155 | mpbid 147 |
. . . . . . . . 9
 
    
              |
157 | | flqge 10268 |
. . . . . . . . . 10
                                   |
158 | 9, 142, 157 | syl2an2r 595 |
. . . . . . . . 9
 
    
        
 
 
               |
159 | 156, 158 | mpbid 147 |
. . . . . . . 8
 
    
                  |
160 | 29 | adantr 276 |
. . . . . . . . 9
 
    
                  |
161 | 10 | adantr 276 |
. . . . . . . . 9
 
    
              |
162 | | elfz 10001 |
. . . . . . . . 9
                                                                                         |
163 | 142, 160,
161, 162 | syl3anc 1238 |
. . . . . . . 8
 
    
                                
                                 |
164 | 148, 159,
163 | mpbir2and 944 |
. . . . . . 7
 
    
                                  |
165 | 164 | ex 115 |
. . . . . 6
      
  
                               |
166 | 116, 165 | biimtrid 152 |
. . . . 5
                                         |
167 | 116 | anbi2i 457 |
. . . . . . 7
                         
     
  
                             
      |
168 | 130 | zcnd 9365 |
. . . . . . . . . . 11
 
    
        |
169 | 168 | adantrl 478 |
. . . . . . . . . 10
 
                             
         |
170 | 58 | zcnd 9365 |
. . . . . . . . . . 11
 
                        
  |
171 | 170 | adantrr 479 |
. . . . . . . . . 10
 
                             
       |
172 | 7 | nncnd 8922 |
. . . . . . . . . . 11
   |
173 | 172 | adantr 276 |
. . . . . . . . . 10
 
                             
    
  |
174 | 7 | nnap0d 8954 |
. . . . . . . . . . 11
 #   |
175 | 174 | adantr 276 |
. . . . . . . . . 10
 
                             
     #   |
176 | 169, 171,
173, 175 | divmulap3d 8771 |
. . . . . . . . 9
 
                             
                 |
177 | 119 | zcnd 9365 |
. . . . . . . . . . 11
 
    
      |
178 | 177 | adantrl 478 |
. . . . . . . . . 10
 
                             
       |
179 | 105 | adantr 276 |
. . . . . . . . . 10
 
                             
    
  |
180 | 104 | adantrr 479 |
. . . . . . . . . 10
 
                             
         |
181 | 178, 179,
180 | subadd2d 8277 |
. . . . . . . . 9
 
                             
                 |
182 | 176, 181 | bitrd 188 |
. . . . . . . 8
 
                             
                 |
183 | | eqcom 2179 |
. . . . . . . 8
    
      |
184 | | eqcom 2179 |
. . . . . . . 8
    
      |
185 | 182, 183,
184 | 3bitr4g 223 |
. . . . . . 7
 
                             
                 |
186 | 167, 185 | sylan2b 287 |
. . . . . 6
 
                                       
       |
187 | 186 | ex 115 |
. . . . 5
                                   
    
        |
188 | 31, 46, 113, 166, 187 | en3d 6763 |
. . . 4
                              
    |
189 | | entr 6778 |
. . . 4
                                                                               
                                
    |
190 | 28, 188, 189 | syl2anc 411 |
. . 3
                              
    |
191 | 1, 18 | fzfigd 10417 |
. . . 4
                           |
192 | | hashen 10748 |
. . . 4
                                    ♯                          ♯      
  
                                   |
193 | 191, 45, 192 | syl2anc 411 |
. . 3
  ♯                          ♯      
  
                                   |
194 | 190, 193 | mpbird 167 |
. 2
 ♯                          ♯            |
195 | | eluzle 9529 |
. . . . . . 7
    
 
    |
196 | 2, 195 | syl 14 |
. . . . . 6
  
  |
197 | | zre 9246 |
. . . . . . . 8
   
   |
198 | | zre 9246 |
. . . . . . . 8
   |
199 | | zre 9246 |
. . . . . . . 8
   |
200 | | lesub1 8403 |
. . . . . . . 8
   
   
 
       |
201 | 197, 198,
199, 200 | syl3an 1280 |
. . . . . . 7
   
   
 
       |
202 | 13, 4, 5, 201 | syl3anc 1238 |
. . . . . 6
             |
203 | 196, 202 | mpbid 147 |
. . . . 5
    
    |
204 | | lediv1 8815 |
. . . . . 6
      
 
 
      
             |
205 | 56, 87, 62, 204 | syl3anc 1238 |
. . . . 5
      
              |
206 | 203, 205 | mpbid 147 |
. . . 4
      
 
    |
207 | | flqword2 10275 |
. . . 4
                 
 
                           |
208 | 16, 9, 206, 207 | syl3anc 1238 |
. . 3
                         |
209 | | uznn0sub 9548 |
. . 3
                                             |
210 | | hashfz1 10747 |
. . 3
                    
♯                                                |
211 | 208, 209,
210 | 3syl 17 |
. 2
 ♯                                                |
212 | 194, 211 | eqtr3d 2212 |
1
 ♯      
                         |