Step | Hyp | Ref
| Expression |
1 | | breq1 4007 |
. . . . . 6
 
   |
2 | 1 | elrab 2894 |
. . . . 5
  
    |
3 | | hashgcdeq 12239 |
. . . . . . 7
 
 ♯   ..^           
      |
4 | 3 | adantrr 479 |
. . . . . 6
    
♯   ..^                  |
5 | | iftrue 3540 |
. . . . . . 7
       
            |
6 | 5 | ad2antll 491 |
. . . . . 6
    
 
                 |
7 | 4, 6 | eqtrd 2210 |
. . . . 5
    
♯   ..^        
    |
8 | 2, 7 | sylan2b 287 |
. . . 4
 
   ♯   ..^             |
9 | 8 | sumeq2dv 11376 |
. . 3
  
 ♯   ..^     
 
        |
10 | | 1zzd 9280 |
. . . . . 6
   |
11 | | nnz 9272 |
. . . . . 6
   |
12 | 10, 11 | fzfigd 10431 |
. . . . 5
       |
13 | | dvdsssfz1 11858 |
. . . . 5
  
      |
14 | | elfznn 10054 |
. . . . . . . 8
       |
15 | | dvdsdc 11805 |
. . . . . . . 8
 
 DECID   |
16 | 14, 11, 15 | syl2anr 290 |
. . . . . . 7
 
     DECID
  |
17 | | ibar 301 |
. . . . . . . . . . 11
 
     |
18 | 14, 17 | syl 14 |
. . . . . . . . . 10
     
     |
19 | | breq1 4007 |
. . . . . . . . . . 11
 
   |
20 | 19 | elrab 2894 |
. . . . . . . . . 10
  
    |
21 | 18, 20 | bitr4di 198 |
. . . . . . . . 9
     
     |
22 | 21 | dcbid 838 |
. . . . . . . 8
     DECID
DECID
     |
23 | 22 | adantl 277 |
. . . . . . 7
 
     DECID
DECID
     |
24 | 16, 23 | mpbid 147 |
. . . . . 6
 
     DECID     |
25 | 24 | ralrimiva 2550 |
. . . . 5
      DECID     |
26 | | ssfidc 6934 |
. . . . 5
           
     DECID     
  |
27 | 12, 13, 25, 26 | syl3anc 1238 |
. . . 4
  
  |
28 | | 0z 9264 |
. . . . . . 7
 |
29 | | fzofig 10432 |
. . . . . . 7
 
  ..^   |
30 | 28, 11, 29 | sylancr 414 |
. . . . . 6
  ..^   |
31 | 30 | adantr 276 |
. . . . 5
 
    ..^   |
32 | | ssrab2 3241 |
. . . . . 6
  ..^     ..^  |
33 | 32 | a1i 9 |
. . . . 5
 
     ..^     ..^   |
34 | | elfzoelz 10147 |
. . . . . . . . . . 11
  ..^
  |
35 | 34 | adantl 277 |
. . . . . . . . . 10
       ..^ 
  |
36 | 11 | ad2antrr 488 |
. . . . . . . . . 10
       ..^ 
  |
37 | 35, 36 | gcdcld 11969 |
. . . . . . . . 9
       ..^ 
    |
38 | 37 | nn0zd 9373 |
. . . . . . . 8
       ..^ 
    |
39 | | elrabi 2891 |
. . . . . . . . . 10
  
  |
40 | 39 | ad2antlr 489 |
. . . . . . . . 9
       ..^ 
  |
41 | 40 | nnzd 9374 |
. . . . . . . 8
       ..^ 
  |
42 | | zdceq 9328 |
. . . . . . . 8
   
 DECID     |
43 | 38, 41, 42 | syl2anc 411 |
. . . . . . 7
       ..^ 
DECID     |
44 | | ibar 301 |
. . . . . . . . . 10
  ..^
 

  ..^       |
45 | | oveq1 5882 |
. . . . . . . . . . . 12
 
     |
46 | 45 | eqeq1d 2186 |
. . . . . . . . . . 11
   
     |
47 | 46 | elrab 2894 |
. . . . . . . . . 10
   ..^      ..^      |
48 | 44, 47 | bitr4di 198 |
. . . . . . . . 9
  ..^
 

  ..^       |
49 | 48 | dcbid 838 |
. . . . . . . 8
  ..^
DECID
  DECID   ..^       |
50 | 49 | adantl 277 |
. . . . . . 7
       ..^ 
DECID
  DECID   ..^       |
51 | 43, 50 | mpbid 147 |
. . . . . 6
       ..^ 
DECID
  ..^      |
52 | 51 | ralrimiva 2550 |
. . . . 5
 
     ..^ DECID   ..^      |
53 | | ssfidc 6934 |
. . . . 5
   ..^   ..^     ..^   ..^ DECID   ..^       ..^      |
54 | 31, 33, 52, 53 | syl3anc 1238 |
. . . 4
 
     ..^      |
55 | | oveq1 5882 |
. . . . . . . . . 10
 
     |
56 | 55 | eqeq1d 2186 |
. . . . . . . . 9
   
     |
57 | 56 | elrab 2894 |
. . . . . . . 8
   ..^      ..^      |
58 | 57 | simprbi 275 |
. . . . . . 7
   ..^   
    |
59 | 58 | rgen 2530 |
. . . . . 6
   ..^       |
60 | 59 | rgenw 2532 |
. . . . 5
 
  
  ..^       |
61 | | invdisj 3998 |
. . . . 5
 
      ..^      Disj  
  ..^      |
62 | 60, 61 | mp1i 10 |
. . . 4
 Disj 
   ..^      |
63 | 27, 54, 62 | hashiun 11486 |
. . 3
 ♯      ..^        ♯   ..^       |
64 | | fveq2 5516 |
. . . 4
               |
65 | | eqid 2177 |
. . . . 5
 
   |
66 | | eqid 2177 |
. . . . 5
  
    
     |
67 | 65, 66 | dvdsflip 11857 |
. . . 4
   
         
   |
68 | | oveq2 5883 |
. . . . 5
       |
69 | | simpr 110 |
. . . . 5
 
   
   |
70 | 11 | adantr 276 |
. . . . . 6
 
     |
71 | 39 | adantl 277 |
. . . . . 6
 
     |
72 | | znq 9624 |
. . . . . 6
 
     |
73 | 70, 71, 72 | syl2anc 411 |
. . . . 5
 
       |
74 | 66, 68, 69, 73 | fvmptd3 5610 |
. . . 4
 
                 |
75 | | elrabi 2891 |
. . . . . . 7
  
  |
76 | 75 | adantl 277 |
. . . . . 6
 
     |
77 | 76 | phicld 12218 |
. . . . 5
 
         |
78 | 77 | nncnd 8933 |
. . . 4
 
         |
79 | 64, 27, 67, 74, 78 | fsumf1o 11398 |
. . 3
  
      
         |
80 | 9, 63, 79 | 3eqtr4rd 2221 |
. 2
  
     ♯  
   ..^       |
81 | | iunrab 3935 |
. . . . 5
 
   ..^      ..^  
     |
82 | | breq1 4007 |
. . . . . . . . 9
   
     |
83 | | elfzoelz 10147 |
. . . . . . . . . . 11
  ..^
  |
84 | 83 | adantl 277 |
. . . . . . . . . 10
 
 ..^    |
85 | 11 | adantr 276 |
. . . . . . . . . 10
 
 ..^ 
  |
86 | | nnne0 8947 |
. . . . . . . . . . . . 13
   |
87 | 86 | neneqd 2368 |
. . . . . . . . . . . 12

  |
88 | 87 | intnand 931 |
. . . . . . . . . . 11
     |
89 | 88 | adantr 276 |
. . . . . . . . . 10
 
 ..^      |
90 | | gcdn0cl 11963 |
. . . . . . . . . 10
           |
91 | 84, 85, 89, 90 | syl21anc 1237 |
. . . . . . . . 9
 
 ..^      |
92 | | gcddvds 11964 |
. . . . . . . . . . 11
 
     
   |
93 | 84, 85, 92 | syl2anc 411 |
. . . . . . . . . 10
 
 ..^      
   |
94 | 93 | simprd 114 |
. . . . . . . . 9
 
 ..^   
  |
95 | 82, 91, 94 | elrabd 2896 |
. . . . . . . 8
 
 ..^        |
96 | | clel5 2875 |
. . . . . . . 8
    
   
   |
97 | 95, 96 | sylib 122 |
. . . . . . 7
 
 ..^  
 
    |
98 | 97 | ralrimiva 2550 |
. . . . . 6
   ..^     
   |
99 | | rabid2 2654 |
. . . . . 6
  ..^   ..^    
 
  ..^     
   |
100 | 98, 99 | sylibr 134 |
. . . . 5
  ..^   ..^    
    |
101 | 81, 100 | eqtr4id 2229 |
. . . 4
  
   ..^     ..^   |
102 | 101 | fveq2d 5520 |
. . 3
 ♯      ..^     ♯  ..^    |
103 | | nnnn0 9183 |
. . . 4
   |
104 | | hashfzo0 10803 |
. . . 4

♯  ..^    |
105 | 103, 104 | syl 14 |
. . 3
 ♯  ..^    |
106 | 102, 105 | eqtrd 2210 |
. 2
 ♯      ..^       |
107 | 80, 106 | eqtrd 2210 |
1
  
       |