Step | Hyp | Ref
| Expression |
1 | | oveq1 5878 |
. . . . . . . . . . . . . 14
 
    
    |
2 | 1 | eqeq1d 2186 |
. . . . . . . . . . . . 13
   
  
      |
3 | | phimul.6 |
. . . . . . . . . . . . 13
       |
4 | 2, 3 | elrab2 2896 |
. . . . . . . . . . . 12



      |
5 | 4 | simplbi 274 |
. . . . . . . . . . 11
   |
6 | 5 | adantl 277 |
. . . . . . . . . 10
 
   |
7 | | elfzoelz 10141 |
. . . . . . . . . . . . . . 15
  ..^  
  |
8 | | crth.1 |
. . . . . . . . . . . . . . 15
 ..^    |
9 | 7, 8 | eleq2s 2272 |
. . . . . . . . . . . . . 14
   |
10 | 6, 9 | syl 14 |
. . . . . . . . . . . . 13
 
   |
11 | | zq 9621 |
. . . . . . . . . . . . 13
   |
12 | 10, 11 | syl 14 |
. . . . . . . . . . . 12
 
   |
13 | | crth.4 |
. . . . . . . . . . . . . . 15
  
    |
14 | 13 | simp1d 1009 |
. . . . . . . . . . . . . 14
   |
15 | 14 | adantr 276 |
. . . . . . . . . . . . 13
 
   |
16 | | nnq 9628 |
. . . . . . . . . . . . 13
   |
17 | 15, 16 | syl 14 |
. . . . . . . . . . . 12
 
   |
18 | 15 | nngt0d 8958 |
. . . . . . . . . . . 12
 
   |
19 | 12, 17, 18 | modqcld 10322 |
. . . . . . . . . . 11
 
 
   |
20 | 13 | simp2d 1010 |
. . . . . . . . . . . . . 14
   |
21 | 20 | adantr 276 |
. . . . . . . . . . . . 13
 
   |
22 | | nnq 9628 |
. . . . . . . . . . . . 13
   |
23 | 21, 22 | syl 14 |
. . . . . . . . . . . 12
 
   |
24 | 21 | nngt0d 8958 |
. . . . . . . . . . . 12
 
   |
25 | 12, 23, 24 | modqcld 10322 |
. . . . . . . . . . 11
 
 
   |
26 | | opexg 4227 |
. . . . . . . . . . 11
    
           |
27 | 19, 25, 26 | syl2anc 411 |
. . . . . . . . . 10
 
  
    
  |
28 | | oveq1 5878 |
. . . . . . . . . . . 12
 
     |
29 | | oveq1 5878 |
. . . . . . . . . . . 12
 
     |
30 | 28, 29 | opeq12d 3786 |
. . . . . . . . . . 11
  
    
         |
31 | | crth.3 |
. . . . . . . . . . 11
          |
32 | 30, 31 | fvmptg 5590 |
. . . . . . . . . 10
                       |
33 | 6, 27, 32 | syl2anc 411 |
. . . . . . . . 9
 
              |
34 | 5, 8 | eleqtrdi 2270 |
. . . . . . . . . . . . . 14
  ..^     |
35 | 34 | adantl 277 |
. . . . . . . . . . . . 13
 
  ..^     |
36 | 35, 7 | syl 14 |
. . . . . . . . . . . 12
 
   |
37 | | zmodfzo 10341 |
. . . . . . . . . . . 12
 
    ..^   |
38 | 36, 15, 37 | syl2anc 411 |
. . . . . . . . . . 11
 
 
  ..^   |
39 | | modgcd 11983 |
. . . . . . . . . . . . 13
 
         |
40 | 36, 15, 39 | syl2anc 411 |
. . . . . . . . . . . 12
 
   
     |
41 | 15 | nnzd 9369 |
. . . . . . . . . . . . . . . . 17
 
   |
42 | | gcddvds 11955 |
. . . . . . . . . . . . . . . . 17
 
    
    |
43 | 36, 41, 42 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
   

    |
44 | 43 | simpld 112 |
. . . . . . . . . . . . . . 15
 
 
   |
45 | | nnne0 8942 |
. . . . . . . . . . . . . . . . . . 19
   |
46 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
     |
47 | 46 | necon3ai 2396 |
. . . . . . . . . . . . . . . . . . 19
 
   |
48 | 15, 45, 47 | 3syl 17 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
49 | | gcdn0cl 11954 |
. . . . . . . . . . . . . . . . . 18
           |
50 | 36, 41, 48, 49 | syl21anc 1237 |
. . . . . . . . . . . . . . . . 17
 
 
   |
51 | 50 | nnzd 9369 |
. . . . . . . . . . . . . . . 16
 
 
   |
52 | 21 | nnzd 9369 |
. . . . . . . . . . . . . . . 16
 
   |
53 | 43 | simprd 114 |
. . . . . . . . . . . . . . . 16
 
 
   |
54 | 51, 41, 52, 53 | dvdsmultr1d 11831 |
. . . . . . . . . . . . . . 15
 
 
     |
55 | 15, 21 | nnmulcld 8963 |
. . . . . . . . . . . . . . . . 17
 
 
   |
56 | 55 | nnzd 9369 |
. . . . . . . . . . . . . . . 16
 
 
   |
57 | | nnne0 8942 |
. . . . . . . . . . . . . . . . 17
   
   |
58 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
         |
59 | 58 | necon3ai 2396 |
. . . . . . . . . . . . . . . . 17
   
     |
60 | 55, 57, 59 | 3syl 17 |
. . . . . . . . . . . . . . . 16
 
 
     |
61 | | dvdslegcd 11956 |
. . . . . . . . . . . . . . . 16
    

  
   
   

     
       |
62 | 51, 36, 56, 60, 61 | syl31anc 1241 |
. . . . . . . . . . . . . . 15
 
     
     
       |
63 | 44, 54, 62 | mp2and 433 |
. . . . . . . . . . . . . 14
 
 
  
    |
64 | 4 | simprbi 275 |
. . . . . . . . . . . . . . 15
 
     |
65 | 64 | adantl 277 |
. . . . . . . . . . . . . 14
 
 
     |
66 | 63, 65 | breqtrd 4028 |
. . . . . . . . . . . . 13
 
 
   |
67 | | nnle1eq1 8938 |
. . . . . . . . . . . . . 14
     
     |
68 | 50, 67 | syl 14 |
. . . . . . . . . . . . 13
 
   
     |
69 | 66, 68 | mpbid 147 |
. . . . . . . . . . . 12
 
 
   |
70 | 40, 69 | eqtrd 2210 |
. . . . . . . . . . 11
 
   
   |
71 | | oveq1 5878 |
. . . . . . . . . . . . 13
  
    
   |
72 | 71 | eqeq1d 2186 |
. . . . . . . . . . . 12
  
 

 
     |
73 | | phimul.4 |
. . . . . . . . . . . 12
  ..^     |
74 | 72, 73 | elrab2 2896 |
. . . . . . . . . . 11
  
 
  ..^        |
75 | 38, 70, 74 | sylanbrc 417 |
. . . . . . . . . 10
 
 
   |
76 | | zmodfzo 10341 |
. . . . . . . . . . . 12
 
    ..^   |
77 | 36, 21, 76 | syl2anc 411 |
. . . . . . . . . . 11
 
 
  ..^   |
78 | | modgcd 11983 |
. . . . . . . . . . . . 13
 
         |
79 | 36, 21, 78 | syl2anc 411 |
. . . . . . . . . . . 12
 
   
     |
80 | | gcddvds 11955 |
. . . . . . . . . . . . . . . . 17
 
    
    |
81 | 36, 52, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
   

    |
82 | 81 | simpld 112 |
. . . . . . . . . . . . . . 15
 
 
   |
83 | 81 | simprd 114 |
. . . . . . . . . . . . . . . 16
 
 
   |
84 | | dvdsmul2 11813 |
. . . . . . . . . . . . . . . . 17
 
     |
85 | 41, 52, 84 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
     |
86 | | nnne0 8942 |
. . . . . . . . . . . . . . . . . . . 20
   |
87 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
     |
88 | 87 | necon3ai 2396 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
89 | 21, 86, 88 | 3syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
90 | | gcdn0cl 11954 |
. . . . . . . . . . . . . . . . . . 19
           |
91 | 36, 52, 89, 90 | syl21anc 1237 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
92 | 91 | nnzd 9369 |
. . . . . . . . . . . . . . . . 17
 
 
   |
93 | | dvdstr 11827 |
. . . . . . . . . . . . . . . . 17
   

          
     |
94 | 92, 52, 56, 93 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
 
         
     |
95 | 83, 85, 94 | mp2and 433 |
. . . . . . . . . . . . . . 15
 
 
     |
96 | | dvdslegcd 11956 |
. . . . . . . . . . . . . . . 16
    

  
   
   

     
       |
97 | 92, 36, 56, 60, 96 | syl31anc 1241 |
. . . . . . . . . . . . . . 15
 
     
     
       |
98 | 82, 95, 97 | mp2and 433 |
. . . . . . . . . . . . . 14
 
 
  
    |
99 | 98, 65 | breqtrd 4028 |
. . . . . . . . . . . . 13
 
 
   |
100 | | nnle1eq1 8938 |
. . . . . . . . . . . . . 14
     
     |
101 | 91, 100 | syl 14 |
. . . . . . . . . . . . 13
 
   
     |
102 | 99, 101 | mpbid 147 |
. . . . . . . . . . . 12
 
 
   |
103 | 79, 102 | eqtrd 2210 |
. . . . . . . . . . 11
 
   
   |
104 | | oveq1 5878 |
. . . . . . . . . . . . 13
  
    
   |
105 | 104 | eqeq1d 2186 |
. . . . . . . . . . . 12
  
 

 
     |
106 | | phimul.5 |
. . . . . . . . . . . 12
  ..^     |
107 | 105, 106 | elrab2 2896 |
. . . . . . . . . . 11
  
 
  ..^        |
108 | 77, 103, 107 | sylanbrc 417 |
. . . . . . . . . 10
 
 
   |
109 | | opelxpi 4657 |
. . . . . . . . . 10
    
             |
110 | 75, 108, 109 | syl2anc 411 |
. . . . . . . . 9
 
  
    
    |
111 | 33, 110 | eqeltrd 2254 |
. . . . . . . 8
 
         |
112 | 111 | ralrimiva 2550 |
. . . . . . 7
          |
113 | | crth.2 |
. . . . . . . . . 10
  ..^  ..^   |
114 | 8, 113, 31, 13 | crth 12215 |
. . . . . . . . 9
       |
115 | | f1ofn 5460 |
. . . . . . . . 9
    
  |
116 | | fnfun 5311 |
. . . . . . . . 9
   |
117 | 114, 115,
116 | 3syl 17 |
. . . . . . . 8
   |
118 | | ssrab2 3240 |
. . . . . . . . . 10
       |
119 | 3, 118 | eqsstri 3187 |
. . . . . . . . 9
 |
120 | | fndm 5313 |
. . . . . . . . . 10
   |
121 | 114, 115,
120 | 3syl 17 |
. . . . . . . . 9
   |
122 | 119, 121 | sseqtrrid 3206 |
. . . . . . . 8

  |
123 | | funimass4 5564 |
. . . . . . . 8
         

         |
124 | 117, 122,
123 | syl2anc 411 |
. . . . . . 7
       

         |
125 | 112, 124 | mpbird 167 |
. . . . . 6
    
    |
126 | | ssrab2 3240 |
. . . . . . . . . . . . . 14
  ..^     ..^  |
127 | 73, 126 | eqsstri 3187 |
. . . . . . . . . . . . 13
 ..^  |
128 | | ssrab2 3240 |
. . . . . . . . . . . . . 14
  ..^     ..^  |
129 | 106, 128 | eqsstri 3187 |
. . . . . . . . . . . . 13
 ..^  |
130 | | xpss12 4732 |
. . . . . . . . . . . . 13
 
 ..^  ..^ 
    ..^  ..^    |
131 | 127, 129,
130 | mp2an 426 |
. . . . . . . . . . . 12
    ..^  ..^   |
132 | 131, 113 | sseqtrri 3190 |
. . . . . . . . . . 11
   |
133 | 132 | sseli 3151 |
. . . . . . . . . 10
     |
134 | | f1ocnvfv2 5775 |
. . . . . . . . . 10
     
            |
135 | 114, 133,
134 | syl2an 289 |
. . . . . . . . 9
 

             |
136 | | f1ocnv 5472 |
. . . . . . . . . . . . 13
    
       |
137 | | f1of 5459 |
. . . . . . . . . . . . 13
             |
138 | 114, 136,
137 | 3syl 17 |
. . . . . . . . . . . 12
        |
139 | | ffvelcdm 5647 |
. . . . . . . . . . . 12
      
        |
140 | 138, 133,
139 | syl2an 289 |
. . . . . . . . . . 11
 

         |
141 | 140, 8 | eleqtrdi 2270 |
. . . . . . . . . . . . . . 15
 

        ..^     |
142 | | elfzoelz 10141 |
. . . . . . . . . . . . . . 15
       ..^  
       |
143 | 141, 142 | syl 14 |
. . . . . . . . . . . . . 14
 

         |
144 | 14 | adantr 276 |
. . . . . . . . . . . . . 14
 

    |
145 | | modgcd 11983 |
. . . . . . . . . . . . . 14
                          |
146 | 143, 144,
145 | syl2anc 411 |
. . . . . . . . . . . . 13
 

         
          |
147 | | zq 9621 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
148 | 143, 147 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
 

         |
149 | 144, 16 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
150 | 144 | nngt0d 8958 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
151 | 148, 149,
150 | modqcld 10322 |
. . . . . . . . . . . . . . . . . . . . 21
 

           |
152 | 20 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

    |
153 | 152, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
154 | 152 | nngt0d 8958 |
. . . . . . . . . . . . . . . . . . . . . 22
 

    |
155 | 148, 153,
154 | modqcld 10322 |
. . . . . . . . . . . . . . . . . . . . 21
 

           |
156 | | opexg 4227 |
. . . . . . . . . . . . . . . . . . . . 21
                                    |
157 | 151, 155,
156 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
 

                     |
158 | | oveq1 5878 |
. . . . . . . . . . . . . . . . . . . . . 22
      
          |
159 | | oveq1 5878 |
. . . . . . . . . . . . . . . . . . . . . 22
      
          |
160 | 158, 159 | opeq12d 3786 |
. . . . . . . . . . . . . . . . . . . . 21
       
    
                   |
161 | 30 | cbvmptv 4098 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                |
162 | 31, 161 | eqtri 2198 |
. . . . . . . . . . . . . . . . . . . . 21
          |
163 | 160, 162 | fvmptg 5590 |
. . . . . . . . . . . . . . . . . . . 20
                                                     |
164 | 140, 157,
163 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
 

                              |
165 | 135, 164 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . 18
 

                     |
166 | | simpr 110 |
. . . . . . . . . . . . . . . . . 18
 

      |
167 | 165, 166 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . 17
 

                       |
168 | | opelxp 4655 |
. . . . . . . . . . . . . . . . 17
                                      |
169 | 167, 168 | sylib 122 |
. . . . . . . . . . . . . . . 16
 

                    |
170 | 169 | simpld 112 |
. . . . . . . . . . . . . . 15
 

           |
171 | | oveq1 5878 |
. . . . . . . . . . . . . . . . 17
                 
   |
172 | 171 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
                       |
173 | 172, 73 | elrab2 2896 |
. . . . . . . . . . . . . . 15
       
         ..^        
    |
174 | 170, 173 | sylib 122 |
. . . . . . . . . . . . . 14
 

           ..^        
    |
175 | 174 | simprd 114 |
. . . . . . . . . . . . 13
 

         
   |
176 | 146, 175 | eqtr3d 2212 |
. . . . . . . . . . . 12
 

           |
177 | | modgcd 11983 |
. . . . . . . . . . . . . 14
                          |
178 | 143, 152,
177 | syl2anc 411 |
. . . . . . . . . . . . 13
 

         
          |
179 | 169 | simprd 114 |
. . . . . . . . . . . . . . 15
 

           |
180 | | oveq1 5878 |
. . . . . . . . . . . . . . . . 17
                 
   |
181 | 180 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
                       |
182 | 181, 106 | elrab2 2896 |
. . . . . . . . . . . . . . 15
       
         ..^        
    |
183 | 179, 182 | sylib 122 |
. . . . . . . . . . . . . 14
 

           ..^        
    |
184 | 183 | simprd 114 |
. . . . . . . . . . . . 13
 

         
   |
185 | 178, 184 | eqtr3d 2212 |
. . . . . . . . . . . 12
 

           |
186 | 14 | nnzd 9369 |
. . . . . . . . . . . . . 14
   |
187 | 186 | adantr 276 |
. . . . . . . . . . . . 13
 

    |
188 | 20 | nnzd 9369 |
. . . . . . . . . . . . . 14
   |
189 | 188 | adantr 276 |
. . . . . . . . . . . . 13
 

    |
190 | | rpmul 12089 |
. . . . . . . . . . . . 13
      
                        
     |
191 | 143, 187,
189, 190 | syl3anc 1238 |
. . . . . . . . . . . 12
 

                         
     |
192 | 176, 185,
191 | mp2and 433 |
. . . . . . . . . . 11
 

        
    |
193 | | oveq1 5878 |
. . . . . . . . . . . . 13
      
         
    |
194 | 193 | eqeq1d 2186 |
. . . . . . . . . . . 12
        
        
     |
195 | 194, 3 | elrab2 2896 |
. . . . . . . . . . 11
     
            
     |
196 | 140, 192,
195 | sylanbrc 417 |
. . . . . . . . . 10
 

         |
197 | | funfvima2 5746 |
. . . . . . . . . . . 12
                         |
198 | 117, 122,
197 | syl2anc 411 |
. . . . . . . . . . 11
                       |
199 | 198 | imp 124 |
. . . . . . . . . 10
 
                     |
200 | 196, 199 | syldan 282 |
. . . . . . . . 9
 

                 |
201 | 135, 200 | eqeltrrd 2255 |
. . . . . . . 8
 

        |
202 | 201 | ex 115 |
. . . . . . 7
           |
203 | 202 | ssrdv 3161 |
. . . . . 6
  
      |
204 | 125, 203 | eqssd 3172 |
. . . . 5
         |
205 | | f1of1 5458 |
. . . . . . 7
    
      |
206 | 114, 205 | syl 14 |
. . . . . 6
       |
207 | 119 | a1i 9 |
. . . . . 6

  |
208 | | 0z 9259 |
. . . . . . . . . 10
 |
209 | 186, 188 | zmulcld 9376 |
. . . . . . . . . 10
     |
210 | | fzofig 10426 |
. . . . . . . . . 10
  
   ..^     |
211 | 208, 209,
210 | sylancr 414 |
. . . . . . . . 9
  ..^     |
212 | 8, 211 | eqeltrid 2264 |
. . . . . . . 8
   |
213 | | elfzoelz 10141 |
. . . . . . . . . . . . . 14
  ..^  
  |
214 | 213, 8 | eleq2s 2272 |
. . . . . . . . . . . . 13
   |
215 | 214 | adantl 277 |
. . . . . . . . . . . 12
 
   |
216 | 209 | adantr 276 |
. . . . . . . . . . . 12
 
 
   |
217 | 215, 216 | gcdcld 11960 |
. . . . . . . . . . 11
 
 
     |
218 | 217 | nn0zd 9368 |
. . . . . . . . . 10
 
 
     |
219 | | 1zzd 9275 |
. . . . . . . . . 10
 
   |
220 | | zdceq 9323 |
. . . . . . . . . 10
   
 
 DECID       |
221 | 218, 219,
220 | syl2anc 411 |
. . . . . . . . 9
 

DECID  
    |
222 | 221 | ralrimiva 2550 |
. . . . . . . 8
  DECID 
     |
223 | 212, 222 | ssfirab 6929 |
. . . . . . 7
         |
224 | 3, 223 | eqeltrid 2264 |
. . . . . 6
   |
225 | | f1imaeng 6788 |
. . . . . 6
     
    
  |
226 | 206, 207,
224, 225 | syl3anc 1238 |
. . . . 5
    
  |
227 | 204, 226 | eqbrtrrd 4026 |
. . . 4
  
  |
228 | | fzofig 10426 |
. . . . . . . . 9
 
  ..^   |
229 | 208, 186,
228 | sylancr 414 |
. . . . . . . 8
  ..^   |
230 | | elfzoelz 10141 |
. . . . . . . . . . . . 13
  ..^
  |
231 | 230 | adantl 277 |
. . . . . . . . . . . 12
 
 ..^    |
232 | 186 | adantr 276 |
. . . . . . . . . . . 12
 
 ..^    |
233 | 231, 232 | gcdcld 11960 |
. . . . . . . . . . 11
 
 ..^      |
234 | 233 | nn0zd 9368 |
. . . . . . . . . 10
 
 ..^      |
235 | | 1z 9274 |
. . . . . . . . . 10
 |
236 | | zdceq 9323 |
. . . . . . . . . 10
   
 DECID     |
237 | 234, 235,
236 | sylancl 413 |
. . . . . . . . 9
 
 ..^  DECID     |
238 | 237 | ralrimiva 2550 |
. . . . . . . 8
   ..^ DECID     |
239 | 229, 238 | ssfirab 6929 |
. . . . . . 7
   ..^      |
240 | 73, 239 | eqeltrid 2264 |
. . . . . 6
   |
241 | | fzofig 10426 |
. . . . . . . . 9
 
  ..^   |
242 | 208, 188,
241 | sylancr 414 |
. . . . . . . 8
  ..^   |
243 | | elfzoelz 10141 |
. . . . . . . . . . . . 13
  ..^
  |
244 | 243 | adantl 277 |
. . . . . . . . . . . 12
 
 ..^    |
245 | 188 | adantr 276 |
. . . . . . . . . . . 12
 
 ..^    |
246 | 244, 245 | gcdcld 11960 |
. . . . . . . . . . 11
 
 ..^      |
247 | 246 | nn0zd 9368 |
. . . . . . . . . 10
 
 ..^      |
248 | | 1zzd 9275 |
. . . . . . . . . 10
 
 ..^    |
249 | | zdceq 9323 |
. . . . . . . . . 10
   
 DECID     |
250 | 247, 248,
249 | syl2anc 411 |
. . . . . . . . 9
 
 ..^  DECID     |
251 | 250 | ralrimiva 2550 |
. . . . . . . 8
   ..^ DECID     |
252 | 242, 251 | ssfirab 6929 |
. . . . . . 7
   ..^      |
253 | 106, 252 | eqeltrid 2264 |
. . . . . 6
   |
254 | | xpfi 6925 |
. . . . . 6
 
     |
255 | 240, 253,
254 | syl2anc 411 |
. . . . 5
     |
256 | | hashen 10756 |
. . . . 5
   
  ♯    ♯       |
257 | 255, 224,
256 | syl2anc 411 |
. . . 4
  ♯    ♯       |
258 | 227, 257 | mpbird 167 |
. . 3
 ♯    ♯    |
259 | | hashxp 10798 |
. . . 4
 
 ♯     ♯  ♯     |
260 | 240, 253,
259 | syl2anc 411 |
. . 3
 ♯     ♯  ♯     |
261 | 258, 260 | eqtr3d 2212 |
. 2
 ♯   ♯  ♯     |
262 | 14, 20 | nnmulcld 8963 |
. . 3
     |
263 | | dfphi2 12211 |
. . . 4
         ♯   ..^           |
264 | 8 | rabeqi 2730 |
. . . . . 6
        ..^    
    |
265 | 3, 264 | eqtri 2198 |
. . . . 5
  ..^    
    |
266 | 265 | fveq2i 5516 |
. . . 4
♯  ♯   ..^          |
267 | 263, 266 | eqtr4di 2228 |
. . 3
         ♯    |
268 | 262, 267 | syl 14 |
. 2
    
  ♯    |
269 | | dfphi2 12211 |
. . . . 5
     ♯   ..^       |
270 | 73 | fveq2i 5516 |
. . . . 5
♯  ♯   ..^      |
271 | 269, 270 | eqtr4di 2228 |
. . . 4
     ♯    |
272 | 14, 271 | syl 14 |
. . 3
     ♯    |
273 | | dfphi2 12211 |
. . . . 5
     ♯   ..^       |
274 | 106 | fveq2i 5516 |
. . . . 5
♯  ♯   ..^      |
275 | 273, 274 | eqtr4di 2228 |
. . . 4
     ♯    |
276 | 20, 275 | syl 14 |
. . 3
     ♯    |
277 | 272, 276 | oveq12d 5889 |
. 2
            ♯  ♯     |
278 | 261, 268,
277 | 3eqtr4d 2220 |
1
    
              |