Proof of Theorem pellexlem6
Step | Hyp | Ref
| Expression |
1 | | pellex.ann |
. . . . . . . . 9
   |
2 | 1 | nncnd 10625 |
. . . . . . . 8
   |
3 | | pellex.enn |
. . . . . . . . 9
   |
4 | 3 | nncnd 10625 |
. . . . . . . 8
   |
5 | 2, 4 | mulcld 9663 |
. . . . . . 7
     |
6 | | pellex.dnn |
. . . . . . . . 9
   |
7 | 6 | nncnd 10625 |
. . . . . . . 8
   |
8 | | pellex.bnn |
. . . . . . . . . 10
   |
9 | 8 | nncnd 10625 |
. . . . . . . . 9
   |
10 | | pellex.fnn |
. . . . . . . . . 10
   |
11 | 10 | nncnd 10625 |
. . . . . . . . 9
   |
12 | 9, 11 | mulcld 9663 |
. . . . . . . 8
     |
13 | 7, 12 | mulcld 9663 |
. . . . . . 7
  
    |
14 | 5, 13 | subcld 9986 |
. . . . . 6
    
      |
15 | | pellex.cz |
. . . . . . 7
   |
16 | 15 | zcnd 11041 |
. . . . . 6
   |
17 | | pellex.cn0 |
. . . . . 6
   |
18 | 14, 16, 17 | absdivd 13517 |
. . . . 5
        
             
            |
19 | 5, 13 | negsubd 9992 |
. . . . . . . . . . 11
     

             |
20 | 19 | eqcomd 2457 |
. . . . . . . . . 10
    
         
     |
21 | 20 | oveq1d 6305 |
. . . . . . . . 9
     

              
          |
22 | 1 | nnred 10624 |
. . . . . . . . . . 11
   |
23 | 3 | nnred 10624 |
. . . . . . . . . . 11
   |
24 | 22, 23 | remulcld 9671 |
. . . . . . . . . 10
     |
25 | 6 | nnred 10624 |
. . . . . . . . . . 11
   |
26 | 8 | nnred 10624 |
. . . . . . . . . . . 12
   |
27 | 10 | nnred 10624 |
. . . . . . . . . . . 12
   |
28 | 26, 27 | remulcld 9671 |
. . . . . . . . . . 11
     |
29 | 25, 28 | remulcld 9671 |
. . . . . . . . . 10
  
    |
30 | 29 | renegcld 10046 |
. . . . . . . . . 10
   
    |
31 | 16, 17 | absrpcld 13510 |
. . . . . . . . . 10
       |
32 | 3 | nnzd 11039 |
. . . . . . . . . . . 12
   |
33 | | pellex.xcg |
. . . . . . . . . . . 12
               |
34 | | modmul1 12143 |
. . . . . . . . . . . 12
                                         |
35 | 22, 23, 32, 31, 33, 34 | syl221anc 1279 |
. . . . . . . . . . 11
                   |
36 | 4 | sqcld 12414 |
. . . . . . . . . . . . . . 15
       |
37 | 11 | sqcld 12414 |
. . . . . . . . . . . . . . . 16
       |
38 | 7, 37 | mulcld 9663 |
. . . . . . . . . . . . . . 15
         |
39 | 36, 38 | npcand 9990 |
. . . . . . . . . . . . . 14
       
                   |
40 | 4 | sqvald 12413 |
. . . . . . . . . . . . . 14
         |
41 | 39, 40 | eqtr2d 2486 |
. . . . . . . . . . . . 13
                         |
42 | 41 | oveq1d 6305 |
. . . . . . . . . . . 12
                                     |
43 | 23 | resqcld 12442 |
. . . . . . . . . . . . . 14
       |
44 | 27 | resqcld 12442 |
. . . . . . . . . . . . . . 15
       |
45 | 25, 44 | remulcld 9671 |
. . . . . . . . . . . . . 14
         |
46 | 43, 45 | resubcld 10047 |
. . . . . . . . . . . . 13
      
        |
47 | | 0red 9644 |
. . . . . . . . . . . . 13
   |
48 | 16 | abscld 13498 |
. . . . . . . . . . . . . . . . . . 19
       |
49 | 48 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
       |
50 | 16, 17 | absne0d 13509 |
. . . . . . . . . . . . . . . . . 18
       |
51 | 49, 50 | dividd 10381 |
. . . . . . . . . . . . . . . . 17
             |
52 | | 1zzd 10968 |
. . . . . . . . . . . . . . . . 17
   |
53 | 51, 52 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
             |
54 | | mod0 12103 |
. . . . . . . . . . . . . . . . 17
                
                  |
55 | 48, 31, 54 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
           
             |
56 | 53, 55 | mpbird 236 |
. . . . . . . . . . . . . . 15
     
       |
57 | 15 | zred 11040 |
. . . . . . . . . . . . . . . 16
   |
58 | | absmod0 13366 |
. . . . . . . . . . . . . . . 16
             
             |
59 | 57, 31, 58 | syl2anc 667 |
. . . . . . . . . . . . . . 15
            
        |
60 | 56, 59 | mpbird 236 |
. . . . . . . . . . . . . 14
         |
61 | | pellex.no2 |
. . . . . . . . . . . . . . 15
      
        |
62 | 61 | oveq1d 6305 |
. . . . . . . . . . . . . 14
       
                   |
63 | | 0mod 12128 |
. . . . . . . . . . . . . . 15
    
        |
64 | 31, 63 | syl 17 |
. . . . . . . . . . . . . 14
         |
65 | 60, 62, 64 | 3eqtr4d 2495 |
. . . . . . . . . . . . 13
       
                   |
66 | | modadd1 12134 |
. . . . . . . . . . . . 13
        
     
                   
                 
       
                                  |
67 | 46, 47, 45, 31, 65, 66 | syl221anc 1279 |
. . . . . . . . . . . 12
                                           |
68 | 38 | addid2d 9834 |
. . . . . . . . . . . . . 14
                 |
69 | 11 | sqvald 12413 |
. . . . . . . . . . . . . . 15
         |
70 | 69 | oveq2d 6306 |
. . . . . . . . . . . . . 14
        
    |
71 | 7, 11, 11 | mul12d 9842 |
. . . . . . . . . . . . . 14
  
        |
72 | 68, 70, 71 | 3eqtrd 2489 |
. . . . . . . . . . . . 13
               |
73 | 72 | oveq1d 6305 |
. . . . . . . . . . . 12
                 
         |
74 | 42, 67, 73 | 3eqtrd 2489 |
. . . . . . . . . . 11
                     |
75 | 6 | nnzd 11039 |
. . . . . . . . . . . . . 14
   |
76 | 10 | nnzd 11039 |
. . . . . . . . . . . . . 14
   |
77 | 75, 76 | zmulcld 11046 |
. . . . . . . . . . . . 13
     |
78 | | pellex.ycg |
. . . . . . . . . . . . . 14
               |
79 | 78 | eqcomd 2457 |
. . . . . . . . . . . . 13
               |
80 | | modmul1 12143 |
. . . . . . . . . . . . 13
                           
                   |
81 | 27, 26, 77, 31, 79, 80 | syl221anc 1279 |
. . . . . . . . . . . 12
   
                   |
82 | 9, 7, 11 | mul12d 9842 |
. . . . . . . . . . . . 13
  
        |
83 | 82 | oveq1d 6305 |
. . . . . . . . . . . 12
   
                   |
84 | 81, 83 | eqtrd 2485 |
. . . . . . . . . . 11
   
                   |
85 | 35, 74, 84 | 3eqtrd 2489 |
. . . . . . . . . 10
                     |
86 | | modadd1 12134 |
. . . . . . . . . 10
      
     
                  
 
            
           
   

          |
87 | 24, 29, 30, 31, 85, 86 | syl221anc 1279 |
. . . . . . . . 9
       
           
   

          |
88 | 13 | negidd 9976 |
. . . . . . . . . 10
   
   

     |
89 | 88 | oveq1d 6305 |
. . . . . . . . 9
         
                |
90 | 21, 87, 89 | 3eqtrd 2489 |
. . . . . . . 8
     

                |
91 | 90, 64 | eqtrd 2485 |
. . . . . . 7
     

          |
92 | 24, 29 | resubcld 10047 |
. . . . . . . 8
    
      |
93 | | absmod0 13366 |
. . . . . . . 8
     
        
     
                              |
94 | 92, 31, 93 | syl2anc 667 |
. . . . . . 7
       
                             |
95 | 91, 94 | mpbid 214 |
. . . . . 6
                     |
96 | 14 | abscld 13498 |
. . . . . . 7
               |
97 | | mod0 12103 |
. . . . . . 7
                                             
             |
98 | 96, 31, 97 | syl2anc 667 |
. . . . . 6
         
                 
             |
99 | 95, 98 | mpbid 214 |
. . . . 5
                     |
100 | 18, 99 | eqeltrd 2529 |
. . . 4
        
        |
101 | 92, 57, 17 | redivcld 10435 |
. . . . 5
     

      |
102 | | absz 13374 |
. . . . 5
     
    
     
            
         |
103 | 101, 102 | syl 17 |
. . . 4
       
                     |
104 | 100, 103 | mpbird 236 |
. . 3
     

      |
105 | | 0lt1 10136 |
. . . . . . . 8
 |
106 | | 0re 9643 |
. . . . . . . . 9
 |
107 | | 1re 9642 |
. . . . . . . . 9
 |
108 | 106, 107 | ltnlei 9755 |
. . . . . . . 8

  |
109 | 105, 108 | mpbi 212 |
. . . . . . 7
 |
110 | 9, 4 | mulcld 9663 |
. . . . . . . . . . . . . 14
     |
111 | 2, 11 | mulcld 9663 |
. . . . . . . . . . . . . 14
     |
112 | 110, 111 | subcld 9986 |
. . . . . . . . . . . . 13
    
    |
113 | 112, 16, 17 | divcld 10383 |
. . . . . . . . . . . 12
     
     |
114 | 113 | abscld 13498 |
. . . . . . . . . . 11
        
      |
115 | 114 | resqcld 12442 |
. . . . . . . . . 10
         
         |
116 | 6 | nnnn0d 10925 |
. . . . . . . . . . 11
   |
117 | 116 | nn0ge0d 10928 |
. . . . . . . . . 10

  |
118 | 114 | sqge0d 12443 |
. . . . . . . . . 10

                  |
119 | 25, 115, 117, 118 | mulge0d 10190 |
. . . . . . . . 9

         
          |
120 | 25, 115 | remulcld 9671 |
. . . . . . . . . 10
          
          |
121 | 47, 120 | suble0d 10204 |
. . . . . . . . 9
            
                  
           |
122 | 119, 121 | mpbird 236 |
. . . . . . . 8
  
                    |
123 | | breq1 4405 |
. . . . . . . 8
           
         
          
            |
124 | 122, 123 | syl5ibrcom 226 |
. . . . . . 7
            
        
   |
125 | 109, 124 | mtoi 182 |
. . . . . 6
           
           |
126 | | absresq 13365 |
. . . . . . . . . . . 12
     
    
         
             

         |
127 | 101, 126 | syl 17 |
. . . . . . . . . . 11
         
               
         |
128 | 14, 16, 17 | sqdivd 12429 |
. . . . . . . . . . 11
       
            
              |
129 | 14 | sqvald 12413 |
. . . . . . . . . . . 12
     

                  

      |
130 | 129 | oveq1d 6305 |
. . . . . . . . . . 11
       
                        

           |
131 | 127, 128,
130 | 3eqtrd 2489 |
. . . . . . . . . 10
         
               
      
            |
132 | 26, 23 | remulcld 9671 |
. . . . . . . . . . . . . . . 16
     |
133 | 22, 27 | remulcld 9671 |
. . . . . . . . . . . . . . . 16
     |
134 | 132, 133 | resubcld 10047 |
. . . . . . . . . . . . . . 15
    
    |
135 | 134, 57, 17 | redivcld 10435 |
. . . . . . . . . . . . . 14
     
     |
136 | | absresq 13365 |
. . . . . . . . . . . . . 14
     
           
                     |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
         
                     |
138 | 112, 16, 17 | sqdivd 12429 |
. . . . . . . . . . . . 13
                  
            |
139 | 137, 138 | eqtrd 2485 |
. . . . . . . . . . . 12
         
                         |
140 | 139 | oveq2d 6306 |
. . . . . . . . . . 11
          
                            |
141 | 112 | sqcld 12414 |
. . . . . . . . . . . 12
     
       |
142 | 16 | sqcld 12414 |
. . . . . . . . . . . 12
       |
143 | | sqne0 12341 |
. . . . . . . . . . . . . 14
         |
144 | 16, 143 | syl 17 |
. . . . . . . . . . . . 13
         |
145 | 17, 144 | mpbird 236 |
. . . . . . . . . . . 12
       |
146 | 7, 141, 142, 145 | divassd 10418 |
. . . . . . . . . . 11
       
                               |
147 | 112 | sqvald 12413 |
. . . . . . . . . . . . 13
     
               
     |
148 | 147 | oveq2d 6306 |
. . . . . . . . . . . 12
      
                 
      |
149 | 148 | oveq1d 6305 |
. . . . . . . . . . 11
       
                       
           |
150 | 140, 146,
149 | 3eqtr2d 2491 |
. . . . . . . . . 10
          
                    
           |
151 | 131, 150 | oveq12d 6308 |
. . . . . . . . 9
          

                 
                       

               
                  |
152 | 14, 14 | mulcld 9663 |
. . . . . . . . . 10
     

              |
153 | 112, 112 | mulcld 9663 |
. . . . . . . . . . 11
     
           |
154 | 7, 153 | mulcld 9663 |
. . . . . . . . . 10
      
            |
155 | 152, 154,
142, 145 | divsubdird 10422 |
. . . . . . . . 9
               

    
    
                      
       

               
                  |
156 | 5, 13, 5, 13 | mulsubd 10077 |
. . . . . . . . . . . 12
     

                 
        
         
      
        |
157 | 110, 111,
110, 111 | mulsubd 10077 |
. . . . . . . . . . . . . 14
     
              
                   
      |
158 | 157 | oveq2d 6306 |
. . . . . . . . . . . . 13
      
                                            |
159 | 110, 110 | mulcld 9663 |
. . . . . . . . . . . . . . 15
    
    |
160 | 111, 111 | mulcld 9663 |
. . . . . . . . . . . . . . 15
    
    |
161 | 159, 160 | addcld 9662 |
. . . . . . . . . . . . . 14
                 |
162 | 110, 111 | mulcld 9663 |
. . . . . . . . . . . . . . 15
    
    |
163 | 162, 162 | addcld 9662 |
. . . . . . . . . . . . . 14
                 |
164 | 7, 161, 163 | subdid 10074 |
. . . . . . . . . . . . 13
                                                                     |
165 | 7, 159, 160 | adddid 9667 |
. . . . . . . . . . . . . 14
      
                       
      |
166 | 7, 162, 162 | adddid 9667 |
. . . . . . . . . . . . . 14
      
                       
      |
167 | 165, 166 | oveq12d 6308 |
. . . . . . . . . . . . 13
                  
                                                        |
168 | 158, 164,
167 | 3eqtrd 2489 |
. . . . . . . . . . . 12
      
                                                  |
169 | 156, 168 | oveq12d 6308 |
. . . . . . . . . . 11
       
      
                
           
        
         
      
            
                         
        |
170 | 169 | oveq1d 6305 |
. . . . . . . . . 10
               

    
    
                            
                     
                   
         
                     |
171 | 5, 13 | mulcomd 9664 |
. . . . . . . . . . . . . . . 16
    
              |
172 | 7, 12, 5 | mulassd 9666 |
. . . . . . . . . . . . . . . 16
   
  
            |
173 | 2, 4 | mulcomd 9664 |
. . . . . . . . . . . . . . . . . . 19
       |
174 | 173 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
    
          |
175 | 9, 11, 4, 2 | mul4d 9845 |
. . . . . . . . . . . . . . . . . 18
    
          |
176 | 11, 2 | mulcomd 9664 |
. . . . . . . . . . . . . . . . . . 19
       |
177 | 176 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
    
          |
178 | 174, 175,
177 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . 17
    
          |
179 | 178 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
                   |
180 | 171, 172,
179 | 3eqtrd 2489 |
. . . . . . . . . . . . . . 15
    
        
     |
181 | 180, 180 | oveq12d 6308 |
. . . . . . . . . . . . . 14
      
                         
      |
182 | 181 | oveq2d 6306 |
. . . . . . . . . . . . 13
           
  
                  
                   
         
               |
183 | 182 | oveq1d 6305 |
. . . . . . . . . . . 12
                
         
                   
                         
                 
                     
                   
         
                |
184 | 5, 5 | mulcld 9663 |
. . . . . . . . . . . . . 14
    
    |
185 | 13, 13 | mulcld 9663 |
. . . . . . . . . . . . . 14
   
  
      |
186 | 184, 185 | addcld 9662 |
. . . . . . . . . . . . 13
          
          |
187 | 7, 159 | mulcld 9663 |
. . . . . . . . . . . . . 14
           |
188 | 7, 160 | mulcld 9663 |
. . . . . . . . . . . . . 14
           |
189 | 187, 188 | addcld 9662 |
. . . . . . . . . . . . 13
      
              |
190 | 7, 162 | mulcld 9663 |
. . . . . . . . . . . . . 14
           |
191 | 190, 190 | addcld 9662 |
. . . . . . . . . . . . 13
      
              |
192 | 186, 189,
191 | nnncan2d 10021 |
. . . . . . . . . . . 12
                
         
                   
                         
           
        
                         |
193 | 184, 185,
187, 188 | addsub4d 10033 |
. . . . . . . . . . . . 13
           
  
                  
                 
           
   
 
         |
194 | 5 | sqvald 12413 |
. . . . . . . . . . . . . . 15
               |
195 | 110 | sqvald 12413 |
. . . . . . . . . . . . . . . 16
               |
196 | 195 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                   |
197 | 194, 196 | oveq12d 6308 |
. . . . . . . . . . . . . 14
        
 
                 
      |
198 | 13 | sqvald 12413 |
. . . . . . . . . . . . . . 15
   
           
     |
199 | 111 | sqvald 12413 |
. . . . . . . . . . . . . . . 16
               |
200 | 199 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                   |
201 | 198, 200 | oveq12d 6308 |
. . . . . . . . . . . . . 14
          
 
         
           
      |
202 | 197, 201 | oveq12d 6308 |
. . . . . . . . . . . . 13
         
           
                    
                  
   
           |
203 | 2, 4 | sqmuld 12428 |
. . . . . . . . . . . . . . . 16
                   |
204 | 9, 4 | sqmuld 12428 |
. . . . . . . . . . . . . . . . . 18
                   |
205 | 204 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
                       |
206 | 9 | sqcld 12414 |
. . . . . . . . . . . . . . . . . 18
       |
207 | 7, 206, 36 | mulassd 9666 |
. . . . . . . . . . . . . . . . 17
                           |
208 | 205, 207 | eqtr4d 2488 |
. . . . . . . . . . . . . . . 16
                       |
209 | 203, 208 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
        
 
                                |
210 | 7 | sqvald 12413 |
. . . . . . . . . . . . . . . . . 18
         |
211 | 9, 11 | sqmuld 12428 |
. . . . . . . . . . . . . . . . . 18
                   |
212 | 210, 211 | oveq12d 6308 |
. . . . . . . . . . . . . . . . 17
                             |
213 | 7, 12 | sqmuld 12428 |
. . . . . . . . . . . . . . . . 17
   
                   |
214 | 7, 7 | mulcld 9663 |
. . . . . . . . . . . . . . . . . 18
     |
215 | 214, 206,
37 | mulassd 9666 |
. . . . . . . . . . . . . . . . 17
                               |
216 | 212, 213,
215 | 3eqtr4d 2495 |
. . . . . . . . . . . . . . . 16
   
                     |
217 | 2, 11 | sqmuld 12428 |
. . . . . . . . . . . . . . . . . 18
                   |
218 | 217 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
                       |
219 | 2 | sqcld 12414 |
. . . . . . . . . . . . . . . . . 18
       |
220 | 7, 219, 37 | mulassd 9666 |
. . . . . . . . . . . . . . . . 17
                           |
221 | 218, 220 | eqtr4d 2488 |
. . . . . . . . . . . . . . . 16
                       |
222 | 216, 221 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
          
 
                                    |
223 | 209, 222 | oveq12d 6308 |
. . . . . . . . . . . . . 14
         
           
                                                                       |
224 | 7, 206 | mulcld 9663 |
. . . . . . . . . . . . . . . . 17
         |
225 | 219, 224,
36 | subdird 10075 |
. . . . . . . . . . . . . . . 16
       
                                     |
226 | | pellex.no1 |
. . . . . . . . . . . . . . . . 17
      
        |
227 | 226 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
       
                   |
228 | 225, 227 | eqtr3d 2487 |
. . . . . . . . . . . . . . 15
                                 |
229 | 7, 7, 206 | mulassd 9666 |
. . . . . . . . . . . . . . . . . 18
          
        |
230 | 229 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
          
                        |
231 | 230 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
           
                                   |
232 | 214, 206 | mulcld 9663 |
. . . . . . . . . . . . . . . . 17
           |
233 | 7, 219 | mulcld 9663 |
. . . . . . . . . . . . . . . . 17
         |
234 | 232, 233,
37 | subdird 10075 |
. . . . . . . . . . . . . . . 16
           
                                         |
235 | | subdi 10052 |
. . . . . . . . . . . . . . . . . . . 20
  
          
 
                    
        |
236 | 235 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19
  
            
                             |
237 | 7, 224, 219, 236 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18
   
                             |
238 | | negsubdi2 9933 |
. . . . . . . . . . . . . . . . . . . . . 22
      
            
                    |
239 | 238 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . 21
      
                        
        |
240 | 219, 224,
239 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
                   
        |
241 | 226 | negeqd 9869 |
. . . . . . . . . . . . . . . . . . . 20
       
         |
242 | 240, 241 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
                |
243 | 242 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
                    |
244 | 7, 16 | mulneg2d 10072 |
. . . . . . . . . . . . . . . . . 18
     
   |
245 | 237, 243,
244 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . 17
   
                  |
246 | 245 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
           
             
        |
247 | 231, 234,
246 | 3eqtr3d 2493 |
. . . . . . . . . . . . . . 15
                               
        |
248 | 228, 247 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                                                                
         |
249 | 7, 16 | mulcld 9663 |
. . . . . . . . . . . . . . . . . 18
     |
250 | 249, 37 | mulneg1d 10071 |
. . . . . . . . . . . . . . . . 17
                     |
251 | 7, 16 | mulcomd 9664 |
. . . . . . . . . . . . . . . . . . . 20
       |
252 | 251 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                   |
253 | 16, 7, 37 | mulassd 9666 |
. . . . . . . . . . . . . . . . . . 19
          
        |
254 | 252, 253 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . 18
          
        |
255 | 254 | negeqd 9869 |
. . . . . . . . . . . . . . . . 17
           

        |
256 | 250, 255 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
           

        |
257 | 256 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
          
                
         |
258 | 16, 36 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
         |
259 | 16, 38 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
  
        |
260 | 258, 259 | negsubd 9992 |
. . . . . . . . . . . . . . 15
         
               

         |
261 | 61 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
                   |
262 | | subdi 10052 |
. . . . . . . . . . . . . . . . . 18
      
                            
         |
263 | 262 | eqcomd 2457 |
. . . . . . . . . . . . . . . . 17
      
                                      |
264 | 16, 36, 38, 263 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                                 |
265 | 16 | sqvald 12413 |
. . . . . . . . . . . . . . . 16
         |
266 | 261, 264,
265 | 3eqtr4d 2495 |
. . . . . . . . . . . . . . 15
                       |
267 | 257, 260,
266 | 3eqtrd 2489 |
. . . . . . . . . . . . . 14
          
             |
268 | 223, 248,
267 | 3eqtrd 2489 |
. . . . . . . . . . . . 13
         
           
                     |
269 | 193, 202,
268 | 3eqtr2d 2491 |
. . . . . . . . . . . 12
           
  
                  
           |
270 | 183, 192,
269 | 3eqtrd 2489 |
. . . . . . . . . . 11
                
         
                   
                         
            |
271 | 270 | oveq1d 6305 |
. . . . . . . . . 10
        
        
         
      
            
                         
                       |
272 | 142, 145 | dividd 10381 |
. . . . . . . . . 10
             |
273 | 170, 271,
272 | 3eqtrd 2489 |
. . . . . . . . 9
               

    
    
                  |
274 | 151, 155,
273 | 3eqtr2d 2491 |
. . . . . . . 8
          

                 
           |
275 | 274 | adantr 467 |
. . . . . . 7
 
 
  
             
         
        
           |
276 | | simpr 463 |
. . . . . . . . . . . 12
 
 
  
              |
277 | 276 | oveq1d 6305 |
. . . . . . . . . . 11
 
 
  
        
         |
278 | 277 | fveq2d 5869 |
. . . . . . . . . 10
 
 
  
            
             |
279 | 16, 17 | div0d 10382 |
. . . . . . . . . . . 12
     |
280 | 279 | abs00bd 13354 |
. . . . . . . . . . 11
         |
281 | 280 | adantr 467 |
. . . . . . . . . 10
 
 
  
            |
282 | 278, 281 | eqtrd 2485 |
. . . . . . . . 9
 
 
  
            
       |
283 | 282 | sq0id 12368 |
. . . . . . . 8
 
 
  
            
           |
284 | 283 | oveq1d 6305 |
. . . . . . 7
 
 
  
             
         
        
                   
           |
285 | 275, 284 | eqtr3d 2487 |
. . . . . 6
 
 
  
              
           |
286 | 125, 285 | mtand 665 |
. . . . 5
    

     |
287 | 286 | neqned 2631 |
. . . 4
    
      |
288 | 14, 16, 287, 17 | divne0d 10399 |
. . 3
     

      |
289 | | nnabscl 13388 |
. . 3
      

        

            
        |
290 | 104, 288,
289 | syl2anc 667 |
. 2
        
        |
291 | 112, 16, 17 | absdivd 13517 |
. . . . 5
        
                      |
292 | | negsub 9922 |
. . . . . . . . . . . 12
    
            
    |
293 | 292 | eqcomd 2457 |
. . . . . . . . . . 11
    
     
      
    |
294 | 110, 111,
293 | syl2anc 667 |
. . . . . . . . . 10
    
           |
295 | 294 | oveq1d 6305 |
. . . . . . . . 9
     
                      |
296 | 133 | renegcld 10046 |
. . . . . . . . . 10
      |
297 | 11, 4 | mulcomd 9664 |
. . . . . . . . . . . 12
       |
298 | 297 | oveq1d 6305 |
. . . . . . . . . . 11
                   |
299 | | modmul1 12143 |
. . . . . . . . . . . 12
                                         |
300 | 26, 27, 32, 31, 78, 299 | syl221anc 1279 |
. . . . . . . . . . 11
                   |
301 | | modmul1 12143 |
. . . . . . . . . . . 12
                                         |
302 | 22, 23, 76, 31, 33, 301 | syl221anc 1279 |
. . . . . . . . . . 11
                   |
303 | 298, 300,
302 | 3eqtr4d 2495 |
. . . . . . . . . 10
                   |
304 | | modadd1 12134 |
. . . . . . . . . 10
          
                
                        
         |
305 | 132, 133,
296, 31, 303, 304 | syl221anc 1279 |
. . . . . . . . 9
                   
         |
306 | 111 | negidd 9976 |
. . . . . . . . . 10
     
    |
307 | 306 | oveq1d 6305 |
. . . . . . . . 9
                      |
308 | 295, 305,
307 | 3eqtrd 2489 |
. . . . . . . 8
     
               |
309 | 308, 64 | eqtrd 2485 |
. . . . . . 7
     
         |
310 | | absmod0 13366 |
. . . . . . . 8
     
            
      
       
           |
311 | 134, 31, 310 | syl2anc 667 |
. . . . . . 7
                                 |
312 | 309, 311 | mpbid 214 |
. . . . . 6
                   |
313 | 112 | abscld 13498 |
. . . . . . 7
             |
314 | | mod0 12103 |
. . . . . . 7
                                         
           |
315 | 313, 31, 314 | syl2anc 667 |
. . . . . 6
         
       
       
           |
316 | 312, 315 | mpbid 214 |
. . . . 5
                   |
317 | 291, 316 | eqeltrd 2529 |
. . . 4
        
      |
318 | | absz 13374 |
. . . . 5
     
        
  
       
       |
319 | 135, 318 | syl 17 |
. . . 4
                         |
320 | 317, 319 | mpbird 236 |
. . 3
     
     |
321 | | pellex.neq |
. . . . . . 7
     |
322 | 10 | nnne0d 10654 |
. . . . . . . . 9
   |
323 | 3 | nnne0d 10654 |
. . . . . . . . 9
   |
324 | 9, 11, 2, 4, 322, 323 | divmuleqd 10429 |
. . . . . . . 8
             |
325 | 61 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
     
        |
326 | 325 | eqcomd 2457 |
. . . . . . . . . . . . . 14
 
    
     
        |
327 | 326 | oveq2d 6306 |
. . . . . . . . . . . . 13
 
    
                              |
328 | 9, 11, 322 | divcld 10383 |
. . . . . . . . . . . . . . . 16
     |
329 | 328 | sqcld 12414 |
. . . . . . . . . . . . . . 15
         |
330 | 329 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
        |
331 | 36 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
      |
332 | 38 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
        |
333 | 330, 331,
332 | subdid 10074 |
. . . . . . . . . . . . 13
 
    
            
                                     |
334 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
                   |
335 | 334 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                               |
336 | 335 | adantl 468 |
. . . . . . . . . . . . . . 15
 
    
                          |
337 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
338 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
339 | 323 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
  |
340 | 337, 338,
339 | sqdivd 12429 |
. . . . . . . . . . . . . . . 16
 
    
                  |
341 | 340 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
 
    
                              |
342 | 219 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
      |
343 | | sqne0 12341 |
. . . . . . . . . . . . . . . . . . 19
         |
344 | 4, 343 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         |
345 | 323, 344 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
       |
346 | 345 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
      |
347 | 342, 331,
346 | divcan1d 10384 |
. . . . . . . . . . . . . . 15
 
    
                      |
348 | 336, 341,
347 | 3eqtrd 2489 |
. . . . . . . . . . . . . 14
 
    
                  |
349 | 7 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
  |
350 | 37 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
      |
351 | 330, 349,
350 | mul12d 9842 |
. . . . . . . . . . . . . . 15
 
    
                              |
352 | 9 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
353 | 11 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
354 | 322 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
355 | 352, 353,
354 | sqdivd 12429 |
. . . . . . . . . . . . . . . . 17
 
    
                  |
356 | 355 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
 
    
                              |
357 | 356 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
 
    
                                  |
358 | 206 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
359 | | sqne0 12341 |
. . . . . . . . . . . . . . . . . . . 20
         |
360 | 11, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         |
361 | 322, 360 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
       |
362 | 361 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
363 | 358, 350,
362 | divcan1d 10384 |
. . . . . . . . . . . . . . . 16
 
    
                |