Step | Hyp | Ref
| Expression |
1 | | elfzoelz 9765 |
. . . . . 6
  ..^  
  |
2 | | crth.1 |
. . . . . 6
 ..^    |
3 | 1, 2 | eleq2s 2194 |
. . . . 5
   |
4 | | simpr 109 |
. . . . . . . 8
 

  |
5 | | crth.4 |
. . . . . . . . . 10
  
    |
6 | 5 | simp1d 961 |
. . . . . . . . 9
   |
7 | 6 | adantr 272 |
. . . . . . . 8
 

  |
8 | | zmodfzo 9961 |
. . . . . . . 8
 
    ..^   |
9 | 4, 7, 8 | syl2anc 406 |
. . . . . . 7
 

   ..^   |
10 | 5 | simp2d 962 |
. . . . . . . . 9
   |
11 | 10 | adantr 272 |
. . . . . . . 8
 

  |
12 | | zmodfzo 9961 |
. . . . . . . 8
 
    ..^   |
13 | 4, 11, 12 | syl2anc 406 |
. . . . . . 7
 

   ..^   |
14 | | opelxpi 4509 |
. . . . . . 7
     ..^ 
  ..^ 
         ..^  ..^    |
15 | 9, 13, 14 | syl2anc 406 |
. . . . . 6
 

 
    
  ..^  ..^    |
16 | | crth.2 |
. . . . . 6
  ..^  ..^   |
17 | 15, 16 | syl6eleqr 2193 |
. . . . 5
 

 
    
  |
18 | 3, 17 | sylan2 282 |
. . . 4
 
  
    
  |
19 | | crth.3 |
. . . 4
          |
20 | 18, 19 | fmptd 5506 |
. . 3
       |
21 | | simprl 501 |
. . . . . . . 8
 

    |
22 | | elfzoelz 9765 |
. . . . . . . . . . . . 13
  ..^  
  |
23 | 22, 2 | eleq2s 2194 |
. . . . . . . . . . . 12
   |
24 | 23 | ad2antrl 477 |
. . . . . . . . . . 11
 

    |
25 | | zq 9268 |
. . . . . . . . . . 11
   |
26 | 24, 25 | syl 14 |
. . . . . . . . . 10
 

    |
27 | 6 | adantr 272 |
. . . . . . . . . . 11
 

 
  |
28 | | nnq 9275 |
. . . . . . . . . . 11
   |
29 | 27, 28 | syl 14 |
. . . . . . . . . 10
 

 
  |
30 | 27 | nngt0d 8622 |
. . . . . . . . . 10
 

 
  |
31 | 26, 29, 30 | modqcld 9942 |
. . . . . . . . 9
 

      |
32 | 10 | adantr 272 |
. . . . . . . . . . 11
 

 
  |
33 | | nnq 9275 |
. . . . . . . . . . 11
   |
34 | 32, 33 | syl 14 |
. . . . . . . . . 10
 

 
  |
35 | 32 | nngt0d 8622 |
. . . . . . . . . 10
 

 
  |
36 | 26, 34, 35 | modqcld 9942 |
. . . . . . . . 9
 

      |
37 | | opexg 4088 |
. . . . . . . . 9
                |
38 | 31, 36, 37 | syl2anc 406 |
. . . . . . . 8
 

           |
39 | | oveq1 5713 |
. . . . . . . . . 10
 
     |
40 | | oveq1 5713 |
. . . . . . . . . 10
 
     |
41 | 39, 40 | opeq12d 3660 |
. . . . . . . . 9
  
    
         |
42 | 41, 19 | fvmptg 5429 |
. . . . . . . 8
                       |
43 | 21, 38, 42 | syl2anc 406 |
. . . . . . 7
 

       
       |
44 | | simprr 502 |
. . . . . . . 8
 

    |
45 | | elfzoelz 9765 |
. . . . . . . . . . . . 13
  ..^  
  |
46 | 45, 2 | eleq2s 2194 |
. . . . . . . . . . . 12
   |
47 | 44, 46 | syl 14 |
. . . . . . . . . . 11
 

    |
48 | | zq 9268 |
. . . . . . . . . . 11
   |
49 | 47, 48 | syl 14 |
. . . . . . . . . 10
 

    |
50 | 49, 29, 30 | modqcld 9942 |
. . . . . . . . 9
 

      |
51 | 49, 34, 35 | modqcld 9942 |
. . . . . . . . 9
 

      |
52 | | opexg 4088 |
. . . . . . . . 9
                |
53 | 50, 51, 52 | syl2anc 406 |
. . . . . . . 8
 

           |
54 | | oveq1 5713 |
. . . . . . . . . 10
 
     |
55 | | oveq1 5713 |
. . . . . . . . . 10
 
     |
56 | 54, 55 | opeq12d 3660 |
. . . . . . . . 9
  
    
         |
57 | 56, 19 | fvmptg 5429 |
. . . . . . . 8
                       |
58 | 44, 53, 57 | syl2anc 406 |
. . . . . . 7
 

       
       |
59 | 43, 58 | eqeq12d 2114 |
. . . . . 6
 

                            |
60 | | opthg 4098 |
. . . . . . 7
         
           
 
   
       |
61 | 31, 36, 60 | syl2anc 406 |
. . . . . 6
 

         
                    |
62 | 59, 61 | bitrd 187 |
. . . . 5
 

                        |
63 | 27 | nnzd 9024 |
. . . . . . 7
 

 
  |
64 | 32 | nnzd 9024 |
. . . . . . 7
 

 
  |
65 | 21, 2 | syl6eleq 2192 |
. . . . . . . . 9
 

   ..^     |
66 | 65, 22 | syl 14 |
. . . . . . . 8
 

    |
67 | 44, 2 | syl6eleq 2192 |
. . . . . . . . 9
 

   ..^     |
68 | 67, 45 | syl 14 |
. . . . . . . 8
 

    |
69 | 66, 68 | zsubcld 9030 |
. . . . . . 7
 

      |
70 | 5 | simp3d 963 |
. . . . . . . 8
     |
71 | 70 | adantr 272 |
. . . . . . 7
 

      |
72 | | coprmdvds2 11567 |
. . . . . . 7
                
      |
73 | 63, 64, 69, 71, 72 | syl31anc 1187 |
. . . . . 6
 

     
  
       |
74 | | moddvds 11297 |
. . . . . . . 8
 
     
     |
75 | 27, 66, 68, 74 | syl3anc 1184 |
. . . . . . 7
 

      
     |
76 | | moddvds 11297 |
. . . . . . . 8
 
     
     |
77 | 32, 66, 68, 76 | syl3anc 1184 |
. . . . . . 7
 

      
     |
78 | 75, 77 | anbi12d 460 |
. . . . . 6
 

       
       
      |
79 | | qmulcl 9279 |
. . . . . . . . . 10
 
     |
80 | 29, 34, 79 | syl2anc 406 |
. . . . . . . . 9
 

      |
81 | | elfzole1 9773 |
. . . . . . . . . 10
  ..^  
  |
82 | 65, 81 | syl 14 |
. . . . . . . . 9
 

 
  |
83 | | elfzolt2 9774 |
. . . . . . . . . 10
  ..^  
    |
84 | 65, 83 | syl 14 |
. . . . . . . . 9
 

 
    |
85 | | modqid 9963 |
. . . . . . . . 9
      
    
     |
86 | 26, 80, 82, 84, 85 | syl22anc 1185 |
. . . . . . . 8
 

   
    |
87 | | elfzole1 9773 |
. . . . . . . . . 10
  ..^  
  |
88 | 67, 87 | syl 14 |
. . . . . . . . 9
 

 
  |
89 | | elfzolt2 9774 |
. . . . . . . . . 10
  ..^  
    |
90 | 67, 89 | syl 14 |
. . . . . . . . 9
 

 
    |
91 | | modqid 9963 |
. . . . . . . . 9
      
    
     |
92 | 49, 80, 88, 90, 91 | syl22anc 1185 |
. . . . . . . 8
 

   
    |
93 | 86, 92 | eqeq12d 2114 |
. . . . . . 7
 

              |
94 | 27, 32 | nnmulcld 8627 |
. . . . . . . 8
 

      |
95 | | moddvds 11297 |
. . . . . . . 8
   
   
     
       |
96 | 94, 66, 68, 95 | syl3anc 1184 |
. . . . . . 7
 

            
     |
97 | 93, 96 | bitr3d 189 |
. . . . . 6
 

    
     |
98 | 73, 78, 97 | 3imtr4d 202 |
. . . . 5
 

       
    
   |
99 | 62, 98 | sylbid 149 |
. . . 4
 

              |
100 | 99 | ralrimivva 2473 |
. . 3
  
            |
101 | | dff13 5601 |
. . 3
    
     

             |
102 | 20, 100, 101 | sylanbrc 411 |
. 2
       |
103 | | nnnn0 8836 |
. . . . . 6
   |
104 | | nnnn0 8836 |
. . . . . 6
   |
105 | | hashfzo0 10410 |
. . . . . . . . 9

♯  ..^    |
106 | | hashfzo0 10410 |
. . . . . . . . 9

♯  ..^    |
107 | 105, 106 | oveqan12d 5725 |
. . . . . . . 8
 
  ♯  ..^  ♯  ..^       |
108 | | 0z 8917 |
. . . . . . . . . 10
 |
109 | | simpl 108 |
. . . . . . . . . . 11
 

  |
110 | 109 | nn0zd 9023 |
. . . . . . . . . 10
 

  |
111 | | fzofig 10046 |
. . . . . . . . . 10
 
  ..^   |
112 | 108, 110,
111 | sylancr 408 |
. . . . . . . . 9
 
  ..^   |
113 | | nn0z 8926 |
. . . . . . . . . . 11

  |
114 | 113 | adantl 273 |
. . . . . . . . . 10
 

  |
115 | | fzofig 10046 |
. . . . . . . . . 10
 
  ..^   |
116 | 108, 114,
115 | sylancr 408 |
. . . . . . . . 9
 
  ..^   |
117 | | hashxp 10413 |
. . . . . . . . 9
   ..^  ..^  ♯   ..^  ..^    ♯  ..^  ♯  ..^     |
118 | 112, 116,
117 | syl2anc 406 |
. . . . . . . 8
 
 ♯   ..^  ..^    ♯  ..^  ♯  ..^     |
119 | | nn0mulcl 8865 |
. . . . . . . . 9
 
     |
120 | | hashfzo0 10410 |
. . . . . . . . 9
  
♯  ..^        |
121 | 119, 120 | syl 14 |
. . . . . . . 8
 
 ♯  ..^        |
122 | 107, 118,
121 | 3eqtr4rd 2143 |
. . . . . . 7
 
 ♯  ..^    ♯   ..^  ..^     |
123 | 119 | nn0zd 9023 |
. . . . . . . . 9
 
     |
124 | | fzofig 10046 |
. . . . . . . . 9
  
   ..^     |
125 | 108, 123,
124 | sylancr 408 |
. . . . . . . 8
 
  ..^     |
126 | | xpfi 6747 |
. . . . . . . . 9
   ..^  ..^    ..^  ..^    |
127 | 112, 116,
126 | syl2anc 406 |
. . . . . . . 8
 
   ..^  ..^    |
128 | | hashen 10371 |
. . . . . . . 8
   ..^     ..^  ..^    ♯  ..^    ♯   ..^  ..^  
 ..^     ..^  ..^     |
129 | 125, 127,
128 | syl2anc 406 |
. . . . . . 7
 
  ♯  ..^    ♯   ..^  ..^  
 ..^     ..^  ..^     |
130 | 122, 129 | mpbid 146 |
. . . . . 6
 
  ..^     ..^  ..^    |
131 | 103, 104,
130 | syl2an 285 |
. . . . 5
 
  ..^     ..^  ..^    |
132 | 6, 10, 131 | syl2anc 406 |
. . . 4
  ..^     ..^  ..^    |
133 | 132, 2, 16 | 3brtr4g 3907 |
. . 3
   |
134 | 6 | nnnn0d 8882 |
. . . . 5
   |
135 | 10 | nnnn0d 8882 |
. . . . 5
   |
136 | 134, 135,
127 | syl2anc 406 |
. . . 4
   ..^  ..^    |
137 | 16, 136 | syl5eqel 2186 |
. . 3
   |
138 | | f1finf1o 6763 |
. . 3
 
             |
139 | 133, 137,
138 | syl2anc 406 |
. 2
             |
140 | 102, 139 | mpbid 146 |
1
       |