Step | Hyp | Ref
| Expression |
1 | | fzfi 12185 |
. . . . . 6
     |
2 | | ssrab2 3514 |
. . . . . 6
           |
3 | | ssfi 7792 |
. . . . . 6
                      
  |
4 | 1, 2, 3 | mp2an 678 |
. . . . 5
       |
5 | 4 | a1i 11 |
. . . 4
               |
6 | | nnnn0 10876 |
. . . . . . . 8
   |
7 | 6 | 3ad2ant3 1031 |
. . . . . . 7
         |
8 | 2 | sseli 3428 |
. . . . . . . 8
             |
9 | | elfzelz 11800 |
. . . . . . . 8
       |
10 | 8, 9 | syl 17 |
. . . . . . 7
         |
11 | | bccl 12507 |
. . . . . . 7
 
     |
12 | 7, 10, 11 | syl2an 480 |
. . . . . 6
      
            |
13 | 12 | nn0zd 11038 |
. . . . 5
      
            |
14 | | simpl1 1011 |
. . . . . . . . 9
      
              |
15 | | simpl2 1012 |
. . . . . . . . 9
      
          |
16 | | frmx 35761 |
. . . . . . . . . 10
Xrm
          |
17 | 16 | fovcl 6401 |
. . . . . . . . 9
        Xrm    |
18 | 14, 15, 17 | syl2anc 667 |
. . . . . . . 8
      
         Xrm    |
19 | 18 | nn0zd 11038 |
. . . . . . 7
      
         Xrm    |
20 | 8 | adantl 468 |
. . . . . . . 8
      
              |
21 | | fznn0sub 11831 |
. . . . . . . 8
     
   |
22 | 20, 21 | syl 17 |
. . . . . . 7
      
        
   |
23 | | zexpcl 12287 |
. . . . . . 7
  
Xrm      
Xrm         |
24 | 19, 22, 23 | syl2anc 667 |
. . . . . 6
      
         
Xrm         |
25 | | rmspecnonsq 35755 |
. . . . . . . . . . 11
    
      
◻NN  |
26 | 25 | eldifad 3416 |
. . . . . . . . . 10
    
        |
27 | 26 | nnzd 11039 |
. . . . . . . . 9
    
        |
28 | 27 | 3ad2ant1 1029 |
. . . . . . . 8
               |
29 | | breq2 4406 |
. . . . . . . . . . . . . 14
 
   |
30 | 29 | notbid 296 |
. . . . . . . . . . . . 13
 
   |
31 | 30 | elrab 3196 |
. . . . . . . . . . . 12
      
    
   |
32 | 31 | simprbi 466 |
. . . . . . . . . . 11
         |
33 | | 1zzd 10968 |
. . . . . . . . . . 11
         |
34 | | n2dvds1 14354 |
. . . . . . . . . . . 12
 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
         |
36 | | omoe 14762 |
. . . . . . . . . . 11
   
       |
37 | 10, 32, 33, 35, 36 | syl22anc 1269 |
. . . . . . . . . 10
           |
38 | | 2z 10969 |
. . . . . . . . . . . 12
 |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
         |
40 | | 2ne0 10702 |
. . . . . . . . . . . 12
 |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
         |
42 | | peano2zm 10980 |
. . . . . . . . . . . 12
     |
43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
           |
44 | | dvdsval2 14308 |
. . . . . . . . . . 11
               |
45 | 39, 41, 43, 44 | syl3anc 1268 |
. . . . . . . . . 10
       
 
       |
46 | 37, 45 | mpbid 214 |
. . . . . . . . 9
             |
47 | 43 | zred 11040 |
. . . . . . . . . 10
           |
48 | | 0red 9644 |
. . . . . . . . . . . . . . 15
       |
49 | | 3re 10683 |
. . . . . . . . . . . . . . . 16
 |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
51 | 9 | zred 11040 |
. . . . . . . . . . . . . . 15
       |
52 | | 3pos 10703 |
. . . . . . . . . . . . . . . 16
 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
54 | | elfzle1 11802 |
. . . . . . . . . . . . . . 15
       |
55 | 48, 50, 51, 53, 54 | ltletrd 9795 |
. . . . . . . . . . . . . 14
       |
56 | | elnnz 10947 |
. . . . . . . . . . . . . 14

    |
57 | 9, 55, 56 | sylanbrc 670 |
. . . . . . . . . . . . 13
       |
58 | | nnm1nn0 10911 |
. . . . . . . . . . . . 13
     |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
         |
60 | 59 | nn0ge0d 10928 |
. . . . . . . . . . 11
         |
61 | 8, 60 | syl 17 |
. . . . . . . . . 10
           |
62 | | 2re 10679 |
. . . . . . . . . . 11
 |
63 | 62 | a1i 11 |
. . . . . . . . . 10
         |
64 | | 2pos 10701 |
. . . . . . . . . . 11
 |
65 | 64 | a1i 11 |
. . . . . . . . . 10
         |
66 | | divge0 10474 |
. . . . . . . . . 10
    
     
      |
67 | 47, 61, 63, 65, 66 | syl22anc 1269 |
. . . . . . . . 9
             |
68 | | elnn0z 10950 |
. . . . . . . . 9
    
            |
69 | 46, 67, 68 | sylanbrc 670 |
. . . . . . . 8
             |
70 | | zexpcl 12287 |
. . . . . . . 8
                             |
71 | 28, 69, 70 | syl2an 480 |
. . . . . . 7
      
                        |
72 | | frmy 35762 |
. . . . . . . . . 10
Yrm
          |
73 | 72 | fovcl 6401 |
. . . . . . . . 9
        Yrm    |
74 | 14, 15, 73 | syl2anc 667 |
. . . . . . . 8
      
         Yrm    |
75 | | elfzel1 11799 |
. . . . . . . . . . . 12
       |
76 | 9, 75 | zsubcld 11045 |
. . . . . . . . . . 11
         |
77 | | subge0 10127 |
. . . . . . . . . . . . 13
 
   
   |
78 | 51, 49, 77 | sylancl 668 |
. . . . . . . . . . . 12
     
 
   |
79 | 54, 78 | mpbird 236 |
. . . . . . . . . . 11
         |
80 | | elnn0z 10950 |
. . . . . . . . . . 11
  
        |
81 | 76, 79, 80 | sylanbrc 670 |
. . . . . . . . . 10
         |
82 | 8, 81 | syl 17 |
. . . . . . . . 9
           |
83 | 82 | adantl 468 |
. . . . . . . 8
      
            |
84 | | zexpcl 12287 |
. . . . . . . 8
  
Yrm      
Yrm         |
85 | 74, 83, 84 | syl2anc 667 |
. . . . . . 7
      
         
Yrm         |
86 | 71, 85 | zmulcld 11046 |
. . . . . 6
      
                         Yrm          |
87 | 24, 86 | zmulcld 11046 |
. . . . 5
      
           Xrm                       
Yrm           |
88 | 13, 87 | zmulcld 11046 |
. . . 4
      
             
Xrm                        Yrm            |
89 | 5, 88 | fsumzcl 13801 |
. . 3
             
      Xrm                        Yrm            |
90 | 73 | 3adant3 1028 |
. . . 4
        Yrm    |
91 | | 3nn0 10887 |
. . . 4
 |
92 | | zexpcl 12287 |
. . . 4
  
Yrm    
Yrm       |
93 | 90, 91, 92 | sylancl 668 |
. . 3
        
Yrm       |
94 | | dvdsmul2 14325 |
. . 3
               Xrm                        Yrm            Yrm       
Yrm                  
Xrm                        Yrm            Yrm        |
95 | 89, 93, 94 | syl2anc 667 |
. 2
        
Yrm                  
Xrm                        Yrm            Yrm        |
96 | | jm2.22 35850 |
. . . . . 6
        Yrm    
            Xrm    
    
Yrm                        |
97 | 6, 96 | syl3an3 1303 |
. . . . 5
        Yrm    
            Xrm    
    
Yrm                        |
98 | | 1lt3 10778 |
. . . . . . . . . . . 12
 |
99 | | 1re 9642 |
. . . . . . . . . . . . 13
 |
100 | 99, 49 | ltnlei 9755 |
. . . . . . . . . . . 12

  |
101 | 98, 100 | mpbi 212 |
. . . . . . . . . . 11
 |
102 | | elfzle1 11802 |
. . . . . . . . . . 11
       |
103 | 101, 102 | mto 180 |
. . . . . . . . . 10
     |
104 | 103 | a1i 11 |
. . . . . . . . 9
      
      |
105 | 104 | intnanrd 928 |
. . . . . . . 8
               |
106 | | breq2 4406 |
. . . . . . . . . 10
 
   |
107 | 106 | notbid 296 |
. . . . . . . . 9
 
   |
108 | 107 | elrab 3196 |
. . . . . . . 8
      
        |
109 | 105, 108 | sylnibr 307 |
. . . . . . 7
      
        |
110 | | disjsn 4032 |
. . . . . . 7
       
  
        |
111 | 109, 110 | sylibr 216 |
. . . . . 6
             
     |
112 | | simpr 463 |
. . . . . . . . . . 11
       
     
 
   |
113 | 112 | olcd 395 |
. . . . . . . . . 10
       
     
 
           |
114 | | elfznn0 11887 |
. . . . . . . . . . . . . . . 16
       |
115 | 114 | adantr 467 |
. . . . . . . . . . . . . . 15
     
   |
116 | 115 | ad2antlr 733 |
. . . . . . . . . . . . . 14
       
     
     |
117 | | simplrr 771 |
. . . . . . . . . . . . . 14
       
     
  
  |
118 | | simpr 463 |
. . . . . . . . . . . . . 14
       
     
     |
119 | | elnn1uz2 11235 |
. . . . . . . . . . . . . . . 16

        |
120 | | df-ne 2624 |
. . . . . . . . . . . . . . . . . . . . 21

  |
121 | 120 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . 20

  |
122 | 121 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . 19
 

  |
123 | 122 | pm2.21d 110 |
. . . . . . . . . . . . . . . . . 18
 
     |
124 | 123 | imp 431 |
. . . . . . . . . . . . . . . . 17
  

   |
125 | | uzp1 11192 |
. . . . . . . . . . . . . . . . . 18
    
          |
126 | | 1z 10967 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
127 | | dvdsmul1 14324 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
128 | 38, 126, 127 | mp2an 678 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
129 | | 2t1e2 10758 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
130 | 128, 129 | breqtri 4426 |
. . . . . . . . . . . . . . . . . . . . 21
 |
131 | | breq2 4406 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
132 | 131 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
  

 
   |
133 | 130, 132 | mpbiri 237 |
. . . . . . . . . . . . . . . . . . . 20
  

   |
134 | | simpl2 1012 |
. . . . . . . . . . . . . . . . . . . 20
  

   |
135 | 133, 134 | pm2.21dd 178 |
. . . . . . . . . . . . . . . . . . 19
  

   |
136 | | eluzle 11171 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
137 | | 2p1e3 10733 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
138 | 137 | fveq2i 5868 |
. . . . . . . . . . . . . . . . . . . . 21
           |
139 | 136, 138 | eleq2s 2547 |
. . . . . . . . . . . . . . . . . . . 20
      
  |
140 | 139 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
  

      
  |
141 | 135, 140 | jaodan 794 |
. . . . . . . . . . . . . . . . . 18
  

           |
142 | 125, 141 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
  

    
  |
143 | 124, 142 | jaodan 794 |
. . . . . . . . . . . . . . . 16
  

         |
144 | 119, 143 | sylan2b 478 |
. . . . . . . . . . . . . . 15
  


  |
145 | | dvds0 14318 |
. . . . . . . . . . . . . . . . . . 19
   |
146 | 38, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 |
147 | | breq2 4406 |
. . . . . . . . . . . . . . . . . 18
 
   |
148 | 146, 147 | mpbiri 237 |
. . . . . . . . . . . . . . . . 17
   |
149 | 148 | adantl 468 |
. . . . . . . . . . . . . . . 16
  

   |
150 | | simpl2 1012 |
. . . . . . . . . . . . . . . 16
  

   |
151 | 149, 150 | pm2.21dd 178 |
. . . . . . . . . . . . . . 15
  

   |
152 | | elnn0 10871 |
. . . . . . . . . . . . . . . . 17

    |
153 | 152 | biimpi 198 |
. . . . . . . . . . . . . . . 16

    |
154 | 153 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . 15
 
 
   |
155 | 144, 151,
154 | mpjaodan 795 |
. . . . . . . . . . . . . 14
 

  |
156 | 116, 117,
118, 155 | syl3anc 1268 |
. . . . . . . . . . . . 13
       
     
  
  |
157 | | elfzle2 11803 |
. . . . . . . . . . . . . . 15
       |
158 | 157 | adantr 467 |
. . . . . . . . . . . . . 14
     
   |
159 | 158 | ad2antlr 733 |
. . . . . . . . . . . . 13
       
     
  
  |
160 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
       |
161 | 160 | adantr 467 |
. . . . . . . . . . . . . . 15
     
   |
162 | 161 | ad2antlr 733 |
. . . . . . . . . . . . . 14
       
     
     |
163 | | 3z 10970 |
. . . . . . . . . . . . . . 15
 |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
       
     
     |
165 | | nnz 10959 |
. . . . . . . . . . . . . . . 16
   |
166 | 165 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . 15
         |
167 | 166 | ad2antrr 732 |
. . . . . . . . . . . . . 14
       
     
  
  |
168 | | elfz 11790 |
. . . . . . . . . . . . . 14
 
     
     |
169 | 162, 164,
167, 168 | syl3anc 1268 |
. . . . . . . . . . . . 13
       
     
        
    |
170 | 156, 159,
169 | mpbir2and 933 |
. . . . . . . . . . . 12
       
     
         |
171 | 170, 117 | jca 535 |
. . . . . . . . . . 11
       
     
           |
172 | 171 | orcd 394 |
. . . . . . . . . 10
       
     
        
    |
173 | 113, 172 | pm2.61dane 2711 |
. . . . . . . . 9
      
     
 
     
    |
174 | | nn0uz 11193 |
. . . . . . . . . . . . . . 15
     |
175 | 91, 174 | eleqtri 2527 |
. . . . . . . . . . . . . 14
     |
176 | | fzss1 11837 |
. . . . . . . . . . . . . 14
    
          |
177 | 175, 176 | ax-mp 5 |
. . . . . . . . . . . . 13
         |
178 | 177 | sseli 3428 |
. . . . . . . . . . . 12
           |
179 | 178 | anim1i 572 |
. . . . . . . . . . 11
     
     
   |
180 | 179 | adantl 468 |
. . . . . . . . . 10
      
     
 
    
   |
181 | | 0le1 10137 |
. . . . . . . . . . . . 13
 |
182 | 181 | a1i 11 |
. . . . . . . . . . . 12
      
 
  |
183 | | nnge1 10635 |
. . . . . . . . . . . . . 14
   |
184 | 183 | 3ad2ant3 1031 |
. . . . . . . . . . . . 13
         |
185 | 184 | adantr 467 |
. . . . . . . . . . . 12
      
 
  |
186 | | 1zzd 10968 |
. . . . . . . . . . . . 13
      
    |
187 | | 0zd 10949 |
. . . . . . . . . . . . 13
      
    |
188 | 166 | adantr 467 |
. . . . . . . . . . . . 13
      
 
  |
189 | | elfz 11790 |
. . . . . . . . . . . . 13
 
     
     |
190 | 186, 187,
188, 189 | syl3anc 1268 |
. . . . . . . . . . . 12
      
       
    |
191 | 182, 185,
190 | mpbir2and 933 |
. . . . . . . . . . 11
      
        |
192 | 34 | a1i 11 |
. . . . . . . . . . 11
      
 
  |
193 | | eleq1 2517 |
. . . . . . . . . . . . 13
     
       |
194 | | breq2 4406 |
. . . . . . . . . . . . . 14
 
   |
195 | 194 | notbid 296 |
. . . . . . . . . . . . 13
 
   |
196 | 193, 195 | anbi12d 717 |
. . . . . . . . . . . 12
       
         |
197 | 196 | adantl 468 |
. . . . . . . . . . 11
      
       

         |
198 | 191, 192,
197 | mpbir2and 933 |
. . . . . . . . . 10
      
          |
199 | 180, 198 | jaodan 794 |
. . . . . . . . 9
      
              
   |
200 | 173, 199 | impbida 843 |
. . . . . . . 8
             
     
     |
201 | 30 | elrab 3196 |
. . . . . . . 8
      
    
   |
202 | | elun 3574 |
. . . . . . . . 9
          
      
     |
203 | | elsn 3982 |
. . . . . . . . . 10
     |
204 | 31, 203 | orbi12i 524 |
. . . . . . . . 9
       
  
     
    |
205 | 202, 204 | bitri 253 |
. . . . . . . 8
          
     
    |
206 | 200, 201,
205 | 3bitr4g 292 |
. . . . . . 7
             
      
      |
207 | 206 | eqrdv 2449 |
. . . . . 6
                   
     |
208 | | fzfi 12185 |
. . . . . . . 8
     |
209 | | ssrab2 3514 |
. . . . . . . 8
           |
210 | | ssfi 7792 |
. . . . . . . 8
                      
  |
211 | 208, 209,
210 | mp2an 678 |
. . . . . . 7
       |
212 | 211 | a1i 11 |
. . . . . 6
               |
213 | 209 | sseli 3428 |
. . . . . . . . . 10
             |
214 | 213, 160 | syl 17 |
. . . . . . . . 9
         |
215 | 7, 214, 11 | syl2an 480 |
. . . . . . . 8
      
            |
216 | 215 | nn0cnd 10927 |
. . . . . . 7
      
            |
217 | 17 | 3adant3 1028 |
. . . . . . . . . . 11
        Xrm    |
218 | 217 | nn0cnd 10927 |
. . . . . . . . . 10
        Xrm    |
219 | 218 | adantr 467 |
. . . . . . . . 9
      
         Xrm    |
220 | 213 | adantl 468 |
. . . . . . . . . 10
      
              |
221 | | fznn0sub 11831 |
. . . . . . . . . 10
     
   |
222 | 220, 221 | syl 17 |
. . . . . . . . 9
      
        
   |
223 | 219, 222 | expcld 12416 |
. . . . . . . 8
      
         
Xrm         |
224 | 90 | zcnd 11041 |
. . . . . . . . . 10
        Yrm    |
225 | 213, 114 | syl 17 |
. . . . . . . . . 10
         |
226 | | expcl 12290 |
. . . . . . . . . 10
  
Yrm    
Yrm       |
227 | 224, 225,
226 | syl2an 480 |
. . . . . . . . 9
      
         
Yrm       |
228 | | rmspecpos 35764 |
. . . . . . . . . . . 12
    
        |
229 | 228 | rpcnd 11343 |
. . . . . . . . . . 11
    
        |
230 | 229 | 3ad2ant1 1029 |
. . . . . . . . . 10
               |
231 | 201 | simprbi 466 |
. . . . . . . . . . . . 13
         |
232 | | 1zzd 10968 |
. . . . . . . . . . . . 13
         |
233 | 34 | a1i 11 |
. . . . . . . . . . . . 13
         |
234 | 214, 231,
232, 233, 36 | syl22anc 1269 |
. . . . . . . . . . . 12
           |
235 | 38 | a1i 11 |
. . . . . . . . . . . . 13
         |
236 | 40 | a1i 11 |
. . . . . . . . . . . . 13
         |
237 | 214, 42 | syl 17 |
. . . . . . . . . . . . 13
           |
238 | 235, 236,
237, 44 | syl3anc 1268 |
. . . . . . . . . . . 12
       
 
       |
239 | 234, 238 | mpbid 214 |
. . . . . . . . . . 11
             |
240 | 237 | zred 11040 |
. . . . . . . . . . . 12
           |
241 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     
   |
242 | 241 | con3dimp 443 |
. . . . . . . . . . . . . . . 16
     

  |
243 | 201, 242 | sylbi 199 |
. . . . . . . . . . . . . . 15
      
  |
244 | 225, 153 | syl 17 |
. . . . . . . . . . . . . . 15
       
   |
245 | | orel2 385 |
. . . . . . . . . . . . . . 15
       |
246 | 243, 244,
245 | sylc 62 |
. . . . . . . . . . . . . 14
         |
247 | 246, 58 | syl 17 |
. . . . . . . . . . . . 13
           |
248 | 247 | nn0ge0d 10928 |
. . . . . . . . . . . 12
           |
249 | 62 | a1i 11 |
. . . . . . . . . . . 12
         |
250 | 64 | a1i 11 |
. . . . . . . . . . . 12
         |
251 | 240, 248,
249, 250, 66 | syl22anc 1269 |
. . . . . . . . . . 11
             |
252 | 239, 251,
68 | sylanbrc 670 |
. . . . . . . . . 10
             |
253 | | expcl 12290 |
. . . . . . . . . 10
                             |
254 | 230, 252,
253 | syl2an 480 |
. . . . . . . . 9
      
                        |
255 | 227, 254 | mulcld 9663 |
. . . . . . . 8
      
           Yrm                      |
256 | 223, 255 | mulcld 9663 |
. . . . . . 7
      
           Xrm          Yrm                       |
257 | 216, 256 | mulcld 9663 |
. . . . . 6
      
             
Xrm          Yrm                        |
258 | 111, 207,
212, 257 | fsumsplit 13806 |
. . . . 5
             
      Xrm          Yrm                                    Xrm          Yrm                      
        Xrm          Yrm                         |
259 | | expcl 12290 |
. . . . . . . . 9
  
Yrm    
Yrm       |
260 | 224, 91, 259 | sylancl 668 |
. . . . . . . 8
        
Yrm       |
261 | 88 | zcnd 11041 |
. . . . . . . 8
      
             
Xrm                        Yrm            |
262 | 5, 260, 261 | fsummulc1 13846 |
. . . . . . 7
                    
Xrm                        Yrm            Yrm            
      
Xrm                        Yrm            Yrm        |
263 | 12 | nn0cnd 10927 |
. . . . . . . . . 10
      
            |
264 | 218 | adantr 467 |
. . . . . . . . . . . 12
      
         Xrm    |
265 | 264, 22 | expcld 12416 |
. . . . . . . . . . 11
      
         
Xrm         |
266 | 230, 69, 253 | syl2an 480 |
. . . . . . . . . . . 12
      
                        |
267 | | expcl 12290 |
. . . . . . . . . . . . 13
  
Yrm      
Yrm         |
268 | 224, 82, 267 | syl2an 480 |
. . . . . . . . . . . 12
      
         
Yrm         |
269 | 266, 268 | mulcld 9663 |
. . . . . . . . . . 11
      
                         Yrm          |
270 | 265, 269 | mulcld 9663 |
. . . . . . . . . 10
      
           Xrm                       
Yrm           |
271 | 260 | adantr 467 |
. . . . . . . . . 10
      
         
Yrm       |
272 | 263, 270,
271 | mulassd 9666 |
. . . . . . . . 9
      
               Xrm                       
Yrm            Yrm             Xrm                       
Yrm           Yrm         |
273 | 265, 269,
271 | mulassd 9666 |
. . . . . . . . . . 11
      
            Xrm                        Yrm           Yrm         Xrm                         Yrm          Yrm         |
274 | 266, 268,
271 | mulassd 9666 |
. . . . . . . . . . . . 13
      
                         
Yrm          Yrm                        Yrm         Yrm         |
275 | 268, 271 | mulcld 9663 |
. . . . . . . . . . . . . 14
      
           Yrm         Yrm        |
276 | 266, 275 | mulcomd 9664 |
. . . . . . . . . . . . 13
      
                         
Yrm        
Yrm          
Yrm        
Yrm                       |
277 | 224 | adantr 467 |
. . . . . . . . . . . . . . . 16
      
         Yrm    |
278 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
      
          |
279 | 277, 278,
83 | expaddd 12418 |
. . . . . . . . . . . . . . 15
      
         
Yrm            Yrm         Yrm        |
280 | 10 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
      
          |
281 | 280 | zcnd 11041 |
. . . . . . . . . . . . . . . . 17
      
          |
282 | | 3cn 10684 |
. . . . . . . . . . . . . . . . 17
 |
283 | | npcan 9884 |
. . . . . . . . . . . . . . . . 17
 
       |
284 | 281, 282,
283 | sylancl 668 |
. . . . . . . . . . . . . . . 16
      
              |
285 | 284 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
      
         
Yrm          
Yrm       |
286 | 279, 285 | eqtr3d 2487 |
. . . . . . . . . . . . . 14
      
           Yrm         Yrm        Yrm       |
287 | 286 | oveq1d 6305 |
. . . . . . . . . . . . 13
      
            Yrm         Yrm                        Yrm                      |
288 | 274, 276,
287 | 3eqtrd 2489 |
. . . . . . . . . . . 12
      
                         
Yrm          Yrm         Yrm                      |
289 | 288 | oveq2d 6306 |
. . . . . . . . . . 11
      
           Xrm                         Yrm          Yrm          Xrm          Yrm                       |
290 | 273, 289 | eqtrd 2485 |
. . . . . . . . . 10
      
            Xrm                        Yrm           Yrm         Xrm          Yrm                       |
291 | 290 | oveq2d 6306 |
. . . . . . . . 9
      
               Xrm                       
Yrm           Yrm            
Xrm          Yrm                        |
292 | 272, 291 | eqtrd 2485 |
. . . . . . . 8
      
               Xrm                       
Yrm            Yrm           
Xrm          Yrm                        |
293 | 292 | sumeq2dv 13769 |
. . . . . . 7
             
      
Xrm                        Yrm            Yrm            
      Xrm          Yrm                        |
294 | 262, 293 | eqtr2d 2486 |
. . . . . 6
             
      Xrm          Yrm                                    Xrm                        Yrm           
Yrm        |
295 | | 1nn 10620 |
. . . . . . 7
 |
296 | | bccl 12507 |
. . . . . . . . . . 11
 
     |
297 | 6, 126, 296 | sylancl 668 |
. . . . . . . . . 10
     |
298 | 297 | nn0cnd 10927 |
. . . . . . . . 9
     |
299 | 298 | 3ad2ant3 1031 |
. . . . . . . 8
           |
300 | | nnm1nn0 10911 |
. . . . . . . . . . 11
 
   |
301 | 300 | 3ad2ant3 1031 |
. . . . . . . . . 10
       
   |
302 | 218, 301 | expcld 12416 |
. . . . . . . . 9
        
Xrm         |
303 | | 1nn0 10885 |
. . . . . . . . . . 11
 |
304 | | expcl 12290 |
. . . . . . . . . . 11
  
Yrm    
Yrm       |
305 | 224, 303,
304 | sylancl 668 |
. . . . . . . . . 10
        
Yrm       |
306 | | 1m1e0 10678 |
. . . . . . . . . . . . . 14
   |
307 | 306 | oveq1i 6300 |
. . . . . . . . . . . . 13
       |
308 | | 2cn 10680 |
. . . . . . . . . . . . . 14
 |
309 | 308, 40 | div0i 10341 |
. . . . . . . . . . . . 13
   |
310 | 307, 309 | eqtri 2473 |
. . . . . . . . . . . 12
     |
311 | | 0nn0 10884 |
. . . . . . . . . . . 12
 |
312 | 310, 311 | eqeltri 2525 |
. . . . . . . . . . 11
     |
313 | | expcl 12290 |
. . . . . . . . . . 11
                             |
314 | 230, 312,
313 | sylancl 668 |
. . . . . . . . . 10
                       |
315 | 305, 314 | mulcld 9663 |
. . . . . . . . 9
          Yrm                      |
316 | 302, 315 | mulcld 9663 |
. . . . . . . 8
          Xrm          Yrm                       |
317 | 299, 316 | mulcld 9663 |
. . . . . . 7
            
Xrm          Yrm                        |
318 | | oveq2 6298 |
. . . . . . . . 9
       |
319 | | oveq2 6298 |
. . . . . . . . . . 11
 
     |
320 | 319 | oveq2d 6306 |
. . . . . . . . . 10
  
Xrm        
Xrm         |
321 | | oveq2 6298 |
. . . . . . . . . . 11
  
Yrm      
Yrm       |
322 | | oveq1 6297 |
. . . . . . . . . . . . 13
       |
323 | 322 | oveq1d 6305 |
. . . . . . . . . . . 12
           |
324 | 323 | oveq2d 6306 |
. . . . . . . . . . 11
                               |
325 | 321, 324 | oveq12d 6308 |
. . . . . . . . . 10
    Yrm                       Yrm                      |
326 | 320, 325 | oveq12d 6308 |
. . . . . . . . 9
    Xrm          Yrm                        Xrm    
    
Yrm                       |
327 | 318, 326 | oveq12d 6308 |
. . . . . . . 8
      
Xrm          Yrm                            Xrm          Yrm                        |
328 | 327 | sumsn 13807 |
. . . . . . 7
        Xrm          Yrm                                Xrm    
    
Yrm                            Xrm          Yrm                        |
329 | 295, 317,
328 | sylancr 669 |
. . . . . 6
               
Xrm          Yrm                            Xrm          Yrm                        |
330 | 294, 329 | oveq12d 6308 |
. . . . 5
                    
Xrm          Yrm                               Xrm    
    
Yrm                         
            Xrm    
                   Yrm            Yrm            Xrm          Yrm                         |
331 | 97, 258, 330 | 3eqtrd 2489 |
. . . 4
        Yrm                   Xrm                        Yrm           
Yrm            Xrm          Yrm                         |
332 | | bcn1 12498 |
. . . . . . 7

    |
333 | 7, 332 | syl 17 |
. . . . . 6
           |
334 | 333 | eqcomd 2457 |
. . . . 5
           |
335 | 224 | exp1d 12411 |
. . . . . . . 8
        
Yrm      Yrm    |
336 | 310 | a1i 11 |
. . . . . . . . . 10
             |
337 | 336 | oveq2d 6306 |
. . . . . . . . 9
                                 |
338 | 230 | exp0d 12410 |
. . . . . . . . 9
                   |
339 | 337, 338 | eqtrd 2485 |
. . . . . . . 8
                       |
340 | 335, 339 | oveq12d 6308 |
. . . . . . 7
          Yrm                     
Yrm     |
341 | 224 | mulid1d 9660 |
. . . . . . 7
        
Yrm    Yrm    |
342 | 340, 341 | eqtr2d 2486 |
. . . . . 6
        Yrm     Yrm                      |
343 | 342 | oveq2d 6306 |
. . . . 5
          Xrm       
Yrm      Xrm    
    
Yrm                       |
344 | 334, 343 | oveq12d 6308 |
. . . 4
       
  
Xrm        Yrm          Xrm          Yrm                        |
345 | 331, 344 | oveq12d 6308 |
. . 3
        
Yrm    
   Xrm       
Yrm              
      Xrm                        Yrm           
Yrm            Xrm          Yrm                            
Xrm          Yrm                         |
346 | 5, 261 | fsumcl 13799 |
. . . . 5
             
      Xrm                        Yrm            |
347 | 346, 260 | mulcld 9663 |
. . . 4
                    
Xrm                        Yrm            Yrm        |
348 | 347, 317 | pncand 9987 |
. . 3
                
      Xrm                        Yrm           
Yrm            Xrm          Yrm                            
Xrm          Yrm                        
            Xrm    
                   Yrm            Yrm        |
349 | 345, 348 | eqtrd 2485 |
. 2
        
Yrm    
   Xrm       
Yrm                   Xrm                        Yrm           
Yrm        |
350 | 95, 349 | breqtrrd 4429 |
1
        
Yrm      
Yrm    
   Xrm       
Yrm       |