Step | Hyp | Ref
| Expression |
1 | | elfzoelz 10146 |
. . . . . . . 8
  ..^
  |
2 | 1 | 3ad2ant1 1018 |
. . . . . . 7
   ..^  ..^    |
3 | | zq 9625 |
. . . . . . 7
   |
4 | 2, 3 | syl 14 |
. . . . . 6
   ..^  ..^    |
5 | | simp3 999 |
. . . . . . 7
   ..^  ..^    |
6 | | zq 9625 |
. . . . . . 7
   |
7 | 5, 6 | syl 14 |
. . . . . 6
   ..^  ..^    |
8 | | elfzo0 10181 |
. . . . . . . . . 10
  ..^ 
   |
9 | 8 | biimpi 120 |
. . . . . . . . 9
  ..^
    |
10 | 9 | 3ad2ant1 1018 |
. . . . . . . 8
   ..^  ..^  
   |
11 | 10 | simp2d 1010 |
. . . . . . 7
   ..^  ..^    |
12 | | nnq 9632 |
. . . . . . 7
   |
13 | 11, 12 | syl 14 |
. . . . . 6
   ..^  ..^    |
14 | 11 | nngt0d 8962 |
. . . . . 6
   ..^  ..^    |
15 | | modqaddmod 10362 |
. . . . . 6
                   |
16 | 4, 7, 13, 14, 15 | syl22anc 1239 |
. . . . 5
   ..^  ..^          
   |
17 | 16 | eqcomd 2183 |
. . . 4
   ..^  ..^              |
18 | | elfzoelz 10146 |
. . . . . . . 8
  ..^
  |
19 | 18 | 3ad2ant2 1019 |
. . . . . . 7
   ..^  ..^    |
20 | | zq 9625 |
. . . . . . 7
   |
21 | 19, 20 | syl 14 |
. . . . . 6
   ..^  ..^    |
22 | | modqaddmod 10362 |
. . . . . 6
                   |
23 | 21, 7, 13, 14, 22 | syl22anc 1239 |
. . . . 5
   ..^  ..^          
   |
24 | 23 | eqcomd 2183 |
. . . 4
   ..^  ..^              |
25 | 17, 24 | eqeq12d 2192 |
. . 3
   ..^  ..^                          |
26 | 2, 11 | zmodcld 10344 |
. . . . . . . . 9
   ..^  ..^      |
27 | 26 | nn0zd 9372 |
. . . . . . . 8
   ..^  ..^      |
28 | 27, 5 | zaddcld 9378 |
. . . . . . 7
   ..^  ..^        |
29 | 28, 11 | zmodcld 10344 |
. . . . . 6
   ..^  ..^          |
30 | 29 | nn0cnd 9230 |
. . . . 5
   ..^  ..^          |
31 | 19, 11 | zmodcld 10344 |
. . . . . . . . 9
   ..^  ..^      |
32 | 31 | nn0zd 9372 |
. . . . . . . 8
   ..^  ..^      |
33 | 32, 5 | zaddcld 9378 |
. . . . . . 7
   ..^  ..^        |
34 | 33, 11 | zmodcld 10344 |
. . . . . 6
   ..^  ..^          |
35 | 34 | nn0cnd 9230 |
. . . . 5
   ..^  ..^          |
36 | 30, 35 | subeq0ad 8277 |
. . . 4
   ..^  ..^                                |
37 | | oveq1 5881 |
. . . . 5
                                   |
38 | 4, 13, 14 | modqcld 10327 |
. . . . . . . . . 10
   ..^  ..^      |
39 | | qaddcl 9634 |
. . . . . . . . . 10
   
       |
40 | 38, 7, 39 | syl2anc 411 |
. . . . . . . . 9
   ..^  ..^        |
41 | 21, 13, 14 | modqcld 10327 |
. . . . . . . . . 10
   ..^  ..^      |
42 | | qaddcl 9634 |
. . . . . . . . . 10
   
       |
43 | 41, 7, 42 | syl2anc 411 |
. . . . . . . . 9
   ..^  ..^        |
44 | | modqsubmodmod 10382 |
. . . . . . . . 9
            
 
                              |
45 | 40, 43, 13, 14, 44 | syl22anc 1239 |
. . . . . . . 8
   ..^  ..^                                |
46 | 26 | nn0cnd 9230 |
. . . . . . . . . 10
   ..^  ..^      |
47 | 31 | nn0cnd 9230 |
. . . . . . . . . 10
   ..^  ..^      |
48 | 5 | zcnd 9375 |
. . . . . . . . . 10
   ..^  ..^    |
49 | 46, 47, 48 | pnpcan2d 8305 |
. . . . . . . . 9
   ..^  ..^                    |
50 | 49 | oveq1d 5889 |
. . . . . . . 8
   ..^  ..^                        |
51 | 45, 50 | eqtrd 2210 |
. . . . . . 7
   ..^  ..^                            |
52 | | q0mod 10354 |
. . . . . . . 8
       |
53 | 13, 14, 52 | syl2anc 411 |
. . . . . . 7
   ..^  ..^      |
54 | 51, 53 | eqeq12d 2192 |
. . . . . 6
   ..^  ..^                                |
55 | | zmodidfzoimp 10353 |
. . . . . . . . . . 11
  ..^
    |
56 | 55 | 3ad2ant1 1018 |
. . . . . . . . . 10
   ..^  ..^      |
57 | | zmodidfzoimp 10353 |
. . . . . . . . . . 11
  ..^
    |
58 | 57 | 3ad2ant2 1019 |
. . . . . . . . . 10
   ..^  ..^      |
59 | 56, 58 | oveq12d 5892 |
. . . . . . . . 9
   ..^  ..^     
      |
60 | 59 | oveq1d 5889 |
. . . . . . . 8
   ..^  ..^                |
61 | 60 | eqeq1d 2186 |
. . . . . . 7
   ..^  ..^                  |
62 | | qsubcl 9637 |
. . . . . . . . . 10
 
     |
63 | 4, 21, 62 | syl2anc 411 |
. . . . . . . . 9
   ..^  ..^      |
64 | | modq0 10328 |
. . . . . . . . 9
   
             |
65 | 63, 13, 14, 64 | syl3anc 1238 |
. . . . . . . 8
   ..^  ..^              |
66 | 2, 19 | zsubcld 9379 |
. . . . . . . . . 10
   ..^  ..^      |
67 | | zdiv 9340 |
. . . . . . . . . 10
  
               |
68 | 11, 66, 67 | syl2anc 411 |
. . . . . . . . 9
   ..^  ..^               |
69 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
     ..^  ..^

 
  |
70 | 69 | oveq2d 5890 |
. . . . . . . . . . . . . . . . 17
     ..^  ..^

 
      |
71 | 11 | nncnd 8932 |
. . . . . . . . . . . . . . . . . . 19
   ..^  ..^    |
72 | 71 | mul01d 8349 |
. . . . . . . . . . . . . . . . . 18
   ..^  ..^      |
73 | 72 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
     ..^  ..^

 
    |
74 | 70, 73 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
     ..^  ..^

 
    |
75 | 74 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
     ..^  ..^

 
 
  

    |
76 | | eqcom 2179 |
. . . . . . . . . . . . . . . 16
  
    |
77 | 10 | simp1d 1009 |
. . . . . . . . . . . . . . . . . . . 20
   ..^  ..^    |
78 | 77 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
     ..^  ..^

 
  |
79 | 78 | nn0cnd 9230 |
. . . . . . . . . . . . . . . . . 18
     ..^  ..^

 
  |
80 | | elfzo0 10181 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ..^ 
   |
81 | 80 | biimpi 120 |
. . . . . . . . . . . . . . . . . . . . . 22
  ..^
    |
82 | 81 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . . . 21
   ..^  ..^  
   |
83 | 82 | simp1d 1009 |
. . . . . . . . . . . . . . . . . . . 20
   ..^  ..^    |
84 | 83 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
     ..^  ..^

 
  |
85 | 84 | nn0cnd 9230 |
. . . . . . . . . . . . . . . . . 18
     ..^  ..^

 
  |
86 | 79, 85 | subeq0ad 8277 |
. . . . . . . . . . . . . . . . 17
     ..^  ..^

 
  
   |
87 | 86 | biimpd 144 |
. . . . . . . . . . . . . . . 16
     ..^  ..^

 
      |
88 | 76, 87 | biimtrid 152 |
. . . . . . . . . . . . . . 15
     ..^  ..^

 
      |
89 | 75, 88 | sylbid 150 |
. . . . . . . . . . . . . 14
     ..^  ..^

 
 
      |
90 | 89 | imp 124 |
. . . . . . . . . . . . 13
      ..^  ..^           |
91 | 90 | an32s 568 |
. . . . . . . . . . . 12
      ..^  ..^           |
92 | | subfzo0 10241 |
. . . . . . . . . . . . . . . . . 18
   ..^  ..^ 
   
     |
93 | 92 | 3adant3 1017 |
. . . . . . . . . . . . . . . . 17
   ..^  ..^     
     |
94 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
      ..^  ..^             

   |
95 | 94 | simprd 114 |
. . . . . . . . . . . . . . 15
      ..^  ..^             |
96 | | simplr 528 |
. . . . . . . . . . . . . . 15
      ..^  ..^         
     |
97 | 71 | mulridd 7973 |
. . . . . . . . . . . . . . . 16
   ..^  ..^      |
98 | 97 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
      ..^  ..^         
   |
99 | 95, 96, 98 | 3brtr4d 4035 |
. . . . . . . . . . . . . 14
      ..^  ..^         
     |
100 | | simpllr 534 |
. . . . . . . . . . . . . . . 16
      ..^  ..^           |
101 | 100 | zred 9374 |
. . . . . . . . . . . . . . 15
      ..^  ..^           |
102 | | 1red 7971 |
. . . . . . . . . . . . . . 15
      ..^  ..^           |
103 | 11 | nnrpd 9693 |
. . . . . . . . . . . . . . . 16
   ..^  ..^    |
104 | 103 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
      ..^  ..^           |
105 | 101, 102,
104 | ltmul2d 9738 |
. . . . . . . . . . . . . 14
      ..^  ..^         
  
    |
106 | 99, 105 | mpbird 167 |
. . . . . . . . . . . . 13
      ..^  ..^           |
107 | | simpr 110 |
. . . . . . . . . . . . . . 15
      ..^  ..^           |
108 | 107 | nnge1d 8961 |
. . . . . . . . . . . . . 14
      ..^  ..^           |
109 | 102, 101,
108 | lensymd 8078 |
. . . . . . . . . . . . 13
      ..^  ..^           |
110 | 106, 109 | pm2.21dd 620 |
. . . . . . . . . . . 12
      ..^  ..^           |
111 | 93 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
      ..^  ..^              

   |
112 | 111 | simpld 112 |
. . . . . . . . . . . . . . . 16
      ..^  ..^               |
113 | | simplr 528 |
. . . . . . . . . . . . . . . 16
      ..^  ..^          
     |
114 | 112, 113 | breqtrrd 4031 |
. . . . . . . . . . . . . . 15
      ..^  ..^               |
115 | 11 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . . 20
   ..^  ..^    |
116 | 115 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
    ..^
 ..^     |
117 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
    ..^
 ..^     |
118 | 116, 117 | zmulcld 9380 |
. . . . . . . . . . . . . . . . . 18
    ..^
 ..^   
   |
119 | 118 | zred 9374 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^   
   |
120 | 119 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
      ..^  ..^          
   |
121 | 11 | nnred 8931 |
. . . . . . . . . . . . . . . . 17
   ..^  ..^    |
122 | 121 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
      ..^  ..^            |
123 | 120, 122 | possumd 8525 |
. . . . . . . . . . . . . . 15
      ..^  ..^          
 
 
      |
124 | 114, 123 | mpbird 167 |
. . . . . . . . . . . . . 14
      ..^  ..^                |
125 | 97 | eqcomd 2183 |
. . . . . . . . . . . . . . . . 17
   ..^  ..^      |
126 | 125 | oveq2d 5890 |
. . . . . . . . . . . . . . . 16
   ..^  ..^              |
127 | 126 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
      ..^  ..^                      |
128 | 71 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
      ..^  ..^            |
129 | 117 | zcnd 9375 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^     |
130 | 129 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
      ..^  ..^            |
131 | | 1cnd 7972 |
. . . . . . . . . . . . . . . 16
      ..^  ..^            |
132 | 128, 130,
131 | adddid 7981 |
. . . . . . . . . . . . . . 15
      ..^  ..^          
           |
133 | 127, 132 | eqtr4d 2213 |
. . . . . . . . . . . . . 14
      ..^  ..^                    |
134 | 124, 133 | breqtrd 4029 |
. . . . . . . . . . . . 13
      ..^  ..^                |
135 | 117 | peano2zd 9377 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^       |
136 | 116, 135 | zmulcld 9380 |
. . . . . . . . . . . . . . . 16
    ..^
 ..^   
     |
137 | 136 | zred 9374 |
. . . . . . . . . . . . . . 15
    ..^
 ..^   
     |
138 | 137 | ad2antrr 488 |
. . . . . . . . . . . . . 14
      ..^  ..^          
     |
139 | | 0red 7957 |
. . . . . . . . . . . . . 14
      ..^  ..^            |
140 | 71 | adantr 276 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^     |
141 | 135 | zcnd 9375 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^       |
142 | 140, 141 | mulcomd 7978 |
. . . . . . . . . . . . . . . 16
    ..^
 ..^   
         |
143 | 142 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
      ..^  ..^          
         |
144 | 135 | zred 9374 |
. . . . . . . . . . . . . . . . 17
    ..^
 ..^       |
145 | 144 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
      ..^  ..^              |
146 | | zcn 9257 |
. . . . . . . . . . . . . . . . . . . 20
   |
147 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . . . 20
   |
148 | 146, 147 | addcomd 8107 |
. . . . . . . . . . . . . . . . . . 19
       |
149 | 147, 146 | subnegd 8274 |
. . . . . . . . . . . . . . . . . . 19
        |
150 | 148, 149 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . . 18
        |
151 | 150 | ad3antlr 493 |
. . . . . . . . . . . . . . . . 17
      ..^  ..^                 |
152 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
      ..^  ..^             |
153 | 152 | nnge1d 8961 |
. . . . . . . . . . . . . . . . . 18
      ..^  ..^             |
154 | | 1red 7971 |
. . . . . . . . . . . . . . . . . . 19
      ..^  ..^            |
155 | 152 | nnred 8931 |
. . . . . . . . . . . . . . . . . . 19
      ..^  ..^             |
156 | 154, 155 | suble0d 8492 |
. . . . . . . . . . . . . . . . . 18
      ..^  ..^             
    |
157 | 153, 156 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
      ..^  ..^            
  |
158 | 151, 157 | eqbrtrd 4025 |
. . . . . . . . . . . . . . . 16
      ..^  ..^              |
159 | 11 | nnnn0d 9228 |
. . . . . . . . . . . . . . . . . 18
   ..^  ..^    |
160 | 159 | nn0ge0d 9231 |
. . . . . . . . . . . . . . . . 17
   ..^  ..^    |
161 | 160 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
      ..^  ..^            |
162 | | mulle0r 8900 |
. . . . . . . . . . . . . . . 16
        
        |
163 | 145, 122,
158, 161, 162 | syl22anc 1239 |
. . . . . . . . . . . . . . 15
      ..^  ..^                |
164 | 143, 163 | eqbrtrd 4025 |
. . . . . . . . . . . . . 14
      ..^  ..^          
     |
165 | 138, 139,
164 | lensymd 8078 |
. . . . . . . . . . . . 13
      ..^  ..^                |
166 | 134, 165 | pm2.21dd 620 |
. . . . . . . . . . . 12
      ..^  ..^            |
167 | | elz 9254 |
. . . . . . . . . . . . . 14

       |
168 | 167 | simprbi 275 |
. . . . . . . . . . . . 13
      |
169 | 168 | ad2antlr 489 |
. . . . . . . . . . . 12
     ..^  ..^

     
     |
170 | 91, 110, 166, 169 | mpjao3dan 1307 |
. . . . . . . . . . 11
     ..^  ..^

     
  |
171 | 170 | ex 115 |
. . . . . . . . . 10
    ..^
 ..^       
   |
172 | 171 | rexlimdva 2594 |
. . . . . . . . 9
   ..^  ..^           |
173 | 68, 172 | sylbird 170 |
. . . . . . . 8
   ..^  ..^      
   |
174 | 65, 173 | sylbid 150 |
. . . . . . 7
   ..^  ..^      
   |
175 | 61, 174 | sylbid 150 |
. . . . . 6
   ..^  ..^          
   |
176 | 54, 175 | sylbid 150 |
. . . . 5
   ..^  ..^                    
   |
177 | 37, 176 | syl5 32 |
. . . 4
   ..^  ..^                    |
178 | 36, 177 | sylbird 170 |
. . 3
   ..^  ..^              
   |
179 | 25, 178 | sylbid 150 |
. 2
   ..^  ..^          
   |
180 | | oveq1 5881 |
. . 3
       |
181 | 180 | oveq1d 5889 |
. 2
   
       |
182 | 179, 181 | impbid1 142 |
1
   ..^  ..^          
   |